Metamath Proof Explorer


Theorem cdlemk19u

Description: Part of Lemma K of Crawley p. 118. Line 12, p. 120, "f (exponent) tau = k". We represent f, k, tau with F , N , U . (Contributed by NM, 31-Jul-2013)

Ref Expression
Hypotheses cdlemk5.b B = Base K
cdlemk5.l ˙ = K
cdlemk5.j ˙ = join K
cdlemk5.m ˙ = meet K
cdlemk5.a A = Atoms K
cdlemk5.h H = LHyp K
cdlemk5.t T = LTrn K W
cdlemk5.r R = trL K W
cdlemk5.z Z = P ˙ R b ˙ N P ˙ R b F -1
cdlemk5.y Y = P ˙ R g ˙ Z ˙ R g b -1
cdlemk5.x X = ι z T | b T b I B R b R F R b R g z P = Y
cdlemk5.u U = g T if F = N g X
Assertion cdlemk19u K HL W H R F = R N F T N T P A ¬ P ˙ W U F = N

Proof

Step Hyp Ref Expression
1 cdlemk5.b B = Base K
2 cdlemk5.l ˙ = K
3 cdlemk5.j ˙ = join K
4 cdlemk5.m ˙ = meet K
5 cdlemk5.a A = Atoms K
6 cdlemk5.h H = LHyp K
7 cdlemk5.t T = LTrn K W
8 cdlemk5.r R = trL K W
9 cdlemk5.z Z = P ˙ R b ˙ N P ˙ R b F -1
10 cdlemk5.y Y = P ˙ R g ˙ Z ˙ R g b -1
11 cdlemk5.x X = ι z T | b T b I B R b R F R b R g z P = Y
12 cdlemk5.u U = g T if F = N g X
13 simp1l K HL W H R F = R N F T N T P A ¬ P ˙ W K HL W H
14 simp1 K HL W H R F = R N F T N T P A ¬ P ˙ W K HL W H R F = R N
15 simp2l K HL W H R F = R N F T N T P A ¬ P ˙ W F T
16 simp2r K HL W H R F = R N F T N T P A ¬ P ˙ W N T
17 simp3 K HL W H R F = R N F T N T P A ¬ P ˙ W P A ¬ P ˙ W
18 1 2 3 4 5 6 7 8 9 10 11 12 cdlemk35u K HL W H R F = R N F T N T F T P A ¬ P ˙ W U F T
19 14 15 16 15 17 18 syl131anc K HL W H R F = R N F T N T P A ¬ P ˙ W U F T
20 simpr K HL W H R F = R N F T N T P A ¬ P ˙ W F = N F = N
21 simpl2l K HL W H R F = R N F T N T P A ¬ P ˙ W F = N F T
22 11 12 cdlemk40t F = N F T U F = F
23 20 21 22 syl2anc K HL W H R F = R N F T N T P A ¬ P ˙ W F = N U F = F
24 23 fveq1d K HL W H R F = R N F T N T P A ¬ P ˙ W F = N U F P = F P
25 fveq1 F = N F P = N P
26 25 adantl K HL W H R F = R N F T N T P A ¬ P ˙ W F = N F P = N P
27 24 26 eqtrd K HL W H R F = R N F T N T P A ¬ P ˙ W F = N U F P = N P
28 simpl1 K HL W H R F = R N F T N T P A ¬ P ˙ W F N K HL W H R F = R N
29 simpl2l K HL W H R F = R N F T N T P A ¬ P ˙ W F N F T
30 simpr K HL W H R F = R N F T N T P A ¬ P ˙ W F N F N
31 simpl2r K HL W H R F = R N F T N T P A ¬ P ˙ W F N N T
32 simpl3 K HL W H R F = R N F T N T P A ¬ P ˙ W F N P A ¬ P ˙ W
33 1 2 3 4 5 6 7 8 9 10 11 12 cdlemk19u1 K HL W H R F = R N F T F N N T P A ¬ P ˙ W U F P = N P
34 28 29 30 31 32 33 syl131anc K HL W H R F = R N F T N T P A ¬ P ˙ W F N U F P = N P
35 27 34 pm2.61dane K HL W H R F = R N F T N T P A ¬ P ˙ W U F P = N P
36 2 5 6 7 cdlemd K HL W H U F T N T P A ¬ P ˙ W U F P = N P U F = N
37 13 19 16 17 35 36 syl311anc K HL W H R F = R N F T N T P A ¬ P ˙ W U F = N