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⁡Kp≠q∧X=pmap⁡K⁡pjoin⁡Kq
8 3 7 syl ⊢K∈HL→X∈N↔∃p∈Atoms⁡K∃q∈Atoms⁡Kp≠q∧X=pmap⁡K⁡pjoin⁡Kq
9 3 adantr ⊢K∈HL∧p∈Atoms⁡K∧q∈Atoms⁡K→K∈Lat
10 eqid ⊢BaseK=BaseK
11 10 5 atbase ⊢p∈Atoms⁡K→p∈BaseK
12 11 ad2antrl ⊢K∈HL∧p∈Atoms⁡K∧q∈Atoms⁡K→p∈BaseK
13 10 5 atbase ⊢q∈Atoms⁡K→q∈BaseK
14 13 ad2antll ⊢K∈HL∧p∈Atoms⁡K∧q∈Atoms⁡K→q∈BaseK
15 10 4 latjcl ⊢K∈Lat∧p∈BaseK∧q∈BaseK→pjoin⁡Kq∈BaseK
16 9 12 14 15 syl3anc ⊢K∈HL∧p∈Atoms⁡K∧q∈Atoms⁡K→pjoin⁡Kq∈BaseK
17 10 6 2 pmapsubclN ⊢K∈HL∧pjoin⁡Kq∈BaseK→pmap⁡K⁡pjoin⁡Kq∈C
18 16 17 syldan ⊢K∈HL∧p∈Atoms⁡K∧q∈Atoms⁡K→pmap⁡K⁡pjoin⁡Kq∈C
19 eleq1a ⊢pmap⁡K⁡pjoin⁡Kq∈C→X=pmap⁡K⁡pjoin⁡Kq→X∈C
20 18 19 syl ⊢K∈HL∧p∈Atoms⁡K∧q∈Atoms⁡K→X=pmap⁡K⁡pjoin⁡Kq→X∈C
21 20 adantld ⊢K∈HL∧p∈Atoms⁡K∧q∈Atoms⁡K→p≠q∧X=pmap⁡K⁡pjoin⁡Kq→X∈C
22 21 rexlimdvva ⊢K∈HL→∃p∈Atoms⁡K∃q∈Atoms⁡Kp≠q∧X=pmap⁡K⁡pjoin⁡Kq→X∈C
23 8 22 sylbid ⊢K∈HL→X∈N→X∈C
24 23 imp ⊢K∈HL∧X∈N→X∈C