Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tendopltp Unicode version

Theorem tendopltp 29658
 Description: Trace-preserving property of endomorphism sum operation , based on theorem trlco 29605. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 29605) 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 .) (Contributed by NM, 9-Jun-2013.)
Hypotheses
Ref Expression
tendopl.h
tendopl.t
tendopl.e
tendopl.p
tendopltp.l
tendopltp.r
Assertion
Ref Expression
tendopltp
Distinct variable groups:   ,,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)   (,,)   ()   (,,)   (,,)   (,,)   (,,)   (,,)

Proof of Theorem tendopltp
StepHypRef Expression
1 eqid 2253 . 2
2 tendopltp.l . 2
3 simp1l 984 . . 3
4 hllat 28242 . . 3
53, 4syl 17 . 2
6 simp1 960 . . 3
7 tendopl.h . . . 4
8 tendopl.t . . . 4
9 tendopl.e . . . 4
10 tendopl.p . . . 4
117, 8, 9, 10tendoplcl2 29656 . . 3
12 tendopltp.r . . . 4
131, 7, 8, 12trlcl 29042 . . 3
146, 11, 13syl2anc 645 . 2
157, 8, 9tendocl 29645 . . . . 5
16153adant2r 1182 . . . 4
171, 7, 8, 12trlcl 29042 . . . 4
186, 16, 17syl2anc 645 . . 3
197, 8, 9tendocl 29645 . . . . 5
20193adant2l 1181 . . . 4
211, 7, 8, 12trlcl 29042 . . . 4
226, 20, 21syl2anc 645 . . 3
23 eqid 2253 . . . 4
241, 23latjcl 14000 . . 3
255, 18, 22, 24syl3anc 1187 . 2
26 simp3 962 . . 3
271, 7, 8, 12trlcl 29042 . . 3
286, 26, 27syl2anc 645 . 2
29 simp2l 986 . . . . 5
30 simp2r 987 . . . . 5
3110, 8tendopl2 29655 . . . . 5
3229, 30, 26, 31syl3anc 1187 . . . 4
3332fveq2d 5381 . . 3
342, 23, 7, 8, 12trlco 29605 . . . 4
356, 16, 20, 34syl3anc 1187 . . 3
3633, 35eqbrtrd 3940 . 2
372, 7, 8, 12, 9tendotp 29639 . . . 4