Theorem tendoplcl2

Description: Value of result of endomorphism sum operation. (Contributed by NM, 10-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. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
Assertion	tendoplcl2	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( ( U P V ) ` F ) e. T )

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. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
5	4 2	tendopl2	|- ( ( U e. E /\ V e. E /\ F e. T ) -> ( ( U P V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )
6	5	3expa	|- ( ( ( U e. E /\ V e. E ) /\ F e. T ) -> ( ( U P V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )
7	6	3adant1	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( ( U P V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )
8		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( K e. HL /\ W e. H ) )
9	1 2 3	tendocl	|- ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ F e. T ) -> ( U ` F ) e. T )
10	9	3adant2r	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( U ` F ) e. T )
11	1 2 3	tendocl	|- ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ F e. T ) -> ( V ` F ) e. T )
12	11	3adant2l	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( V ` F ) e. T )
13	1 2	ltrnco	|- ( ( ( K e. HL /\ W e. H ) /\ ( U ` F ) e. T /\ ( V ` F ) e. T ) -> ( ( U ` F ) o. ( V ` F ) ) e. T )
14	8 10 12 13	syl3anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( ( U ` F ) o. ( V ` F ) ) e. T )
15	7 14	eqeltrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( ( U P V ) ` F ) e. T )