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 ⊢ N = Lines ⁡ K
linepsubcl.c ⊢ C = PSubCl ⁡ K
Assertion linepsubclN ⊢ K ∈ HL ∧ X ∈ N → X ∈ C

Proof

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