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