Metamath Proof Explorer


Theorem cdlemk56

Description: Part of Lemma K of Crawley p. 118. Line 11, p. 120, "tau is in Delta" i.e. U is a trace-preserving endormorphism. (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
cdlemk5.e E = TEndo K W
Assertion cdlemk56 K HL W H F T N T R F = R N P A ¬ P ˙ W U E

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 cdlemk5.e E = TEndo K W
14 simp11 K HL W H F T N T R F = R N P A ¬ P ˙ W K HL W H
15 vex g V
16 riotaex ι z T | b T b I B R b R F R b R g z P = Y V
17 11 16 eqeltri X V
18 15 17 ifex if F = N g X V
19 18 rgenw g T if F = N g X V
20 12 fnmpt g T if F = N g X V U Fn T
21 19 20 mp1i K HL W H F T N T R F = R N P A ¬ P ˙ W U Fn T
22 simpl11 K HL W H F T N T R F = R N P A ¬ P ˙ W f T K HL W H
23 simpl2 K HL W H F T N T R F = R N P A ¬ P ˙ W f T R F = R N
24 simpl12 K HL W H F T N T R F = R N P A ¬ P ˙ W f T F T
25 simpl13 K HL W H F T N T R F = R N P A ¬ P ˙ W f T N T
26 simpr K HL W H F T N T R F = R N P A ¬ P ˙ W f T f T
27 simpl3 K HL W H F T N T R F = R N P A ¬ P ˙ W f T P A ¬ P ˙ W
28 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
29 22 23 24 25 26 27 28 syl231anc K HL W H F T N T R F = R N P A ¬ P ˙ W f T U f T
30 29 ralrimiva K HL W H F T N T R F = R N P A ¬ P ˙ W f T U f T
31 ffnfv U : T T U Fn T f T U f T
32 21 30 31 sylanbrc K HL W H F T N T R F = R N P A ¬ P ˙ W U : T T
33 simp11 K HL W H F T N T R F = R N P A ¬ P ˙ W f T h T K HL W H F T N T
34 simp12 K HL W H F T N T R F = R N P A ¬ P ˙ W f T h T R F = R N
35 simp2 K HL W H F T N T R F = R N P A ¬ P ˙ W f T h T f T
36 simp3 K HL W H F T N T R F = R N P A ¬ P ˙ W f T h T h T
37 simp13 K HL W H F T N T R F = R N P A ¬ P ˙ W f T h T P A ¬ P ˙ W
38 1 2 3 4 5 6 7 8 9 10 11 12 cdlemk55u K HL W H F T N T R F = R N f T h T P A ¬ P ˙ W U f h = U f U h
39 33 34 35 36 37 38 syl131anc K HL W H F T N T R F = R N P A ¬ P ˙ W f T h T U f h = U f U h
40 simpl1 K HL W H F T N T R F = R N P A ¬ P ˙ W f T K HL W H F T N T
41 1 2 3 4 5 6 7 8 9 10 11 12 cdlemk39u K HL W H F T N T R F = R N f T P A ¬ P ˙ W R U f ˙ R f
42 40 23 26 27 41 syl121anc K HL W H F T N T R F = R N P A ¬ P ˙ W f T R U f ˙ R f
43 2 6 7 8 13 14 32 39 42 istendod K HL W H F T N T R F = R N P A ¬ P ˙ W U E