Metamath Proof Explorer


Theorem erngfmul

Description: Ring multiplication operation. (Contributed by NM, 9-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.m · ˙ = D
Assertion erngfmul K V W H · ˙ = s E , t E s t

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