Metamath Proof Explorer

Theorem isline3

Description: Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012)

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

Proof

Step Hyp Ref Expression
1 isline3.b ⊢B=BaseK
2 isline3.j ⊢∨˙=join⁡K
3 isline3.a ⊢A=Atoms⁡K
4 isline3.n ⊢N=Lines⁡K
5 isline3.m ⊢M=pmap⁡K
6 hllat ⊢K∈HL→K∈Lat
7 6 adantr ⊢K∈HL∧X∈B→K∈Lat
8 2 3 4 5 isline2 ⊢K∈Lat→M⁡X∈N↔∃p∈A∃q∈Ap≠q∧M⁡X=M⁡p∨˙q
9 7 8 syl ⊢K∈HL∧X∈B→M⁡X∈N↔∃p∈A∃q∈Ap≠q∧M⁡X=M⁡p∨˙q
10 simpll ⊢K∈HL∧X∈B∧p∈A∧q∈A→K∈HL
11 simplr ⊢K∈HL∧X∈B∧p∈A∧q∈A→X∈B
12 6 ad2antrr ⊢K∈HL∧X∈B∧p∈A∧q∈A→K∈Lat
13 1 3 atbase ⊢p∈A→p∈B
14 13 ad2antrl ⊢K∈HL∧X∈B∧p∈A∧q∈A→p∈B
15 1 3 atbase ⊢q∈A→q∈B
16 15 ad2antll ⊢K∈HL∧X∈B∧p∈A∧q∈A→q∈B
17 1 2 latjcl ⊢K∈Lat∧p∈B∧q∈B→p∨˙q∈B
18 12 14 16 17 syl3anc ⊢K∈HL∧X∈B∧p∈A∧q∈A→p∨˙q∈B
19 1 5 pmap11 ⊢K∈HL∧X∈B∧p∨˙q∈B→M⁡X=M⁡p∨˙q↔X=p∨˙q
20 10 11 18 19 syl3anc ⊢K∈HL∧X∈B∧p∈A∧q∈A→M⁡X=M⁡p∨˙q↔X=p∨˙q
21 20 anbi2d ⊢K∈HL∧X∈B∧p∈A∧q∈A→p≠q∧M⁡X=M⁡p∨˙q↔p≠q∧X=p∨˙q
22 21 2rexbidva ⊢K∈HL∧X∈B→∃p∈A∃q∈Ap≠q∧M⁡X=M⁡p∨˙q↔∃p∈A∃q∈Ap≠q∧X=p∨˙q
23 9 22 bitrd ⊢K∈HL∧X∈B→M⁡X∈N↔∃p∈A∃q∈Ap≠q∧X=p∨˙q