Theorem 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={\mathrm{Base}}_W$$
	lfl1sc.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
	lfl1sc.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lfl1sc.k	$$⊢K={\mathrm{Base}}_D$$
	lfl1sc.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	lfl1sc.i	$$⊢\underset{\dot{}}{1}=1_D$$
	lfl1sc.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lfl1sc.g	$$⊢\phi \to G\in F$$
Assertion	lfl1sc	$$⊢\phi \to G{\underset{\dot{}}{·}}_f\left(V\times \left\{\underset{\dot{}}{1}\right\}\right)=G$$

Proof

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