ldualvsass2

Description: Associative law for scalar product operation, using operations from the dual space. (Contributed by NM, 20-Oct-2014)

	Ref	Expression
Hypotheses	ldualvsass2.f	$⊢ F = LFnl (W)$
	ldualvsass2.r	$⊢ R = Scalar (W)$
	ldualvsass2.k	$⊢ K = {Base}_{R}$
	ldualvsass2.d	$⊢ D = LDual (W)$
	ldualvsass2.q	$⊢ Q = Scalar (D)$
	ldualvsass2.t	$⊢ \underset{˙}{\times} = \cdot_{Q}$
	ldualvsass2.s	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	ldualvsass2.w	$⊢ φ \to W \in LMod$
	ldualvsass2.x	$⊢ φ \to X \in K$
	ldualvsass2.y	$⊢ φ \to Y \in K$
	ldualvsass2.g	$⊢ φ \to G \in F$
Assertion	ldualvsass2	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} G = X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} G)$

Step	Hyp	Ref	Expression
1		ldualvsass2.f	$⊢ F = LFnl (W)$
2		ldualvsass2.r	$⊢ R = Scalar (W)$
3		ldualvsass2.k	$⊢ K = {Base}_{R}$
4		ldualvsass2.d	$⊢ D = LDual (W)$
5		ldualvsass2.q	$⊢ Q = Scalar (D)$
6		ldualvsass2.t	$⊢ \underset{˙}{\times} = \cdot_{Q}$
7		ldualvsass2.s	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
8		ldualvsass2.w	$⊢ φ \to W \in LMod$
9		ldualvsass2.x	$⊢ φ \to X \in K$
10		ldualvsass2.y	$⊢ φ \to Y \in K$
11		ldualvsass2.g	$⊢ φ \to G \in F$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13	2 3 12 4 5 6 8 9 10	ldualsmul	$⊢ φ \to X \underset{˙}{\times} Y = Y \cdot_{R} X$
14	13	oveq1d	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} G = (Y \cdot_{R} X) \underset{˙}{\cdot} G$
15	1 2 3 12 4 7 8 9 10 11	ldualvsass	$⊢ φ \to (Y \cdot_{R} X) \underset{˙}{\cdot} G = X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} G)$
16	14 15	eqtrd	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\cdot} G = X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} G)$

Metamath Proof Explorer