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

Theorem tendopltp 31514
 Description: Trace-preserving property of endomorphism sum operation , based on theorem trlco 31461. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 31461) 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 2435 . 2
2 tendopltp.l . 2
3 simp1l 981 . . 3
4 hllat 30098 . . 3
53, 4syl 16 . 2
6 simp1 957 . . 3
7 tendopl.h . . . 4
8 tendopl.t . . . 4
9 tendopl.e . . . 4
10 tendopl.p . . . 4
117, 8, 9, 10tendoplcl2 31512 . . 3
12 tendopltp.r . . . 4
131, 7, 8, 12trlcl 30898 . . 3
146, 11, 13syl2anc 643 . 2
157, 8, 9tendocl 31501 . . . . 5
16153adant2r 1179 . . . 4
171, 7, 8, 12trlcl 30898 . . . 4
186, 16, 17syl2anc 643 . . 3
197, 8, 9tendocl 31501 . . . . 5
20193adant2l 1178 . . . 4
211, 7, 8, 12trlcl 30898 . . . 4
226, 20, 21syl2anc 643 . . 3
23 eqid 2435 . . . 4
241, 23latjcl 14471 . . 3
255, 18, 22, 24syl3anc 1184 . 2
26 simp3 959 . . 3
271, 7, 8, 12trlcl 30898 . . 3
286, 26, 27syl2anc 643 . 2
29 simp2l 983 . . . . 5
30 simp2r 984 . . . . 5
3110, 8tendopl2 31511 . . . . 5
3229, 30, 26, 31syl3anc 1184 . . . 4
3332fveq2d 5724 . . 3
342, 23, 7, 8, 12trlco 31461 . . . 4
356, 16, 20, 34syl3anc 1184 . . 3
3633, 35eqbrtrd 4224 . 2
372, 7, 8, 12, 9tendotp 31495 . . . 4