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 ∧ 𝑋 ∈ 𝐶 ) → ( 𝑀 ‘ ( 𝑈 ‘ 𝑋 ) ) = 𝑋 )