This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = 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 dvhfmulr ⊢ K ∈ V ∧ W ∈ H → · ˙ = s ∈ E , t ∈ E ⟼ s ∘ t

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 eqid ⊢ EDRing ⁡ K ⁡ W = EDRing ⁡ K ⁡ W
8 1 7 4 5 dvhsca ⊢ K ∈ V ∧ W ∈ H → F = EDRing ⁡ K ⁡ W
9 8 fveq2d ⊢ K ∈ V ∧ W ∈ H → ⋅ F = ⋅ EDRing ⁡ K ⁡ W
10 6 9 eqtrid ⊢ K ∈ V ∧ W ∈ H → · ˙ = ⋅ EDRing ⁡ K ⁡ W
11 eqid ⊢ ⋅ EDRing ⁡ K ⁡ W = ⋅ EDRing ⁡ K ⁡ W
12 1 2 3 7 11 erngfmul ⊢ K ∈ V ∧ W ∈ H → ⋅ EDRing ⁡ K ⁡ W = s ∈ E , t ∈ E ⟼ s ∘ t
13 10 12 eqtrd ⊢ K ∈ V ∧ W ∈ H → · ˙ = s ∈ E , t ∈ E ⟼ s ∘ t