Metamath Proof Explorer


Theorem erngfmul-rN

Description: Ring multiplication 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 = EDRing R K W
erng.m-r · ˙ = D
Assertion erngfmul-rN K V W H · ˙ = s E , t E t s

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 = EDRing R K W
5 erng.m-r · ˙ = D
6 1 2 3 4 erngset-rN K V W H D = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E t s
7 6 fveq2d K V W H D = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E t s
8 3 fvexi E V
9 8 8 mpoex s E , t E t s V
10 eqid Base ndx E + ndx s E , t E f T s f t f ndx s E , t E t s = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E t s
11 10 rngmulr s E , t E t s V s E , t E t s = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E t s
12 9 11 ax-mp s E , t E t s = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E t s
13 7 5 12 3eqtr4g K V W H · ˙ = s E , t E t s