Theorem erngmul-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.m-r	|- .x. = ( .r ` D )
Assertion	erngmul-rN	|- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .x. V ) = ( V o. U ) )

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.m-r	|- .x. = ( .r ` D )
6	1 2 3 4 5	erngfmul-rN	|- ( ( K e. X /\ W e. H ) -> .x. = ( s e. E , t e. E |-> ( t o. s ) ) )
7	6	adantr	|- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> .x. = ( s e. E , t e. E |-> ( t o. s ) ) )
8	7	oveqd	|- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .x. V ) = ( U ( s e. E , t e. E |-> ( t o. s ) ) V ) )
9		coexg	|- ( ( V e. E /\ U e. E ) -> ( V o. U ) e. _V )
10	9	ancoms	|- ( ( U e. E /\ V e. E ) -> ( V o. U ) e. _V )
11		coeq2	|- ( s = U -> ( t o. s ) = ( t o. U ) )
12		coeq1	|- ( t = V -> ( t o. U ) = ( V o. U ) )
13		eqid	|- ( s e. E , t e. E |-> ( t o. s ) ) = ( s e. E , t e. E |-> ( t o. s ) )
14	11 12 13	ovmpog	|- ( ( U e. E /\ V e. E /\ ( V o. U ) e. _V ) -> ( U ( s e. E , t e. E |-> ( t o. s ) ) V ) = ( V o. U ) )
15	10 14	mpd3an3	|- ( ( U e. E /\ V e. E ) -> ( U ( s e. E , t e. E |-> ( t o. s ) ) V ) = ( V o. U ) )
16	15	adantl	|- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U ( s e. E , t e. E |-> ( t o. s ) ) V ) = ( V o. U ) )
17	8 16	eqtrd	|- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .x. V ) = ( V o. U ) )