Metamath Proof Explorer


Theorem cdlemg4c

Description: TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013)

Ref Expression
Hypotheses cdlemg4.l ˙ = K
cdlemg4.a A = Atoms K
cdlemg4.h H = LHyp K
cdlemg4.t T = LTrn K W
cdlemg4.r R = trL K W
cdlemg4.j ˙ = join K
cdlemg4b.v V = R G
Assertion cdlemg4c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T ¬ Q ˙ P ˙ V ¬ G Q ˙ P ˙ V

Proof

Step Hyp Ref Expression
1 cdlemg4.l ˙ = K
2 cdlemg4.a A = Atoms K
3 cdlemg4.h H = LHyp K
4 cdlemg4.t T = LTrn K W
5 cdlemg4.r R = trL K W
6 cdlemg4.j ˙ = join K
7 cdlemg4b.v V = R G
8 simpll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V K HL W H
9 simplr2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V Q A ¬ Q ˙ W
10 simplr3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V G T
11 1 2 3 4 5 6 7 cdlemg4b2 K HL W H Q A ¬ Q ˙ W G T G Q ˙ V = Q ˙ G Q
12 8 9 10 11 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V G Q ˙ V = Q ˙ G Q
13 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V G Q ˙ P ˙ V
14 simpll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T K HL
15 14 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T K Lat
16 simpr1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T P A
17 eqid Base K = Base K
18 17 2 atbase P A P Base K
19 16 18 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T P Base K
20 simpl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T K HL W H
21 simpr3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G T
22 17 3 4 5 trlcl K HL W H G T R G Base K
23 20 21 22 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T R G Base K
24 7 23 eqeltrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T V Base K
25 17 1 6 latlej2 K Lat P Base K V Base K V ˙ P ˙ V
26 15 19 24 25 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T V ˙ P ˙ V
27 26 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V V ˙ P ˙ V
28 simpr2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T Q A
29 17 2 atbase Q A Q Base K
30 28 29 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T Q Base K
31 17 3 4 ltrncl K HL W H G T Q Base K G Q Base K
32 20 21 30 31 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q Base K
33 17 6 latjcl K Lat P Base K V Base K P ˙ V Base K
34 15 19 24 33 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T P ˙ V Base K
35 17 1 6 latjle12 K Lat G Q Base K V Base K P ˙ V Base K G Q ˙ P ˙ V V ˙ P ˙ V G Q ˙ V ˙ P ˙ V
36 15 32 24 34 35 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V V ˙ P ˙ V G Q ˙ V ˙ P ˙ V
37 36 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V G Q ˙ P ˙ V V ˙ P ˙ V G Q ˙ V ˙ P ˙ V
38 13 27 37 mpbi2and K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V G Q ˙ V ˙ P ˙ V
39 12 38 eqbrtrrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V Q ˙ G Q ˙ P ˙ V
40 15 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V K Lat
41 30 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V Q Base K
42 32 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V G Q Base K
43 19 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V P Base K
44 8 10 22 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V R G Base K
45 7 44 eqeltrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V V Base K
46 40 43 45 33 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V P ˙ V Base K
47 17 1 6 latjle12 K Lat Q Base K G Q Base K P ˙ V Base K Q ˙ P ˙ V G Q ˙ P ˙ V Q ˙ G Q ˙ P ˙ V
48 40 41 42 46 47 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V Q ˙ P ˙ V G Q ˙ P ˙ V Q ˙ G Q ˙ P ˙ V
49 39 48 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V Q ˙ P ˙ V G Q ˙ P ˙ V
50 49 simpld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V Q ˙ P ˙ V
51 50 ex K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G Q ˙ P ˙ V Q ˙ P ˙ V
52 51 con3d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T ¬ Q ˙ P ˙ V ¬ G Q ˙ P ˙ V
53 52 3impia K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T ¬ Q ˙ P ˙ V ¬ G Q ˙ P ˙ V