lfl0sc

Description: The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of ( V X. { .0. } ) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lfl0sc.v	$⊢ V = {Base}_{W}$
2		lfl0sc.d	$⊢ D = Scalar (W)$
3		lfl0sc.f	$⊢ F = LFnl (W)$
4		lfl0sc.k	$⊢ K = {Base}_{D}$
5		lfl0sc.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
6		lfl0sc.o	$⊢ \underset{˙}{0} = 0_{D}$
7		lfl0sc.w	$⊢ φ \to W \in LMod$
8		lfl0sc.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	2	lmodring	$⊢ W \in LMod \to D \in Ring$
14	7 13	syl	$⊢ φ \to D \in Ring$
15	4 6	ring0cl	$⊢ D \in Ring \to \underset{˙}{0} \in K$
16	14 15	syl	$⊢ φ \to \underset{˙}{0} \in K$
17	4 5 6	ringrz	$⊢ (D \in Ring \land k \in K) \to k \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
18	14 17	sylan	$⊢ (φ \land k \in K) \to k \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
19	10 12 16 16 18	caofid1	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{\underset{˙}{0}\}) = V \times \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem lfl0sc

Proof