Metamath Proof Explorer


Theorem cdlemg31d

Description: Eliminate ( FP ) =/= P from cdlemg31c . TODO: Prove directly. TODO: do we need to eliminate ( FP ) =/= P ? It might be better to do this all at once at the end. See also cdlemg29 versus cdlemg28 . (Contributed by NM, 29-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
cdlemg31.n N = P ˙ v ˙ Q ˙ R F
Assertion cdlemg31d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A ¬ N ˙ 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 cdlemg31.n N = P ˙ v ˙ Q ˙ R F
9 simp22r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A ¬ Q ˙ W
10 9 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P ¬ Q ˙ W
11 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P K HL W H
12 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A P A
13 12 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P P A
14 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A Q A
15 14 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P Q A
16 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A v A
17 16 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P v A
18 simpl31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P F T
19 1 2 3 4 5 6 7 8 cdlemg31b K HL W H P A Q A v A F T N ˙ Q ˙ R F
20 11 13 15 17 18 19 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P N ˙ Q ˙ R F
21 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P P A ¬ P ˙ W
22 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P F P = P
23 eqid 0. K = 0. K
24 1 23 4 5 6 7 trl0 K HL W H P A ¬ P ˙ W F T F P = P R F = 0. K
25 11 21 18 22 24 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P R F = 0. K
26 25 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P Q ˙ R F = Q ˙ 0. K
27 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A K HL
28 hlol K HL K OL
29 27 28 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A K OL
30 29 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P K OL
31 eqid Base K = Base K
32 31 4 atbase Q A Q Base K
33 15 32 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P Q Base K
34 31 2 23 olj01 K OL Q Base K Q ˙ 0. K = Q
35 30 33 34 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P Q ˙ 0. K = Q
36 26 35 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P Q ˙ R F = Q
37 20 36 breqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P N ˙ Q
38 hlatl K HL K AtLat
39 27 38 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A K AtLat
40 39 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P K AtLat
41 simpl33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P N A
42 1 4 atcmp K AtLat N A Q A N ˙ Q N = Q
43 40 41 15 42 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P N ˙ Q N = Q
44 37 43 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P N = Q
45 44 breq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P N ˙ W Q ˙ W
46 10 45 mtbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P = P ¬ N ˙ W
47 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P P K HL W H
48 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P P P A ¬ P ˙ W
49 simpl22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P P Q A ¬ Q ˙ W
50 simpl23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P P v A v ˙ W
51 simpl31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P P F T
52 simpl32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P P v R F
53 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P P F P P
54 simpl33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P P N A
55 1 2 3 4 5 6 7 8 cdlemg31c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F F P P N A ¬ N ˙ W
56 47 48 49 50 51 52 53 54 55 syl323anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A F P P ¬ N ˙ W
57 46 56 pm2.61dane K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W v A v ˙ W F T v R F N A ¬ N ˙ W