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	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
Assertion	dvamulr	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E)) \to R \underset{˙}{\cdot} S = R \circ S$

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	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
7	1 2 3 4 5 6	dvafmulr	$⊢ (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$

Metamath Proof Explorer