Metamath Proof Explorer


Theorem cdlemg33c

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
cdlemg33.o O = P ˙ v ˙ Q ˙ R G
Assertion cdlemg33c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q 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 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
11 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W
12 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N A
13 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r F T
14 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r
15 1 2 3 4 5 6 7 8 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
16 10 11 12 13 14 15 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z ˙ P ˙ v
17 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r K HL
18 17 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A K HL
19 hlatl K HL K AtLat
20 18 19 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A K AtLat
21 eqid 0. K = 0. K
22 21 4 atn0 K AtLat z A z 0. K
23 20 22 sylancom K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z 0. K
24 simp22r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r O = 0. K
25 24 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A O = 0. K
26 23 25 neeqtrrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z O
27 26 biantrud K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z N z N z O
28 27 anbi1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z N z ˙ P ˙ v z N z O z ˙ P ˙ v
29 df-3an z N z O z ˙ P ˙ v z N z O z ˙ P ˙ v
30 28 29 bitr4di K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A z N z ˙ P ˙ v z N z O z ˙ P ˙ v
31 30 anbi2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z ˙ P ˙ v ¬ z ˙ W z N z O z ˙ P ˙ v
32 31 rexbidva K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z ˙ P ˙ v z A ¬ z ˙ W z N z O z ˙ P ˙ v
33 16 32 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W N A O = 0. K F T G T P Q v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z O z ˙ P ˙ v