lfl1sc

Description: The (right vector space) scalar product of a functional with one is the functional. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	lfl1sc.v	$⊢ V = {Base}_{W}$
	lfl1sc.d	$⊢ D = Scalar (W)$
	lfl1sc.f	$⊢ F = LFnl (W)$
	lfl1sc.k	$⊢ K = {Base}_{D}$
	lfl1sc.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lfl1sc.i	$⊢ \underset{˙}{1} = 1_{D}$
	lfl1sc.w	$⊢ φ \to W \in LMod$
	lfl1sc.g	$⊢ φ \to G \in F$
Assertion	lfl1sc	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{\underset{˙}{1}\}) = G$

Step	Hyp	Ref	Expression
1		lfl1sc.v	$⊢ V = {Base}_{W}$
2		lfl1sc.d	$⊢ D = Scalar (W)$
3		lfl1sc.f	$⊢ F = LFnl (W)$
4		lfl1sc.k	$⊢ K = {Base}_{D}$
5		lfl1sc.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
6		lfl1sc.i	$⊢ \underset{˙}{1} = 1_{D}$
7		lfl1sc.w	$⊢ φ \to W \in LMod$
8		lfl1sc.g	$⊢ φ \to G \in F$
9	1	fvexi	$⊢ V \in V$
10	9	a1i	$⊢ φ \to V \in V$
11	2 4 1 3	lflf	$⊢ (W \in LMod \land G \in F) \to G : V ⟶ K$
12	7 8 11	syl2anc	$⊢ φ \to G : V ⟶ K$
13	6	fvexi	$⊢ \underset{˙}{1} \in V$
14	13	a1i	$⊢ φ \to \underset{˙}{1} \in V$
15	2	lmodring	$⊢ W \in LMod \to D \in Ring$
16	7 15	syl	$⊢ φ \to D \in Ring$
17	4 5 6	ringridm	$⊢ (D \in Ring \land k \in K) \to k \underset{˙}{\cdot} \underset{˙}{1} = k$
18	16 17	sylan	$⊢ (φ \land k \in K) \to k \underset{˙}{\cdot} \underset{˙}{1} = k$
19	10 12 14 18	caofid0r	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{\underset{˙}{1}\}) = G$

Metamath Proof Explorer