Theorem erngplus2-rN

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

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

Proof

Step	Hyp	Ref	Expression
1		erngset.h-r	|- H = ( LHyp ` K )
2		erngset.t-r	|- T = ( ( LTrn ` K ) ` W )
3		erngset.e-r	|- E = ( ( TEndo ` K ) ` W )
4		erngset.d-r	|- D = ( ( EDRingR ` K ) ` W )
5		erng.p-r	|- .+ = ( +g ` D )
6	1 2 3 4 5	erngplus-rN	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .+ V ) = ( f e. T |-> ( ( U ` f ) o. ( V ` f ) ) ) )
7	6	3adantr3	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) -> ( U .+ V ) = ( f e. T |-> ( ( U ` f ) o. ( V ` f ) ) ) )
8		fveq2	|- ( f = F -> ( U ` f ) = ( U ` F ) )
9		fveq2	|- ( f = F -> ( V ` f ) = ( V ` F ) )
10	8 9	coeq12d	|- ( f = F -> ( ( U ` f ) o. ( V ` f ) ) = ( ( U ` F ) o. ( V ` F ) ) )
11	10	adantl	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) /\ f = F ) -> ( ( U ` f ) o. ( V ` f ) ) = ( ( U ` F ) o. ( V ` F ) ) )
12		simpr3	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) -> F e. T )
13		fvex	|- ( U ` F ) e. _V
14		fvex	|- ( V ` F ) e. _V
15	13 14	coex	|- ( ( U ` F ) o. ( V ` F ) ) e. _V
16	15	a1i	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) -> ( ( U ` F ) o. ( V ` F ) ) e. _V )
17	7 11 12 16	fvmptd	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) -> ( ( U .+ V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )