Metamath Proof Explorer

Theorem isline2

Description: Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012)

Ref Expression
Hypotheses isline2.j ⊢∨˙=join⁡K
isline2.a ⊢A=Atoms⁡K
isline2.n ⊢N=Lines⁡K
isline2.m ⊢M=pmap⁡K
Assertion isline2 ⊢K∈Lat→X∈N↔∃p∈A∃q∈Ap≠q∧X=M⁡p∨˙q

Proof

Step Hyp Ref Expression
1 isline2.j ⊢∨˙=join⁡K
2 isline2.a ⊢A=Atoms⁡K
3 isline2.n ⊢N=Lines⁡K
4 isline2.m ⊢M=pmap⁡K
5 eqid ⊢≤K=≤K
6 5 1 2 3 isline ⊢K∈Lat→X∈N↔∃p∈A∃q∈Ap≠q∧X=r∈A|r≤Kp∨˙q
7 simpl ⊢K∈Lat∧p∈A∧q∈A→K∈Lat
8 eqid ⊢BaseK=BaseK
9 8 2 atbase ⊢p∈A→p∈BaseK
10 9 ad2antrl ⊢K∈Lat∧p∈A∧q∈A→p∈BaseK
11 8 2 atbase ⊢q∈A→q∈BaseK
12 11 ad2antll ⊢K∈Lat∧p∈A∧q∈A→q∈BaseK
13 8 1 latjcl ⊢K∈Lat∧p∈BaseK∧q∈BaseK→p∨˙q∈BaseK
14 7 10 12 13 syl3anc ⊢K∈Lat∧p∈A∧q∈A→p∨˙q∈BaseK
15 8 5 2 4 pmapval ⊢K∈Lat∧p∨˙q∈BaseK→M⁡p∨˙q=r∈A|r≤Kp∨˙q
16 14 15 syldan ⊢K∈Lat∧p∈A∧q∈A→M⁡p∨˙q=r∈A|r≤Kp∨˙q
17 16 eqeq2d ⊢K∈Lat∧p∈A∧q∈A→X=M⁡p∨˙q↔X=r∈A|r≤Kp∨˙q
18 17 anbi2d ⊢K∈Lat∧p∈A∧q∈A→p≠q∧X=M⁡p∨˙q↔p≠q∧X=r∈A|r≤Kp∨˙q
19 18 2rexbidva ⊢K∈Lat→∃p∈A∃q∈Ap≠q∧X=M⁡p∨˙q↔∃p∈A∃q∈Ap≠q∧X=r∈A|r≤Kp∨˙q
20 6 19 bitr4d ⊢K∈Lat→X∈N↔∃p∈A∃q∈Ap≠q∧X=M⁡p∨˙q