Metamath Proof Explorer

Theorem dvhmulr

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 = LHyp ⁡ K
dvhfmul.t ⊢ T = LTrn ⁡ K ⁡ W
dvhfmul.e ⊢ E = TEndo ⁡ K ⁡ W
dvhfmul.u ⊢ U = DVecH ⁡ K ⁡ W
dvhfmul.f ⊢ F = Scalar ⁡ U
dvhfmul.m ⊢ · ˙ = ⋅ F
Assertion dvhmulr ⊢ K ∈ V ∧ W ∈ H ∧ R ∈ E ∧ S ∈ E → R · ˙ S = R ∘ S

Proof

Step Hyp Ref Expression
1 dvhfmul.h ⊢ H = LHyp ⁡ K
2 dvhfmul.t ⊢ T = LTrn ⁡ K ⁡ W
3 dvhfmul.e ⊢ E = TEndo ⁡ K ⁡ W
4 dvhfmul.u ⊢ U = DVecH ⁡ K ⁡ W
5 dvhfmul.f ⊢ F = Scalar ⁡ U
6 dvhfmul.m ⊢ · ˙ = ⋅ F
7 1 2 3 4 5 6 dvhfmulr ⊢ 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