Metamath Proof Explorer


Theorem llnexchb2

Description: Line exchange property (compare cvlatexchb2 for atoms). (Contributed by NM, 17-Nov-2012)

Ref Expression
Hypotheses llnexch.l ˙ = K
llnexch.j ˙ = join K
llnexch.m ˙ = meet K
llnexch.a A = Atoms K
llnexch.n N = LLines K
Assertion llnexchb2 K HL X N Y N Z N X ˙ Y A X Z X ˙ Y ˙ Z X ˙ Y = X ˙ Z

Proof

Step Hyp Ref Expression
1 llnexch.l ˙ = K
2 llnexch.j ˙ = join K
3 llnexch.m ˙ = meet K
4 llnexch.a A = Atoms K
5 llnexch.n N = LLines K
6 simp23 K HL X N Y N Z N X ˙ Y A X Z Z N
7 simp1 K HL X N Y N Z N X ˙ Y A X Z K HL
8 eqid Base K = Base K
9 8 5 llnbase Z N Z Base K
10 6 9 syl K HL X N Y N Z N X ˙ Y A X Z Z Base K
11 8 2 4 5 islln3 K HL Z Base K Z N p A q A p q Z = p ˙ q
12 7 10 11 syl2anc K HL X N Y N Z N X ˙ Y A X Z Z N p A q A p q Z = p ˙ q
13 6 12 mpbid K HL X N Y N Z N X ˙ Y A X Z p A q A p q Z = p ˙ q
14 simp3r K HL X N Y N Z N X ˙ Y A X Z X Z
15 14 necomd K HL X N Y N Z N X ˙ Y A X Z Z X
16 simp11 K HL X N Y N Z N X ˙ Y A X Z p A q A p q K HL
17 16 hllatd K HL X N Y N Z N X ˙ Y A X Z p A q A p q K Lat
18 simp2l K HL X N Y N Z N X ˙ Y A X Z p A q A p q p A
19 8 4 atbase p A p Base K
20 18 19 syl K HL X N Y N Z N X ˙ Y A X Z p A q A p q p Base K
21 simp2r K HL X N Y N Z N X ˙ Y A X Z p A q A p q q A
22 8 4 atbase q A q Base K
23 21 22 syl K HL X N Y N Z N X ˙ Y A X Z p A q A p q q Base K
24 simp121 K HL X N Y N Z N X ˙ Y A X Z p A q A p q X N
25 8 5 llnbase X N X Base K
26 24 25 syl K HL X N Y N Z N X ˙ Y A X Z p A q A p q X Base K
27 8 1 2 latjle12 K Lat p Base K q Base K X Base K p ˙ X q ˙ X p ˙ q ˙ X
28 17 20 23 26 27 syl13anc K HL X N Y N Z N X ˙ Y A X Z p A q A p q p ˙ X q ˙ X p ˙ q ˙ X
29 simp3 K HL X N Y N Z N X ˙ Y A X Z p A q A p q p q
30 2 4 5 llni2 K HL p A q A p q p ˙ q N
31 16 18 21 29 30 syl31anc K HL X N Y N Z N X ˙ Y A X Z p A q A p q p ˙ q N
32 1 5 llncmp K HL p ˙ q N X N p ˙ q ˙ X p ˙ q = X
33 16 31 24 32 syl3anc K HL X N Y N Z N X ˙ Y A X Z p A q A p q p ˙ q ˙ X p ˙ q = X
34 28 33 bitr2d K HL X N Y N Z N X ˙ Y A X Z p A q A p q p ˙ q = X p ˙ X q ˙ X
35 34 necon3abid K HL X N Y N Z N X ˙ Y A X Z p A q A p q p ˙ q X ¬ p ˙ X q ˙ X
36 ianor ¬ p ˙ X q ˙ X ¬ p ˙ X ¬ q ˙ X
37 35 36 bitrdi K HL X N Y N Z N X ˙ Y A X Z p A q A p q p ˙ q X ¬ p ˙ X ¬ q ˙ X
38 simpl11 K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X K HL
39 24 adantr K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X X N
40 simp122 K HL X N Y N Z N X ˙ Y A X Z p A q A p q Y N
41 40 adantr K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X Y N
42 simpl2l K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X p A
43 simpl2r K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X q A
44 simpr K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X ¬ p ˙ X
45 simp13l K HL X N Y N Z N X ˙ Y A X Z p A q A p q X ˙ Y A
46 45 adantr K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X X ˙ Y A
47 1 2 3 4 5 llnexchb2lem K HL X N Y N p A q A ¬ p ˙ X X ˙ Y A X ˙ Y ˙ p ˙ q X ˙ Y = X ˙ p ˙ q
48 38 39 41 42 43 44 46 47 syl331anc K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X X ˙ Y ˙ p ˙ q X ˙ Y = X ˙ p ˙ q
49 48 ex K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X X ˙ Y ˙ p ˙ q X ˙ Y = X ˙ p ˙ q
50 simpl11 K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X K HL
51 24 adantr K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X X N
52 40 adantr K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X Y N
53 simpl2r K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X q A
54 simpl2l K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X p A
55 simpr K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X ¬ q ˙ X
56 45 adantr K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X X ˙ Y A
57 1 2 3 4 5 llnexchb2lem K HL X N Y N q A p A ¬ q ˙ X X ˙ Y A X ˙ Y ˙ q ˙ p X ˙ Y = X ˙ q ˙ p
58 50 51 52 53 54 55 56 57 syl331anc K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X X ˙ Y ˙ q ˙ p X ˙ Y = X ˙ q ˙ p
59 2 4 hlatjcom K HL p A q A p ˙ q = q ˙ p
60 50 54 53 59 syl3anc K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X p ˙ q = q ˙ p
61 60 breq2d K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X X ˙ Y ˙ p ˙ q X ˙ Y ˙ q ˙ p
62 60 oveq2d K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X X ˙ p ˙ q = X ˙ q ˙ p
63 62 eqeq2d K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X X ˙ Y = X ˙ p ˙ q X ˙ Y = X ˙ q ˙ p
64 58 61 63 3bitr4d K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X X ˙ Y ˙ p ˙ q X ˙ Y = X ˙ p ˙ q
65 64 ex K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ q ˙ X X ˙ Y ˙ p ˙ q X ˙ Y = X ˙ p ˙ q
66 49 65 jaod K HL X N Y N Z N X ˙ Y A X Z p A q A p q ¬ p ˙ X ¬ q ˙ X X ˙ Y ˙ p ˙ q X ˙ Y = X ˙ p ˙ q
67 37 66 sylbid K HL X N Y N Z N X ˙ Y A X Z p A q A p q p ˙ q X X ˙ Y ˙ p ˙ q X ˙ Y = X ˙ p ˙ q
68 neeq1 Z = p ˙ q Z X p ˙ q X
69 breq2 Z = p ˙ q X ˙ Y ˙ Z X ˙ Y ˙ p ˙ q
70 oveq2 Z = p ˙ q X ˙ Z = X ˙ p ˙ q
71 70 eqeq2d Z = p ˙ q X ˙ Y = X ˙ Z X ˙ Y = X ˙ p ˙ q
72 69 71 bibi12d Z = p ˙ q X ˙ Y ˙ Z X ˙ Y = X ˙ Z X ˙ Y ˙ p ˙ q X ˙ Y = X ˙ p ˙ q
73 68 72 imbi12d Z = p ˙ q Z X X ˙ Y ˙ Z X ˙ Y = X ˙ Z p ˙ q X X ˙ Y ˙ p ˙ q X ˙ Y = X ˙ p ˙ q
74 67 73 syl5ibrcom K HL X N Y N Z N X ˙ Y A X Z p A q A p q Z = p ˙ q Z X X ˙ Y ˙ Z X ˙ Y = X ˙ Z
75 74 3exp K HL X N Y N Z N X ˙ Y A X Z p A q A p q Z = p ˙ q Z X X ˙ Y ˙ Z X ˙ Y = X ˙ Z
76 75 imp4a K HL X N Y N Z N X ˙ Y A X Z p A q A p q Z = p ˙ q Z X X ˙ Y ˙ Z X ˙ Y = X ˙ Z
77 76 rexlimdvv K HL X N Y N Z N X ˙ Y A X Z p A q A p q Z = p ˙ q Z X X ˙ Y ˙ Z X ˙ Y = X ˙ Z
78 13 15 77 mp2d K HL X N Y N Z N X ˙ Y A X Z X ˙ Y ˙ Z X ˙ Y = X ˙ Z