Metamath Proof Explorer

Theorem linepsubclN

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

Ref Expression
Hypotheses linepsubcl.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
linepsubcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion linepsubclN ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → 𝑋 ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 linepsubcl.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
2 linepsubcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
3 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
4 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
5 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6 eqid ⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
7 4 5 1 6 isline2 ⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( ( pmap ‘ 𝐾 ) ‘ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) )
8 3 7 syl ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( ( pmap ‘ 𝐾 ) ‘ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) )
9 3 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ) → 𝐾 ∈ Lat )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 5 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
12 11 ad2antrl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
13 10 5 atbase ⊢ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
14 13 ad2antll ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
15 10 4 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
16 9 12 14 15 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
17 10 6 2 pmapsubclN ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐶 )
18 16 17 syldan ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐶 )
19 eleq1a ⊢ ( ( ( pmap ‘ 𝐾 ) ‘ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐶 → ( 𝑋 = ( ( pmap ‘ 𝐾 ) ‘ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → 𝑋 ∈ 𝐶 ) )
20 18 19 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑋 = ( ( pmap ‘ 𝐾 ) ‘ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → 𝑋 ∈ 𝐶 ) )
21 20 adantld ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( ( pmap ‘ 𝐾 ) ‘ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) → 𝑋 ∈ 𝐶 ) )
22 21 rexlimdvva ⊢ ( 𝐾 ∈ HL → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( ( pmap ‘ 𝐾 ) ‘ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) → 𝑋 ∈ 𝐶 ) )
23 8 22 sylbid ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 → 𝑋 ∈ 𝐶 ) )
24 23 imp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → 𝑋 ∈ 𝐶 )