Metamath Proof Explorer


Theorem isline4N

Description: Definition of line in terms of original lattice elements. (Contributed by NM, 16-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses isline4.b B = Base K
isline4.c C = K
isline4.a A = Atoms K
isline4.n N = Lines K
isline4.m M = pmap K
Assertion isline4N K HL X B M X N p A p C X

Proof

Step Hyp Ref Expression
1 isline4.b B = Base K
2 isline4.c C = K
3 isline4.a A = Atoms K
4 isline4.n N = Lines K
5 isline4.m M = pmap K
6 eqid join K = join K
7 1 6 3 4 5 isline3 K HL X B M X N p A q A p q X = p join K q
8 simpll K HL X B p A K HL
9 1 3 atbase p A p B
10 9 adantl K HL X B p A p B
11 simplr K HL X B p A X B
12 eqid K = K
13 1 12 6 2 3 cvrval3 K HL p B X B p C X q A ¬ q K p p join K q = X
14 8 10 11 13 syl3anc K HL X B p A p C X q A ¬ q K p p join K q = X
15 hlatl K HL K AtLat
16 15 ad3antrrr K HL X B p A q A K AtLat
17 simpr K HL X B p A q A q A
18 simplr K HL X B p A q A p A
19 12 3 atncmp K AtLat q A p A ¬ q K p q p
20 16 17 18 19 syl3anc K HL X B p A q A ¬ q K p q p
21 necom q p p q
22 20 21 bitrdi K HL X B p A q A ¬ q K p p q
23 eqcom p join K q = X X = p join K q
24 23 a1i K HL X B p A q A p join K q = X X = p join K q
25 22 24 anbi12d K HL X B p A q A ¬ q K p p join K q = X p q X = p join K q
26 25 rexbidva K HL X B p A q A ¬ q K p p join K q = X q A p q X = p join K q
27 14 26 bitrd K HL X B p A p C X q A p q X = p join K q
28 27 rexbidva K HL X B p A p C X p A q A p q X = p join K q
29 7 28 bitr4d K HL X B M X N p A p C X