Metamath Proof Explorer


Theorem cdlemg36

Description: Use cdlemg35 to eliminate v from cdlemg34 . TODO: Fix comment. (Contributed by NM, 31-May-2013)

Ref Expression
Hypotheses cdlemg35.l ˙ = K
cdlemg35.j ˙ = join K
cdlemg35.m ˙ = meet K
cdlemg35.a A = Atoms K
cdlemg35.h H = LHyp K
cdlemg35.t T = LTrn K W
cdlemg35.r R = trL K W
Assertion cdlemg36 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ F G P ˙ W = Q ˙ F G Q ˙ W

Proof

Step Hyp Ref Expression
1 cdlemg35.l ˙ = K
2 cdlemg35.j ˙ = join K
3 cdlemg35.m ˙ = meet K
4 cdlemg35.a A = Atoms K
5 cdlemg35.h H = LHyp K
6 cdlemg35.t T = LTrn K W
7 cdlemg35.r R = trL K W
8 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r K HL W H
9 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r P A ¬ P ˙ W
10 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r F T
11 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r G T
12 simp31l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r F P P
13 simp31r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r G P P
14 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r R F R G
15 1 2 3 4 5 6 7 cdlemg35 K HL W H P A ¬ P ˙ W F T G T F P P G P P R F R G v A v ˙ W v R F v R G
16 8 9 10 11 12 13 14 15 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G
17 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
18 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G v A
19 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G v ˙ W
20 18 19 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G v A v ˙ W
21 simp121 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G F T
22 simp122 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G G T
23 21 22 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G F T G T
24 simp123 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G P Q
25 simp3rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G v R F
26 simp3rr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G v R G
27 simp133 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G r A ¬ r ˙ W P ˙ r = Q ˙ r
28 eqid P ˙ v ˙ Q ˙ R F = P ˙ v ˙ Q ˙ R F
29 eqid P ˙ v ˙ Q ˙ R G = P ˙ v ˙ Q ˙ R G
30 1 2 3 4 5 6 7 28 29 cdlemg34 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T G T P Q v R F v R G r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
31 17 20 23 24 25 26 27 30 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
32 31 rexlimdv3a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r v A v ˙ W v R F v R G P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
33 16 32 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F P P G P P R F R G r A ¬ r ˙ W P ˙ r = Q ˙ r P ˙ F G P ˙ W = Q ˙ F G Q ˙ W