lfl0f

Description: The zero function is a functional. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	lfl0f.d	$⊢ D = Scalar (W)$
	lfl0f.o	$⊢ \underset{˙}{0} = 0_{D}$
	lfl0f.v	$⊢ V = {Base}_{W}$
	lfl0f.f	$⊢ F = LFnl (W)$
Assertion	lfl0f	$⊢ W \in LMod \to V \times \{\underset{˙}{0}\} \in F$

Proof

Step	Hyp	Ref	Expression
1		lfl0f.d	$⊢ D = Scalar (W)$
2		lfl0f.o	$⊢ \underset{˙}{0} = 0_{D}$
3		lfl0f.v	$⊢ V = {Base}_{W}$
4		lfl0f.f	$⊢ F = LFnl (W)$
5	2	fvexi	$⊢ \underset{˙}{0} \in V$
6	5	fconst	$⊢ (V \times \{\underset{˙}{0}\}) : V ⟶ \{\underset{˙}{0}\}$
7		eqid	$⊢ {Base}_{D} = {Base}_{D}$
8	1 7 2	lmod0cl	$⊢ W \in LMod \to \underset{˙}{0} \in {Base}_{D}$
9	8	snssd	$⊢ W \in LMod \to \{\underset{˙}{0}\} \subseteq {Base}_{D}$
10		fss	$⊢ ((V \times \{\underset{˙}{0}\}) : V ⟶ \{\underset{˙}{0}\} \land \{\underset{˙}{0}\} \subseteq {Base}_{D}) \to (V \times \{\underset{˙}{0}\}) : V ⟶ {Base}_{D}$
11	6 9 10	sylancr	$⊢ W \in LMod \to (V \times \{\underset{˙}{0}\}) : V ⟶ {Base}_{D}$
12	1	lmodring	$⊢ W \in LMod \to D \in Ring$
13	12	ad2antrr	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to D \in Ring$
14		simplrl	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to r \in {Base}_{D}$
15		eqid	$⊢ \cdot_{D} = \cdot_{D}$
16	7 15 2	ringrz	$⊢ (D \in Ring \land r \in {Base}_{D}) \to r \cdot_{D} \underset{˙}{0} = \underset{˙}{0}$
17	13 14 16	syl2anc	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to r \cdot_{D} \underset{˙}{0} = \underset{˙}{0}$
18	17	oveq1d	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to (r \cdot_{D} \underset{˙}{0}) +_{D} \underset{˙}{0} = \underset{˙}{0} +_{D} \underset{˙}{0}$
19		ringgrp	$⊢ D \in Ring \to D \in Grp$
20	13 19	syl	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to D \in Grp$
21	7 2	grpidcl	$⊢ D \in Grp \to \underset{˙}{0} \in {Base}_{D}$
22		eqid	$⊢ +_{D} = +_{D}$
23	7 22 2	grplid	$⊢ (D \in Grp \land \underset{˙}{0} \in {Base}_{D}) \to \underset{˙}{0} +_{D} \underset{˙}{0} = \underset{˙}{0}$
24	20 21 23	syl2anc2	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to \underset{˙}{0} +_{D} \underset{˙}{0} = \underset{˙}{0}$
25	18 24	eqtrd	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to (r \cdot_{D} \underset{˙}{0}) +_{D} \underset{˙}{0} = \underset{˙}{0}$
26		simplrr	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to x \in V$
27	5	fvconst2	$⊢ x \in V \to (V \times \{\underset{˙}{0}\}) (x) = \underset{˙}{0}$
28	26 27	syl	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to (V \times \{\underset{˙}{0}\}) (x) = \underset{˙}{0}$
29	28	oveq2d	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to r \cdot_{D} (V \times \{\underset{˙}{0}\}) (x) = r \cdot_{D} \underset{˙}{0}$
30	5	fvconst2	$⊢ y \in V \to (V \times \{\underset{˙}{0}\}) (y) = \underset{˙}{0}$
31	30	adantl	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to (V \times \{\underset{˙}{0}\}) (y) = \underset{˙}{0}$
32	29 31	oveq12d	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to (r \cdot_{D} (V \times \{\underset{˙}{0}\}) (x)) +_{D} (V \times \{\underset{˙}{0}\}) (y) = (r \cdot_{D} \underset{˙}{0}) +_{D} \underset{˙}{0}$
33		simpll	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to W \in LMod$
34		eqid	$⊢ \cdot_{W} = \cdot_{W}$
35	3 1 34 7	lmodvscl	$⊢ (W \in LMod \land r \in {Base}_{D} \land x \in V) \to r \cdot_{W} x \in V$
36	33 14 26 35	syl3anc	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to r \cdot_{W} x \in V$
37		simpr	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to y \in V$
38		eqid	$⊢ +_{W} = +_{W}$
39	3 38	lmodvacl	$⊢ (W \in LMod \land r \cdot_{W} x \in V \land y \in V) \to (r \cdot_{W} x) +_{W} y \in V$
40	33 36 37 39	syl3anc	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to (r \cdot_{W} x) +_{W} y \in V$
41	5	fvconst2	$⊢ (r \cdot_{W} x) +_{W} y \in V \to (V \times \{\underset{˙}{0}\}) ((r \cdot_{W} x) +_{W} y) = \underset{˙}{0}$
42	40 41	syl	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to (V \times \{\underset{˙}{0}\}) ((r \cdot_{W} x) +_{W} y) = \underset{˙}{0}$
43	25 32 42	3eqtr4rd	$⊢ ((W \in LMod \land (r \in {Base}_{D} \land x \in V)) \land y \in V) \to (V \times \{\underset{˙}{0}\}) ((r \cdot_{W} x) +_{W} y) = (r \cdot_{D} (V \times \{\underset{˙}{0}\}) (x)) +_{D} (V \times \{\underset{˙}{0}\}) (y)$
44	43	ralrimiva	$⊢ (W \in LMod \land (r \in {Base}_{D} \land x \in V)) \to \forall y \in V (V \times \{\underset{˙}{0}\}) ((r \cdot_{W} x) +_{W} y) = (r \cdot_{D} (V \times \{\underset{˙}{0}\}) (x)) +_{D} (V \times \{\underset{˙}{0}\}) (y)$
45	44	ralrimivva	$⊢ W \in LMod \to \forall r \in {Base}_{D} \forall x \in V \forall y \in V (V \times \{\underset{˙}{0}\}) ((r \cdot_{W} x) +_{W} y) = (r \cdot_{D} (V \times \{\underset{˙}{0}\}) (x)) +_{D} (V \times \{\underset{˙}{0}\}) (y)$
46	3 38 1 34 7 22 15 4	islfl	$⊢ W \in LMod \to (V \times \{\underset{˙}{0}\} \in F \leftrightarrow ((V \times \{\underset{˙}{0}\}) : V ⟶ {Base}_{D} \land \forall r \in {Base}_{D} \forall x \in V \forall y \in V (V \times \{\underset{˙}{0}\}) ((r \cdot_{W} x) +_{W} y) = (r \cdot_{D} (V \times \{\underset{˙}{0}\}) (x)) +_{D} (V \times \{\underset{˙}{0}\}) (y)))$
47	11 45 46	mpbir2and	$⊢ W \in LMod \to V \times \{\underset{˙}{0}\} \in F$

Metamath Proof Explorer

Theorem lfl0f

Proof