Theorem erngplus

Description: Ring addition operation. (Contributed by NM, 10-Jun-2013)

	Ref	Expression
Hypotheses	erngset.h	|- H = ( LHyp ` K )
	erngset.t	|- T = ( ( LTrn ` K ) ` W )
	erngset.e	|- E = ( ( TEndo ` K ) ` W )
	erngset.d	|- D = ( ( EDRing ` K ) ` W )
	erng.p	|- .+ = ( +g ` D )
Assertion	erngplus	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .+ V ) = ( f e. T |-> ( ( U ` f ) o. ( V ` f ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		erngset.h	|- H = ( LHyp ` K )
2		erngset.t	|- T = ( ( LTrn ` K ) ` W )
3		erngset.e	|- E = ( ( TEndo ` K ) ` W )
4		erngset.d	|- D = ( ( EDRing ` K ) ` W )
5		erng.p	|- .+ = ( +g ` D )
6	1 2 3 4 5	erngfplus	|- ( ( K e. HL /\ W e. H ) -> .+ = ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) ) )
7	6	oveqd	|- ( ( K e. HL /\ W e. H ) -> ( U .+ V ) = ( U ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) ) V ) )
8		eqid	|- ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) ) = ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) )
9	8 2	tendopl	|- ( ( U e. E /\ V e. E ) -> ( U ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) ) V ) = ( f e. T |-> ( ( U ` f ) o. ( V ` f ) ) ) )
10	7 9	sylan9eq	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .+ V ) = ( f e. T |-> ( ( U ` f ) o. ( V ` f ) ) ) )