lflvsass

Description: Associative law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014)

	Ref	Expression
Hypotheses	lflass.v	$⊢ V = {Base}_{W}$
	lflass.r	$⊢ R = Scalar (W)$
	lflass.k	$⊢ K = {Base}_{R}$
	lflass.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	lflass.f	$⊢ F = LFnl (W)$
	lflass.w	$⊢ φ \to W \in LMod$
	lflass.x	$⊢ φ \to X \in K$
	lflass.y	$⊢ φ \to Y \in K$
	lflass.g	$⊢ φ \to G \in F$
Assertion	lflvsass	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{X \underset{˙}{\cdot} Y\}) = (G {\underset{˙}{\cdot}}_{f} (V \times \{X\})) {\underset{˙}{\cdot}}_{f} (V \times \{Y\})$

Proof

Step	Hyp	Ref	Expression
1		lflass.v	$⊢ V = {Base}_{W}$
2		lflass.r	$⊢ R = Scalar (W)$
3		lflass.k	$⊢ K = {Base}_{R}$
4		lflass.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		lflass.f	$⊢ F = LFnl (W)$
6		lflass.w	$⊢ φ \to W \in LMod$
7		lflass.x	$⊢ φ \to X \in K$
8		lflass.y	$⊢ φ \to Y \in K$
9		lflass.g	$⊢ φ \to G \in F$
10	1	fvexi	$⊢ V \in V$
11	10	a1i	$⊢ φ \to V \in V$
12	2 3 1 5	lflf	$⊢ (W \in LMod \land G \in F) \to G : V ⟶ K$
13	6 9 12	syl2anc	$⊢ φ \to G : V ⟶ K$
14		fconst6g	$⊢ X \in K \to (V \times \{X\}) : V ⟶ K$
15	7 14	syl	$⊢ φ \to (V \times \{X\}) : V ⟶ K$
16		fconst6g	$⊢ Y \in K \to (V \times \{Y\}) : V ⟶ K$
17	8 16	syl	$⊢ φ \to (V \times \{Y\}) : V ⟶ K$
18	2	lmodring	$⊢ W \in LMod \to R \in Ring$
19	6 18	syl	$⊢ φ \to R \in Ring$
20	3 4	ringass	$⊢ (R \in Ring \land (x \in K \land y \in K \land z \in K)) \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)$
21	19 20	sylan	$⊢ (φ \land (x \in K \land y \in K \land z \in K)) \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)$
22	11 13 15 17 21	caofass	$⊢ φ \to (G {\underset{˙}{\cdot}}_{f} (V \times \{X\})) {\underset{˙}{\cdot}}_{f} (V \times \{Y\}) = G {\underset{˙}{\cdot}}_{f} ((V \times \{X\}) {\underset{˙}{\cdot}}_{f} (V \times \{Y\}))$
23	11 7 8	ofc12	$⊢ φ \to (V \times \{X\}) {\underset{˙}{\cdot}}_{f} (V \times \{Y\}) = V \times \{X \underset{˙}{\cdot} Y\}$
24	23	oveq2d	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} ((V \times \{X\}) {\underset{˙}{\cdot}}_{f} (V \times \{Y\})) = G {\underset{˙}{\cdot}}_{f} (V \times \{X \underset{˙}{\cdot} Y\})$
25	22 24	eqtr2d	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{X \underset{˙}{\cdot} Y\}) = (G {\underset{˙}{\cdot}}_{f} (V \times \{X\})) {\underset{˙}{\cdot}}_{f} (V \times \{Y\})$

Metamath Proof Explorer

Theorem lflvsass

Proof