Theorem tendoeq1

Description: Condition determining equality of two trace-preserving endomorphisms. (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypotheses	tendof.h	|- H = ( LHyp ` K )
	tendof.t	|- T = ( ( LTrn ` K ) ` W )
	tendof.e	|- E = ( ( TEndo ` K ) ` W )
Assertion	tendoeq1	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> U = V )

Proof

Step	Hyp	Ref	Expression
1		tendof.h	|- H = ( LHyp ` K )
2		tendof.t	|- T = ( ( LTrn ` K ) ` W )
3		tendof.e	|- E = ( ( TEndo ` K ) ` W )
4		simp3	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> A. f e. T ( U ` f ) = ( V ` f ) )
5		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> ( K e. HL /\ W e. H ) )
6		simp2l	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> U e. E )
7	1 2 3	tendof	|- ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> U : T --> T )
8	5 6 7	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> U : T --> T )
9	8	ffnd	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> U Fn T )
10		simp2r	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> V e. E )
11	1 2 3	tendof	|- ( ( ( K e. HL /\ W e. H ) /\ V e. E ) -> V : T --> T )
12	5 10 11	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> V : T --> T )
13	12	ffnd	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> V Fn T )
14		eqfnfv	|- ( ( U Fn T /\ V Fn T ) -> ( U = V <-> A. f e. T ( U ` f ) = ( V ` f ) ) )
15	9 13 14	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> ( U = V <-> A. f e. T ( U ` f ) = ( V ` f ) ) )
16	4 15	mpbird	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> U = V )