Metamath Proof Explorer


Theorem cdlemg27a

Description: For use with case when ( P .\/ v ) ./\ ( Q .\/ ( RF ) ) or ( P .\/ v ) ./\ ( Q .\/ ( RF ) ) is zero, letting us establish -. z .<_ W /\ z .<_ ( P .\/ v ) via 4atex . TODO: Fix comment. (Contributed by NM, 28-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 cdlemg27a K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P ¬ R F ˙ P ˙ z

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 v A v ˙ W z A F T v R F z ˙ P ˙ v F P P K HL W H
9 simp12 K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P P A ¬ P ˙ W
10 simp31 K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P v R F
11 simp13 K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P v A v ˙ W
12 simp2r K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P F T
13 simp33 K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P F P P
14 1 4 5 6 7 trlat K HL W H P A ¬ P ˙ W F T F P P R F A
15 8 9 12 13 14 syl112anc K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P R F A
16 1 5 6 7 trlle K HL W H F T R F ˙ W
17 8 12 16 syl2anc K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P R F ˙ W
18 1 2 4 5 lhp2atnle K HL W H P A ¬ P ˙ W v R F v A v ˙ W R F A R F ˙ W ¬ R F ˙ P ˙ v
19 8 9 10 11 15 17 18 syl312anc K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P ¬ R F ˙ P ˙ v
20 simp11l K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P K HL
21 simp12l K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P P A
22 simp13l K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P v A
23 1 2 4 hlatlej1 K HL P A v A P ˙ P ˙ v
24 20 21 22 23 syl3anc K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P P ˙ P ˙ v
25 simp32 K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P z ˙ P ˙ v
26 20 hllatd K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P K Lat
27 eqid Base K = Base K
28 27 4 atbase P A P Base K
29 21 28 syl K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P P Base K
30 simp2l K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P z A
31 27 4 atbase z A z Base K
32 30 31 syl K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P z Base K
33 27 2 4 hlatjcl K HL P A v A P ˙ v Base K
34 20 21 22 33 syl3anc K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P P ˙ v Base K
35 27 1 2 latjle12 K Lat P Base K z Base K P ˙ v Base K P ˙ P ˙ v z ˙ P ˙ v P ˙ z ˙ P ˙ v
36 26 29 32 34 35 syl13anc K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P P ˙ P ˙ v z ˙ P ˙ v P ˙ z ˙ P ˙ v
37 24 25 36 mpbi2and K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P P ˙ z ˙ P ˙ v
38 27 4 atbase R F A R F Base K
39 15 38 syl K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P R F Base K
40 27 2 4 hlatjcl K HL P A z A P ˙ z Base K
41 20 21 30 40 syl3anc K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P P ˙ z Base K
42 27 1 lattr K Lat R F Base K P ˙ z Base K P ˙ v Base K R F ˙ P ˙ z P ˙ z ˙ P ˙ v R F ˙ P ˙ v
43 26 39 41 34 42 syl13anc K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P R F ˙ P ˙ z P ˙ z ˙ P ˙ v R F ˙ P ˙ v
44 37 43 mpan2d K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P R F ˙ P ˙ z R F ˙ P ˙ v
45 19 44 mtod K HL W H P A ¬ P ˙ W v A v ˙ W z A F T v R F z ˙ P ˙ v F P P ¬ R F ˙ P ˙ z