Metamath Proof Explorer


Theorem cdlemg12d

Description: TODO: FIX COMMENT. (Contributed by NM, 5-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
Assertion cdlemg12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R G ˙ R F ˙ F G P ˙ P ˙ F G Q ˙ Q

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 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q K HL W H
9 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P A ¬ P ˙ W
10 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q Q A ¬ Q ˙ W
11 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F T
12 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q G T
13 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P Q
14 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q ¬ R G ˙ P ˙ Q
15 1 2 3 4 5 6 7 cdlemg12c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R G ˙ P ˙ Q P ˙ G P ˙ Q ˙ G Q ˙ G P ˙ F G P ˙ G Q ˙ F G Q ˙ F G P ˙ P ˙ F G Q ˙ Q
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 ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P ˙ G P ˙ Q ˙ G Q ˙ G P ˙ F G P ˙ G Q ˙ F G Q ˙ F G P ˙ P ˙ F G Q ˙ Q
17 1 2 3 4 5 6 7 trlval4 K HL W H G T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R G ˙ P ˙ Q R G = P ˙ G P ˙ Q ˙ G Q
18 8 12 9 10 13 14 17 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R G = P ˙ G P ˙ Q ˙ G Q
19 1 4 5 6 ltrnel K HL W H G T P A ¬ P ˙ W G P A ¬ G P ˙ W
20 8 12 9 19 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q G P A ¬ G P ˙ W
21 1 4 5 6 ltrnel K HL W H G T Q A ¬ Q ˙ W G Q A ¬ G Q ˙ W
22 8 12 10 21 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q G Q A ¬ G Q ˙ W
23 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P A
24 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q Q A
25 4 5 6 ltrn11at K HL W H G T P A Q A P Q G P G Q
26 8 12 23 24 13 25 syl113anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q G P G Q
27 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q ¬ R F ˙ P ˙ Q
28 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F T G T
29 1 2 3 4 5 6 7 cdlemg10c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T R F ˙ G P ˙ G Q R F ˙ P ˙ Q
30 8 9 10 28 29 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F ˙ G P ˙ G Q R F ˙ P ˙ Q
31 27 30 mtbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q ¬ R F ˙ G P ˙ G Q
32 1 2 3 4 5 6 7 trlval4 K HL W H F T G P A ¬ G P ˙ W G Q A ¬ G Q ˙ W G P G Q ¬ R F ˙ G P ˙ G Q R F = G P ˙ F G P ˙ G Q ˙ F G Q
33 8 11 20 22 26 31 32 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F = G P ˙ F G P ˙ G Q ˙ F G Q
34 33 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R F ˙ F G P ˙ P ˙ F G Q ˙ Q = G P ˙ F G P ˙ G Q ˙ F G Q ˙ F G P ˙ P ˙ F G Q ˙ Q
35 16 18 34 3brtr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q R G ˙ R F ˙ F G P ˙ P ˙ F G Q ˙ Q