Let X, Tx, phi, N and x be given.
Assume HTx: topology_on X Tx.
Assume HNopen: N ∈ Tx.
Assume HxN: x ∈ N.
Assume Hdisj: support_of X Tx phi ∩ N = Empty.
We will prove apply_fun phi x = 0.
Apply (xm (apply_fun phi x = 0)) to the current goal.
Assume Heq: apply_fun phi x = 0.
An exact proof term for the current goal is Heq.
Assume Hneq0: apply_fun phi x ≠ 0.
Apply FalseE to the current goal.
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HNPow: N ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub N HNopen).
We prove the intermediate claim HNsubX: N ⊆ X.
An exact proof term for the current goal is (PowerE X N HNPow).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HNsubX x HxN).
We prove the intermediate claim HxSupp: x ∈ support_of X Tx phi.
An exact proof term for the current goal is (support_of_contains_nonzero X Tx phi x HTx HxX Hneq0).
We prove the intermediate claim HxInt: x ∈ support_of X Tx phi ∩ N.
An exact proof term for the current goal is (binintersectI (support_of X Tx phi) N x HxSupp HxN).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HxInt.
An exact proof term for the current goal is (EmptyE x HxE).
∎