Metamath Proof Explorer


Theorem tendopltp

Description: Trace-preserving property of endomorphism sum operation P , based on Theorems trlco . Part of remark in Crawley p. 118, 2nd line, "it is clear from the second part of G (our trlco ) that Delta is a subring of E." (In our development, we will bypass their E and go directly to their Delta, whose base set is our ( TEndoK )W .) (Contributed by NM, 9-Jun-2013)

Ref Expression
Hypotheses tendopl.h H = LHyp K
tendopl.t T = LTrn K W
tendopl.e E = TEndo K W
tendopl.p P = s E , t E f T s f t f
tendopltp.l ˙ = K
tendopltp.r R = trL K W
Assertion tendopltp K HL W H U E V E F T R U P V F ˙ R F

Proof

Step Hyp Ref Expression
1 tendopl.h H = LHyp K
2 tendopl.t T = LTrn K W
3 tendopl.e E = TEndo K W
4 tendopl.p P = s E , t E f T s f t f
5 tendopltp.l ˙ = K
6 tendopltp.r R = trL K W
7 eqid Base K = Base K
8 simp1l K HL W H U E V E F T K HL
9 8 hllatd K HL W H U E V E F T K Lat
10 simp1 K HL W H U E V E F T K HL W H
11 1 2 3 4 tendoplcl2 K HL W H U E V E F T U P V F T
12 7 1 2 6 trlcl K HL W H U P V F T R U P V F Base K
13 10 11 12 syl2anc K HL W H U E V E F T R U P V F Base K
14 1 2 3 tendocl K HL W H U E F T U F T
15 14 3adant2r K HL W H U E V E F T U F T
16 7 1 2 6 trlcl K HL W H U F T R U F Base K
17 10 15 16 syl2anc K HL W H U E V E F T R U F Base K
18 1 2 3 tendocl K HL W H V E F T V F T
19 18 3adant2l K HL W H U E V E F T V F T
20 7 1 2 6 trlcl K HL W H V F T R V F Base K
21 10 19 20 syl2anc K HL W H U E V E F T R V F Base K
22 eqid join K = join K
23 7 22 latjcl K Lat R U F Base K R V F Base K R U F join K R V F Base K
24 9 17 21 23 syl3anc K HL W H U E V E F T R U F join K R V F Base K
25 simp3 K HL W H U E V E F T F T
26 7 1 2 6 trlcl K HL W H F T R F Base K
27 10 25 26 syl2anc K HL W H U E V E F T R F Base K
28 simp2l K HL W H U E V E F T U E
29 simp2r K HL W H U E V E F T V E
30 4 2 tendopl2 U E V E F T U P V F = U F V F
31 28 29 25 30 syl3anc K HL W H U E V E F T U P V F = U F V F
32 31 fveq2d K HL W H U E V E F T R U P V F = R U F V F
33 5 22 1 2 6 trlco K HL W H U F T V F T R U F V F ˙ R U F join K R V F
34 10 15 19 33 syl3anc K HL W H U E V E F T R U F V F ˙ R U F join K R V F
35 32 34 eqbrtrd K HL W H U E V E F T R U P V F ˙ R U F join K R V F
36 5 1 2 6 3 tendotp K HL W H U E F T R U F ˙ R F
37 36 3adant2r K HL W H U E V E F T R U F ˙ R F
38 5 1 2 6 3 tendotp K HL W H V E F T R V F ˙ R F
39 38 3adant2l K HL W H U E V E F T R V F ˙ R F
40 7 5 22 latjle12 K Lat R U F Base K R V F Base K R F Base K R U F ˙ R F R V F ˙ R F R U F join K R V F ˙ R F
41 9 17 21 27 40 syl13anc K HL W H U E V E F T R U F ˙ R F R V F ˙ R F R U F join K R V F ˙ R F
42 37 39 41 mpbi2and K HL W H U E V E F T R U F join K R V F ˙ R F
43 7 5 9 13 24 27 35 42 lattrd K HL W H U E V E F T R U P V F ˙ R F