Metamath Proof Explorer


Theorem cdlemg33b0

Description: TODO: Fix comment. (Contributed by NM, 30-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
Assertion cdlemg33b0 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N 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 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r K HL W H
10 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P A ¬ P ˙ W
11 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r Q A ¬ Q ˙ W
12 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N A
13 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v A
14 simp21r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v ˙ W
15 13 14 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W
16 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r F T
17 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v R F
18 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
19 9 10 11 15 16 17 12 18 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ N ˙ W
20 12 19 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N A ¬ N ˙ W
21 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P Q
22 nbrne2 v ˙ W ¬ N ˙ W v N
23 22 necomd v ˙ W ¬ N ˙ W N v
24 14 19 23 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N v
25 13 24 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v A N v
26 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r r A ¬ r ˙ W P ˙ r = Q ˙ r
27 1 2 4 5 4atex3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W N A ¬ N ˙ W P Q v A N v r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z v z ˙ N ˙ v
28 9 10 11 20 21 25 26 27 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z v z ˙ N ˙ v
29 df-3an z N z v z ˙ N ˙ v z N z v z ˙ N ˙ v
30 simpl z N z v z N
31 30 a1i K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z N z v z N
32 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P A
33 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r Q A
34 1 2 3 4 5 6 7 8 cdlemg31a K HL W H P A Q A v A F T N ˙ P ˙ v
35 9 32 33 13 16 34 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N ˙ P ˙ v
36 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r K HL
37 1 2 4 hlatlej2 K HL P A v A v ˙ P ˙ v
38 36 32 13 37 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v ˙ P ˙ v
39 36 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r K Lat
40 eqid Base K = Base K
41 40 4 atbase N A N Base K
42 12 41 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N Base K
43 40 4 atbase v A v Base K
44 13 43 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v Base K
45 40 2 4 hlatjcl K HL P A v A P ˙ v Base K
46 36 32 13 45 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ v Base K
47 40 1 2 latjle12 K Lat N Base K v Base K P ˙ v Base K N ˙ P ˙ v v ˙ P ˙ v N ˙ v ˙ P ˙ v
48 39 42 44 46 47 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N ˙ P ˙ v v ˙ P ˙ v N ˙ v ˙ P ˙ v
49 35 38 48 mpbi2and K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N ˙ v ˙ P ˙ v
50 49 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A N ˙ v ˙ P ˙ v
51 39 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A K Lat
52 40 4 atbase z A z Base K
53 52 adantl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z Base K
54 40 2 4 hlatjcl K HL N A v A N ˙ v Base K
55 36 12 13 54 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N ˙ v Base K
56 55 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A N ˙ v Base K
57 46 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A P ˙ v Base K
58 40 1 lattr K Lat z Base K N ˙ v Base K P ˙ v Base K z ˙ N ˙ v N ˙ v ˙ P ˙ v z ˙ P ˙ v
59 51 53 56 57 58 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z ˙ N ˙ v N ˙ v ˙ P ˙ v z ˙ P ˙ v
60 50 59 mpan2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z ˙ N ˙ v z ˙ P ˙ v
61 31 60 anim12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z N z v z ˙ N ˙ v z N z ˙ P ˙ v
62 29 61 syl5bi K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z N z v z ˙ N ˙ v z N z ˙ P ˙ v
63 62 anim2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z v z ˙ N ˙ v ¬ z ˙ W z N z ˙ P ˙ v
64 63 reximdva K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z v z ˙ N ˙ v z A ¬ z ˙ W z N z ˙ P ˙ v
65 28 64 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A F T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z ˙ P ˙ v