Metamath Proof Explorer


Theorem dvamulr

Description: Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013)

Ref Expression
Hypotheses dvafmul.h H = LHyp K
dvafmul.t T = LTrn K W
dvafmul.e E = TEndo K W
dvafmul.u U = DVecA K W
dvafmul.f F = Scalar U
dvafmul.p · ˙ = F
Assertion dvamulr K V W H R E S E R · ˙ S = R S

Proof

Step Hyp Ref Expression
1 dvafmul.h H = LHyp K
2 dvafmul.t T = LTrn K W
3 dvafmul.e E = TEndo K W
4 dvafmul.u U = DVecA K W
5 dvafmul.f F = Scalar U
6 dvafmul.p · ˙ = F
7 1 2 3 4 5 6 dvafmulr K V W H · ˙ = r E , s E r s
8 7 oveqd K V W H R · ˙ S = R r E , s E r s S
9 coexg R E S E R S V
10 coeq1 r = R r s = R s
11 coeq2 s = S R s = R S
12 eqid r E , s E r s = r E , s E r s
13 10 11 12 ovmpog R E S E R S V R r E , s E r s S = R S
14 9 13 mpd3an3 R E S E R r E , s E r s S = R S
15 8 14 sylan9eq K V W H R E S E R · ˙ S = R S