Metamath Proof Explorer


Theorem cdlemg12e

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
cdlemg12e.z 0 ˙ = 0. K
Assertion cdlemg12e 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 ˙ P ˙ F G Q ˙ Q 0 ˙

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 cdlemg12e.z 0 ˙ = 0. K
9 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 R F R G
10 simpl1 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
11 simpl21 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ F T
12 simpl22 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ G T
13 simpl23 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ P Q
14 simpl31 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ ¬ R F ˙ P ˙ Q
15 simpl32 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ ¬ R G ˙ P ˙ Q
16 1 2 3 4 5 6 7 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
17 10 11 12 13 14 15 16 syl123anc 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R G ˙ R F ˙ F G P ˙ P ˙ F G Q ˙ Q
18 simpr 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ F G P ˙ P ˙ F G Q ˙ Q = 0 ˙
19 18 oveq2d 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R F ˙ F G P ˙ P ˙ F G Q ˙ Q = R F ˙ 0 ˙
20 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 K HL
21 20 adantr 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ K HL
22 hlol K HL K OL
23 21 22 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ K OL
24 simpl11 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ K HL W H
25 eqid Base K = Base K
26 25 5 6 7 trlcl K HL W H F T R F Base K
27 24 11 26 syl2anc 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R F Base K
28 25 2 8 olj01 K OL R F Base K R F ˙ 0 ˙ = R F
29 23 27 28 syl2anc 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R F ˙ 0 ˙ = R F
30 19 29 eqtrd 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R F ˙ F G P ˙ P ˙ F G Q ˙ Q = R F
31 17 30 breqtrd 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R G ˙ R F
32 hlatl K HL K AtLat
33 21 32 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ K AtLat
34 hlop K HL K OP
35 21 34 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ K OP
36 25 5 6 7 trlcl K HL W H G T R G Base K
37 24 12 36 syl2anc 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R G Base K
38 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 P A
39 38 adantr 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ P A
40 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 Q A
41 40 adantr 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ Q A
42 25 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
43 21 39 41 42 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ P ˙ Q Base K
44 25 1 8 opnlen0 K OP R G Base K P ˙ Q Base K ¬ R G ˙ P ˙ Q R G 0 ˙
45 35 37 43 15 44 syl31anc 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R G 0 ˙
46 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 W H
47 46 adantr 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ W H
48 8 4 5 6 7 trlatn0 K HL W H G T R G A R G 0 ˙
49 21 47 12 48 syl21anc 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R G A R G 0 ˙
50 45 49 mpbird 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R G A
51 25 1 8 opnlen0 K OP R F Base K P ˙ Q Base K ¬ R F ˙ P ˙ Q R F 0 ˙
52 35 27 43 14 51 syl31anc 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R F 0 ˙
53 8 4 5 6 7 trlatn0 K HL W H F T R F A R F 0 ˙
54 21 47 11 53 syl21anc 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R F A R F 0 ˙
55 52 54 mpbird 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R F A
56 1 4 atcmp K AtLat R G A R F A R G ˙ R F R G = R F
57 33 50 55 56 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R G ˙ R F R G = R F
58 31 57 mpbid 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R G = R F
59 58 eqcomd 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R F = R G
60 59 ex 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 ˙ P ˙ F G Q ˙ Q = 0 ˙ R F = R G
61 60 necon3d 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 R F R G F G P ˙ P ˙ F G Q ˙ Q 0 ˙
62 9 61 mpd 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 ˙ P ˙ F G Q ˙ Q 0 ˙