Theorem erngfplus-rN

Description: Ring addition operation. (Contributed by NM, 9-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	erngfplus-rN	|- ( ( K e. V /\ W e. H ) -> .+ = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` 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	erngset-rN	|- ( ( K e. V /\ W e. H ) -> D = { <. ( Base ` ndx ) , E >. , <. ( +g ` ndx ) , ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. E , t e. E |-> ( t o. s ) ) >. } )
7	6	fveq2d	|- ( ( K e. V /\ W e. H ) -> ( +g ` D ) = ( +g ` { <. ( Base ` ndx ) , E >. , <. ( +g ` ndx ) , ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. E , t e. E |-> ( t o. s ) ) >. } ) )
8	3	fvexi	|- E e. _V
9	8 8	mpoex	|- ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) e. _V
10		eqid	|- { <. ( Base ` ndx ) , E >. , <. ( +g ` ndx ) , ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. E , t e. E |-> ( t o. s ) ) >. } = { <. ( Base ` ndx ) , E >. , <. ( +g ` ndx ) , ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. E , t e. E |-> ( t o. s ) ) >. }
11	10	rngplusg	|- ( ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) e. _V -> ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) = ( +g ` { <. ( Base ` ndx ) , E >. , <. ( +g ` ndx ) , ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. E , t e. E |-> ( t o. s ) ) >. } ) )
12	9 11	ax-mp	|- ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) = ( +g ` { <. ( Base ` ndx ) , E >. , <. ( +g ` ndx ) , ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. E , t e. E |-> ( t o. s ) ) >. } )
13	7 5 12	3eqtr4g	|- ( ( K e. V /\ W e. H ) -> .+ = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) )