Metamath Proof Explorer

Theorem pmapidclN

Description: Projective map of the LUB of a closed subspace. (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmapidcl.u ⊢ U = lub ⁡ K
pmapidcl.m ⊢ M = pmap ⁡ K
pmapidcl.c ⊢ C = PSubCl ⁡ K
Assertion pmapidclN ⊢ K ∈ HL ∧ X ∈ C → M ⁡ U ⁡ X = X

Proof

Step Hyp Ref Expression
1 pmapidcl.u ⊢ U = lub ⁡ K
2 pmapidcl.m ⊢ M = pmap ⁡ K
3 pmapidcl.c ⊢ C = PSubCl ⁡ K
4 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
5 4 3 psubclssatN ⊢ K ∈ HL ∧ X ∈ C → X ⊆ Atoms ⁡ K
6 eqid ⊢ ⊥ 𝑃 ⁡ K = ⊥ 𝑃 ⁡ K
7 1 4 2 6 2polvalN ⊢ K ∈ HL ∧ X ⊆ Atoms ⁡ K → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ X = M ⁡ U ⁡ X
8 5 7 syldan ⊢ K ∈ HL ∧ X ∈ C → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ X = M ⁡ U ⁡ X
9 6 3 psubcli2N ⊢ K ∈ HL ∧ X ∈ C → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ X = X
10 8 9 eqtr3d ⊢ K ∈ HL ∧ X ∈ C → M ⁡ U ⁡ X = X