Metamath Proof Explorer


Theorem cdlemg33b

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 cdlemg33b 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 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 df-3an z N z O z ˙ P ˙ v z N z O z ˙ P ˙ v
11 neeq2 N = O z N z O
12 11 anbi2d N = O z N z N z N z O
13 anidm z N z N z N
14 12 13 bitr3di N = O z N z O z N
15 14 anbi1d N = O z N z O z ˙ P ˙ v z N z ˙ P ˙ v
16 10 15 syl5bb N = O z N z O z ˙ P ˙ v z N z ˙ P ˙ v
17 16 anbi2d N = O ¬ z ˙ W z N z O z ˙ P ˙ v ¬ z ˙ W z N z ˙ P ˙ v
18 17 rexbidv N = O z A ¬ z ˙ W z N z O z ˙ P ˙ v z A ¬ z ˙ W z N z ˙ P ˙ v
19 simpl1 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N O K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
20 simpl2 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N O v A v ˙ W N A O A F T G T
21 simpl31 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N O P Q
22 simpr 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N O 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N O P Q N O
24 simpl32 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N O v R F
25 simpl33 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N O r A ¬ r ˙ W P ˙ r = Q ˙ r
26 1 2 3 4 5 6 7 8 9 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
27 19 20 23 24 25 26 syl113anc 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N O z A ¬ z ˙ W z N z O z ˙ P ˙ v
28 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W
29 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r N A
30 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r F T
31 28 29 30 3jca 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W N A F T
32 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
33 31 32 syld3an2 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z ˙ P ˙ v
34 18 27 33 pm2.61ne 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 v R F r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W z N z O z ˙ P ˙ v