Theorem pmapsubclN

Description: A projective map value is a closed projective subspace. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmapsubcl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	pmapsubcl.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
	pmapsubcl.c	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion	pmapsubclN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		pmapsubcl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		pmapsubcl.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
3		pmapsubcl.c	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
4		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
5	1 4 2	pmapssat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
6		eqid	⊢ ( ⊥𝑃 ‘ 𝐾 ) = ( ⊥𝑃 ‘ 𝐾 )
7	1 2 6	2polpmapN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( 𝑀 ‘ 𝑋 ) )
8	4 6 3	ispsubclN	⊢ ( 𝐾 ∈ HL → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝐶 ↔ ( ( 𝑀 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( 𝑀 ‘ 𝑋 ) ) ) )
9	8	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝐶 ↔ ( ( 𝑀 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( 𝑀 ‘ 𝑋 ) ) ) )
10	5 7 9	mpbir2and	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝐶 )