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	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
	Assertion	dvhmulr	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E)) \to R \underset{˙}{\cdot} S = R \circ 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	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
7	1 2 3 4 5 6	dvhfmulr	$⊢ (K \in V \land W \in H) \to \underset{˙}{\cdot} = (r \in E, s \in E ⟼ r \circ s)$
8	7	oveqd	$⊢ (K \in V \land W \in H) \to R \underset{˙}{\cdot} S = R (r \in E, s \in E ⟼ r \circ s) S$
9		coexg	$⊢ (R \in E \land S \in E) \to R \circ S \in V$
10		coeq1	$⊢ r = R \to r \circ s = R \circ s$
11		coeq2	$⊢ s = S \to R \circ s = R \circ S$
12		eqid	$⊢ (r \in E, s \in E ⟼ r \circ s) = (r \in E, s \in E ⟼ r \circ s)$
13	10 11 12	ovmpog	$⊢ (R \in E \land S \in E \land R \circ S \in V) \to R (r \in E, s \in E ⟼ r \circ s) S = R \circ S$
14	9 13	mpd3an3	$⊢ (R \in E \land S \in E) \to R (r \in E, s \in E ⟼ r \circ s) S = R \circ S$
15	8 14	sylan9eq	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E)) \to R \underset{˙}{\cdot} S = R \circ S$