Metamath Proof Explorer


Theorem cdlemg4

Description: TODO: FIX COMMENT. (Contributed by NM, 25-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 cdlemg4 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P F G Q = Q

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 eqid meet K = meet K
9 1 2 3 4 5 6 7 8 cdlemg4g K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P F G Q = Q ˙ V meet K P ˙ Q
10 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P K HL
11 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P A
12 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P Q A
13 6 2 hlatjcom K HL P A Q A P ˙ Q = Q ˙ P
14 10 11 12 13 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P ˙ Q = Q ˙ P
15 14 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P Q ˙ V meet K P ˙ Q = Q ˙ V meet K Q ˙ P
16 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P K HL W H
17 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P G T
18 eqid Base K = Base K
19 18 3 4 5 trlcl K HL W H G T R G Base K
20 16 17 19 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P R G Base K
21 7 20 eqeltrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P V Base K
22 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P ¬ Q ˙ P ˙ V
23 simp21r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P ¬ P ˙ W
24 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P A ¬ P ˙ W
25 1 6 8 2 3 4 5 trlval2 K HL W H G T P A ¬ P ˙ W R G = P ˙ G P meet K W
26 16 17 24 25 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P R G = P ˙ G P meet K W
27 7 26 syl5eq K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P V = P ˙ G P meet K W
28 10 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P K Lat
29 1 2 3 4 ltrnel K HL W H G T P A ¬ P ˙ W G P A ¬ G P ˙ W
30 16 17 24 29 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P G P A ¬ G P ˙ W
31 30 simpld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P G P A
32 18 6 2 hlatjcl K HL P A G P A P ˙ G P Base K
33 10 11 31 32 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P ˙ G P Base K
34 simp1r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P W H
35 18 3 lhpbase W H W Base K
36 34 35 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P W Base K
37 18 1 8 latmle2 K Lat P ˙ G P Base K W Base K P ˙ G P meet K W ˙ W
38 28 33 36 37 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P ˙ G P meet K W ˙ W
39 27 38 eqbrtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P V ˙ W
40 18 2 atbase P A P Base K
41 11 40 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P Base K
42 18 1 lattr K Lat P Base K V Base K W Base K P ˙ V V ˙ W P ˙ W
43 28 41 21 36 42 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P ˙ V V ˙ W P ˙ W
44 39 43 mpan2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P ˙ V P ˙ W
45 23 44 mtod K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P ¬ P ˙ V
46 18 1 6 2 hlexch2 K HL P A Q A V Base K ¬ P ˙ V P ˙ Q ˙ V Q ˙ P ˙ V
47 10 11 12 21 45 46 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P ˙ Q ˙ V Q ˙ P ˙ V
48 22 47 mtod K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P ¬ P ˙ Q ˙ V
49 18 1 6 8 2 2llnma1b K HL V Base K Q A P A ¬ P ˙ Q ˙ V Q ˙ V meet K Q ˙ P = Q
50 10 21 12 11 48 49 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P Q ˙ V meet K Q ˙ P = Q
51 9 15 50 3eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P F G Q = Q