Metamath Proof Explorer


Theorem cdlemg12f

Description: TODO: FIX COMMENT. (Contributed by NM, 6-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 cdlemg12f 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 R G F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ Q ˙ F G Q ˙ P ˙ F G P ˙ W

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 simp11l 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 R G F G P ˙ F G Q P ˙ Q K HL
9 8 hllatd 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 R G F G P ˙ F G Q P ˙ Q K Lat
10 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 R F R G F G P ˙ F G Q P ˙ Q P A
11 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 R F R G F G P ˙ F G Q P ˙ Q K HL W H
12 simp21 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 R G F G P ˙ F G Q P ˙ Q F T
13 simp22 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 R G F G P ˙ F G Q P ˙ Q G T
14 1 4 5 6 ltrncoat K HL W H F T G T P A F G P A
15 11 12 13 10 14 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 R G F G P ˙ F G Q P ˙ Q F G P A
16 eqid Base K = Base K
17 16 2 4 hlatjcl K HL P A F G P A P ˙ F G P Base K
18 8 10 15 17 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 R F R G F G P ˙ F G Q P ˙ Q P ˙ F G P Base K
19 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 R F R G F G P ˙ F G Q P ˙ Q Q A
20 1 4 5 6 ltrncoat K HL W H F T G T Q A F G Q A
21 11 12 13 19 20 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 R G F G P ˙ F G Q P ˙ Q F G Q A
22 16 2 4 hlatjcl K HL Q A F G Q A Q ˙ F G Q Base K
23 8 19 21 22 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 R F R G F G P ˙ F G Q P ˙ Q Q ˙ F G Q Base K
24 16 1 3 latmle1 K Lat P ˙ F G P Base K Q ˙ F G Q Base K P ˙ F G P ˙ Q ˙ F G Q ˙ P ˙ F G P
25 9 18 23 24 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 R F R G F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ Q ˙ F G Q ˙ P ˙ F G P
26 simp1 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 R G F G P ˙ F G Q P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
27 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 R F R G F G P ˙ F G Q P ˙ Q F T G T P Q
28 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 F R G F G P ˙ F G Q P ˙ Q F G P ˙ F G Q P ˙ Q
29 simp31l 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 R G F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q
30 simp31r 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 R G F G P ˙ F G Q P ˙ Q ¬ R G ˙ P ˙ Q
31 1 2 3 4 5 6 7 cdlemg10 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P ˙ F G P ˙ Q ˙ F G Q ˙ W
32 26 27 28 29 30 31 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 R F R G F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ Q ˙ F G Q ˙ W
33 16 3 latmcl K Lat P ˙ F G P Base K Q ˙ F G Q Base K P ˙ F G P ˙ Q ˙ F G Q Base K
34 9 18 23 33 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 R F R G F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ Q ˙ F G Q Base K
35 simp11r 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 R G F G P ˙ F G Q P ˙ Q W H
36 16 5 lhpbase W H W Base K
37 35 36 syl 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 R G F G P ˙ F G Q P ˙ Q W Base K
38 16 1 3 latlem12 K Lat P ˙ F G P ˙ Q ˙ F G Q Base K P ˙ F G P Base K W Base K P ˙ F G P ˙ Q ˙ F G Q ˙ P ˙ F G P P ˙ F G P ˙ Q ˙ F G Q ˙ W P ˙ F G P ˙ Q ˙ F G Q ˙ P ˙ F G P ˙ W
39 9 34 18 37 38 syl13anc 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 R G F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ Q ˙ F G Q ˙ P ˙ F G P P ˙ F G P ˙ Q ˙ F G Q ˙ W P ˙ F G P ˙ Q ˙ F G Q ˙ P ˙ F G P ˙ W
40 25 32 39 mpbi2and 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 R G F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ Q ˙ F G Q ˙ P ˙ F G P ˙ W