lcoel0

Description: The zero vector is always a linear combination. (Contributed by AV, 12-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

		Ref	Expression
	Assertion	lcoel0	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to 0_{M} \in (M LinCo V)$

Proof

Step	Hyp	Ref	Expression
1		fvex	$⊢ 0_{M} \in V$
2	1	snid	$⊢ 0_{M} \in \{0_{M}\}$
3		oveq2	$⊢ V = \emptyset \to M LinCo V = M LinCo \emptyset$
4		lmodgrp	$⊢ M \in LMod \to M \in Grp$
5		grpmnd	$⊢ M \in Grp \to M \in Mnd$
6		lco0	$⊢ M \in Mnd \to M LinCo \emptyset = \{0_{M}\}$
7	4 5 6	3syl	$⊢ M \in LMod \to M LinCo \emptyset = \{0_{M}\}$
8	7	adantr	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to M LinCo \emptyset = \{0_{M}\}$
9	3 8	sylan9eq	$⊢ (V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to M LinCo V = \{0_{M}\}$
10	2 9	eleqtrrid	$⊢ (V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to 0_{M} \in (M LinCo V)$
11		eqid	$⊢ {Base}_{M} = {Base}_{M}$
12		eqid	$⊢ 0_{M} = 0_{M}$
13	11 12	lmod0vcl	$⊢ M \in LMod \to 0_{M} \in {Base}_{M}$
14	13	adantr	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to 0_{M} \in {Base}_{M}$
15	14	adantl	$⊢ (\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to 0_{M} \in {Base}_{M}$
16		eqid	$⊢ Scalar (M) = Scalar (M)$
17		eqid	$⊢ 0_{Scalar (M)} = 0_{Scalar (M)}$
18		eqidd	$⊢ v = w \to 0_{Scalar (M)} = 0_{Scalar (M)}$
19	18	cbvmptv	$⊢ (v \in V ⟼ 0_{Scalar (M)}) = (w \in V ⟼ 0_{Scalar (M)})$
20		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
21	11 16 17 12 19 20	lcoc0	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to ((v \in V ⟼ 0_{Scalar (M)}) \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ 0_{Scalar (M)})) \land (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M})$
22	21	adantl	$⊢ (\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to ((v \in V ⟼ 0_{Scalar (M)}) \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ 0_{Scalar (M)})) \land (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M})$
23		simpl	$⊢ ((v \in V ⟼ 0_{Scalar (M)}) \in ({Base}_{Scalar (M)}^{V}) \land (\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M}))) \to (v \in V ⟼ 0_{Scalar (M)}) \in ({Base}_{Scalar (M)}^{V})$
24		breq1	$⊢ s = (v \in V ⟼ 0_{Scalar (M)}) \to ({finSupp}_{0_{Scalar (M)}} (s) \leftrightarrow {finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ 0_{Scalar (M)})))$
25		oveq1	$⊢ s = (v \in V ⟼ 0_{Scalar (M)}) \to s linC (M) V = (v \in V ⟼ 0_{Scalar (M)}) linC (M) V$
26	25	eqeq2d	$⊢ s = (v \in V ⟼ 0_{Scalar (M)}) \to (0_{M} = s linC (M) V \leftrightarrow 0_{M} = (v \in V ⟼ 0_{Scalar (M)}) linC (M) V)$
27		eqcom	$⊢ 0_{M} = (v \in V ⟼ 0_{Scalar (M)}) linC (M) V \leftrightarrow (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M}$
28	26 27	bitrdi	$⊢ s = (v \in V ⟼ 0_{Scalar (M)}) \to (0_{M} = s linC (M) V \leftrightarrow (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M})$
29	24 28	anbi12d	$⊢ s = (v \in V ⟼ 0_{Scalar (M)}) \to (({finSupp}_{0_{Scalar (M)}} (s) \land 0_{M} = s linC (M) V) \leftrightarrow ({finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ 0_{Scalar (M)})) \land (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M}))$
30	29	adantl	$⊢ (((v \in V ⟼ 0_{Scalar (M)}) \in ({Base}_{Scalar (M)}^{V}) \land (\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M}))) \land s = (v \in V ⟼ 0_{Scalar (M)})) \to (({finSupp}_{0_{Scalar (M)}} (s) \land 0_{M} = s linC (M) V) \leftrightarrow ({finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ 0_{Scalar (M)})) \land (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M}))$
31	23 30	rspcedv	$⊢ ((v \in V ⟼ 0_{Scalar (M)}) \in ({Base}_{Scalar (M)}^{V}) \land (\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M}))) \to (({finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ 0_{Scalar (M)})) \land (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land 0_{M} = s linC (M) V))$
32	31	ex	$⊢ (v \in V ⟼ 0_{Scalar (M)}) \in ({Base}_{Scalar (M)}^{V}) \to ((\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to (({finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ 0_{Scalar (M)})) \land (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land 0_{M} = s linC (M) V)))$
33	32	com23	$⊢ (v \in V ⟼ 0_{Scalar (M)}) \in ({Base}_{Scalar (M)}^{V}) \to (({finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ 0_{Scalar (M)})) \land (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M}) \to ((\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land 0_{M} = s linC (M) V)))$
34	33	3impib	$⊢ ((v \in V ⟼ 0_{Scalar (M)}) \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ 0_{Scalar (M)})) \land (v \in V ⟼ 0_{Scalar (M)}) linC (M) V = 0_{M}) \to ((\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land 0_{M} = s linC (M) V))$
35	22 34	mpcom	$⊢ (\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land 0_{M} = s linC (M) V)$
36	11 16 20	lcoval	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (0_{M} \in (M LinCo V) \leftrightarrow (0_{M} \in {Base}_{M} \land \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land 0_{M} = s linC (M) V)))$
37	36	adantl	$⊢ (\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to (0_{M} \in (M LinCo V) \leftrightarrow (0_{M} \in {Base}_{M} \land \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land 0_{M} = s linC (M) V)))$
38	15 35 37	mpbir2and	$⊢ (\neg V = \emptyset \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to 0_{M} \in (M LinCo V)$
39	10 38	pm2.61ian	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to 0_{M} \in (M LinCo V)$

Metamath Proof Explorer

Theorem lcoel0

Proof