Metamath Proof Explorer


Theorem dvhfmulr

Description: Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dvhfmul.h H=LHypK
dvhfmul.t T=LTrnKW
dvhfmul.e E=TEndoKW
dvhfmul.u U=DVecHKW
dvhfmul.f F=ScalarU
dvhfmul.m ·˙=F
Assertion dvhfmulr KVWH·˙=sE,tEst

Proof

Step Hyp Ref Expression
1 dvhfmul.h H=LHypK
2 dvhfmul.t T=LTrnKW
3 dvhfmul.e E=TEndoKW
4 dvhfmul.u U=DVecHKW
5 dvhfmul.f F=ScalarU
6 dvhfmul.m ·˙=F
7 eqid EDRingKW=EDRingKW
8 1 7 4 5 dvhsca KVWHF=EDRingKW
9 8 fveq2d KVWHF=EDRingKW
10 6 9 eqtrid KVWH·˙=EDRingKW
11 eqid EDRingKW=EDRingKW
12 1 2 3 7 11 erngfmul KVWHEDRingKW=sE,tEst
13 10 12 eqtrd KVWH·˙=sE,tEst