Theorem tendo0tp

Description: Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypotheses	tendo0.b	|- B = ( Base ` K )
	tendo0.h	|- H = ( LHyp ` K )
	tendo0.t	|- T = ( ( LTrn ` K ) ` W )
	tendo0.e	|- E = ( ( TEndo ` K ) ` W )
	tendo0.o	|- O = ( f e. T |-> ( _I |` B ) )
	tendo0tp.l	|- .<_ = ( le ` K )
	tendo0tp.r	|- R = ( ( trL ` K ) ` W )
Assertion	tendo0tp	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` ( O ` F ) ) .<_ ( R ` F ) )

Proof

Step	Hyp	Ref	Expression
1		tendo0.b	|- B = ( Base ` K )
2		tendo0.h	|- H = ( LHyp ` K )
3		tendo0.t	|- T = ( ( LTrn ` K ) ` W )
4		tendo0.e	|- E = ( ( TEndo ` K ) ` W )
5		tendo0.o	|- O = ( f e. T |-> ( _I |` B ) )
6		tendo0tp.l	|- .<_ = ( le ` K )
7		tendo0tp.r	|- R = ( ( trL ` K ) ` W )
8	5 1	tendo02	|- ( F e. T -> ( O ` F ) = ( _I |` B ) )
9	8	adantl	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( O ` F ) = ( _I |` B ) )
10	9	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` ( O ` F ) ) = ( R ` ( _I |` B ) ) )
11		eqid	|- ( 0. ` K ) = ( 0. ` K )
12	1 11 2 7	trlid0	|- ( ( K e. HL /\ W e. H ) -> ( R ` ( _I |` B ) ) = ( 0. ` K ) )
13	12	adantr	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` ( _I |` B ) ) = ( 0. ` K ) )
14	10 13	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` ( O ` F ) ) = ( 0. ` K ) )
15		hlop	|- ( K e. HL -> K e. OP )
16	15	ad2antrr	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> K e. OP )
17	1 2 3 7	trlcl	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. B )
18	1 6 11	op0le	|- ( ( K e. OP /\ ( R ` F ) e. B ) -> ( 0. ` K ) .<_ ( R ` F ) )
19	16 17 18	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( 0. ` K ) .<_ ( R ` F ) )
20	14 19	eqbrtrd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` ( O ` F ) ) .<_ ( R ` F ) )