This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑈 = ( lub ‘ 𝐾 )
pmapidcl.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
pmapidcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion pmapidclN ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → ( 𝑀 ‘ ( 𝑈 ‘ 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 pmapidcl.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
2 pmapidcl.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
3 pmapidcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
4 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
5 4 3 psubclssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
6 eqid ⊢ ( ⊥𝑃 ‘ 𝐾 ) = ( ⊥𝑃 ‘ 𝐾 )
7 1 4 2 6 2polvalN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( 𝑈 ‘ 𝑋 ) ) )
8 5 7 syldan ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( 𝑈 ‘ 𝑋 ) ) )
9 6 3 psubcli2N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 )
10 8 9 eqtr3d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → ( 𝑀 ‘ ( 𝑈 ‘ 𝑋 ) ) = 𝑋 )