lflsc0N

Description: The scalar product with the zero functional is the zero functional. (Contributed by NM, 7-Oct-2014) (New usage is discouraged.)

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

Step	Hyp	Ref	Expression
1		lflsc0.v	$⊢ V = {Base}_{W}$
2		lflsc0.d	$⊢ D = Scalar (W)$
3		lflsc0.k	$⊢ K = {Base}_{D}$
4		lflsc0.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
5		lflsc0.o	$⊢ \underset{˙}{0} = 0_{D}$
6		lflsc0.w	$⊢ φ \to W \in LMod$
7		lflsc0.x	$⊢ φ \to X \in K$
8	1	fvexi	$⊢ V \in V$
9	8	a1i	$⊢ φ \to V \in V$
10	2	lmodring	$⊢ W \in LMod \to D \in Ring$
11	6 10	syl	$⊢ φ \to D \in Ring$
12	3 5	ring0cl	$⊢ D \in Ring \to \underset{˙}{0} \in K$
13	11 12	syl	$⊢ φ \to \underset{˙}{0} \in K$
14	9 13 7	ofc12	$⊢ φ \to (V \times \{\underset{˙}{0}\}) {\underset{˙}{\cdot}}_{f} (V \times \{X\}) = V \times \{\underset{˙}{0} \underset{˙}{\cdot} X\}$
15	3 4 5	ringlz	$⊢ (D \in Ring \land X \in K) \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0}$
16	11 7 15	syl2anc	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0}$
17	16	sneqd	$⊢ φ \to \{\underset{˙}{0} \underset{˙}{\cdot} X\} = \{\underset{˙}{0}\}$
18	17	xpeq2d	$⊢ φ \to V \times \{\underset{˙}{0} \underset{˙}{\cdot} X\} = V \times \{\underset{˙}{0}\}$
19	14 18	eqtrd	$⊢ φ \to (V \times \{\underset{˙}{0}\}) {\underset{˙}{\cdot}}_{f} (V \times \{X\}) = V \times \{\underset{˙}{0}\}$

Metamath Proof Explorer