Metamath Proof Explorer


Theorem cdlemg33a

Description: TODO: Fix comment. (Contributed by NM, 29-May-2013)

Ref Expression
Hypotheses cdlemg12.l ˙ = K
cdlemg12.j ˙ = join K
cdlemg12.m ˙ = meet K
cdlemg12.a A = Atoms K
cdlemg12.h H = LHyp K
cdlemg12.t T = LTrn K W
cdlemg12b.r R = trL K W
cdlemg31.n N = P ˙ v ˙ Q ˙ R F
cdlemg33.o O = P ˙ v ˙ Q ˙ R G
Assertion cdlemg33a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z O z ˙ P ˙ v

Proof

Step Hyp Ref Expression
1 cdlemg12.l ˙ = K
2 cdlemg12.j ˙ = join K
3 cdlemg12.m ˙ = meet K
4 cdlemg12.a A = Atoms K
5 cdlemg12.h H = LHyp K
6 cdlemg12.t T = LTrn K W
7 cdlemg12b.r R = trL K W
8 cdlemg31.n N = P ˙ v ˙ Q ˙ R F
9 cdlemg33.o O = P ˙ v ˙ Q ˙ R G
10 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r K HL W H
11 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P A ¬ P ˙ W
12 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r Q A ¬ Q ˙ W
13 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N A
14 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W
15 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r F T
16 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v R F
17 1 2 3 4 5 6 7 8 cdlemg31d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A ¬ N ˙ W
18 10 11 12 14 15 16 13 17 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ N ˙ W
19 13 18 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N A ¬ N ˙ W
20 simp31l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P Q
21 simp22r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r O A
22 simp31r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N O
23 21 22 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r O A N O
24 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r r A ¬ r ˙ W P ˙ r = Q ˙ r
25 1 2 4 5 4atex3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W N A ¬ N ˙ W P Q O A N O r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z O z ˙ N ˙ O
26 10 11 12 19 20 23 24 25 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z O z ˙ N ˙ O
27 idd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z N z N
28 idd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z O z O
29 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P A
30 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r Q A
31 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v A
32 1 2 3 4 5 6 7 8 cdlemg31a K HL W H P A Q A v A F T N ˙ P ˙ v
33 10 29 30 31 15 32 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N ˙ P ˙ v
34 simp23r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r G T
35 1 2 3 4 5 6 7 9 cdlemg31a K HL W H P A Q A v A G T O ˙ P ˙ v
36 10 29 30 31 34 35 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r O ˙ P ˙ v
37 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r K HL
38 37 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r K Lat
39 eqid Base K = Base K
40 39 4 atbase N A N Base K
41 13 40 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N Base K
42 39 2 4 hlatjcl K HL P A v A P ˙ v Base K
43 37 29 31 42 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ v Base K
44 39 4 atbase O A O Base K
45 21 44 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r O Base K
46 39 1 2 latjlej12 K Lat N Base K P ˙ v Base K O Base K P ˙ v Base K N ˙ P ˙ v O ˙ P ˙ v N ˙ O ˙ P ˙ v ˙ P ˙ v
47 38 41 43 45 43 46 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N ˙ P ˙ v O ˙ P ˙ v N ˙ O ˙ P ˙ v ˙ P ˙ v
48 33 36 47 mp2and K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N ˙ O ˙ P ˙ v ˙ P ˙ v
49 39 2 latjidm K Lat P ˙ v Base K P ˙ v ˙ P ˙ v = P ˙ v
50 38 43 49 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ v ˙ P ˙ v = P ˙ v
51 48 50 breqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N ˙ O ˙ P ˙ v
52 51 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A N ˙ O ˙ P ˙ v
53 38 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A K Lat
54 39 4 atbase z A z Base K
55 54 adantl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z Base K
56 39 2 4 hlatjcl K HL N A O A N ˙ O Base K
57 37 13 21 56 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N ˙ O Base K
58 57 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A N ˙ O Base K
59 43 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A P ˙ v Base K
60 39 1 lattr K Lat z Base K N ˙ O Base K P ˙ v Base K z ˙ N ˙ O N ˙ O ˙ P ˙ v z ˙ P ˙ v
61 53 55 58 59 60 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z ˙ N ˙ O N ˙ O ˙ P ˙ v z ˙ P ˙ v
62 52 61 mpan2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z ˙ N ˙ O z ˙ P ˙ v
63 27 28 62 3anim123d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z N z O z ˙ N ˙ O z N z O z ˙ P ˙ v
64 63 anim2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z O z ˙ N ˙ O ¬ z ˙ W z N z O z ˙ P ˙ v
65 64 reximdva K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z O z ˙ N ˙ O z A ¬ z ˙ W z N z O z ˙ P ˙ v
66 26 65 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O A F T G T P Q N O v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z O z ˙ P ˙ v