lcoc0

Description: Properties of a linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lincvalsc0.b	$⊢ B = {Base}_{M}$
	lincvalsc0.s	$⊢ S = Scalar (M)$
	lincvalsc0.0	$⊢ \underset{˙}{0} = 0_{S}$
	lincvalsc0.z	$⊢ Z = 0_{M}$
	lincvalsc0.f	$⊢ F = (x \in V ⟼ \underset{˙}{0})$
	lcoc0.r	$⊢ R = {Base}_{S}$
Assertion	lcoc0	$⊢ (M \in LMod \land V \in 𝒫 B) \to (F \in (R^{V}) \land {finSupp}_{\underset{˙}{0}} (F) \land F linC (M) V = Z)$

Proof

Step	Hyp	Ref	Expression
1		lincvalsc0.b	$⊢ B = {Base}_{M}$
2		lincvalsc0.s	$⊢ S = Scalar (M)$
3		lincvalsc0.0	$⊢ \underset{˙}{0} = 0_{S}$
4		lincvalsc0.z	$⊢ Z = 0_{M}$
5		lincvalsc0.f	$⊢ F = (x \in V ⟼ \underset{˙}{0})$
6		lcoc0.r	$⊢ R = {Base}_{S}$
7	2 6 3	lmod0cl	$⊢ M \in LMod \to \underset{˙}{0} \in R$
8	7	ad2antrr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in V) \to \underset{˙}{0} \in R$
9	8 5	fmptd	$⊢ (M \in LMod \land V \in 𝒫 B) \to F : V ⟶ R$
10	6	fvexi	$⊢ R \in V$
11	10	a1i	$⊢ M \in LMod \to R \in V$
12		elmapg	$⊢ (R \in V \land V \in 𝒫 B) \to (F \in (R^{V}) \leftrightarrow F : V ⟶ R)$
13	11 12	sylan	$⊢ (M \in LMod \land V \in 𝒫 B) \to (F \in (R^{V}) \leftrightarrow F : V ⟶ R)$
14	9 13	mpbird	$⊢ (M \in LMod \land V \in 𝒫 B) \to F \in (R^{V})$
15		eqidd	$⊢ x = v \to \underset{˙}{0} = \underset{˙}{0}$
16	15	cbvmptv	$⊢ (x \in V ⟼ \underset{˙}{0}) = (v \in V ⟼ \underset{˙}{0})$
17	5 16	eqtri	$⊢ F = (v \in V ⟼ \underset{˙}{0})$
18		simpr	$⊢ (M \in LMod \land V \in 𝒫 B) \to V \in 𝒫 B$
19	3	fvexi	$⊢ \underset{˙}{0} \in V$
20	19	a1i	$⊢ (M \in LMod \land V \in 𝒫 B) \to \underset{˙}{0} \in V$
21	19	a1i	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to \underset{˙}{0} \in V$
22	17 18 20 21	mptsuppd	$⊢ (M \in LMod \land V \in 𝒫 B) \to F supp \underset{˙}{0} = \{v \in V \| \underset{˙}{0} \neq \underset{˙}{0}\}$
23		neirr	$⊢ \neg \underset{˙}{0} \neq \underset{˙}{0}$
24	23	a1i	$⊢ (M \in LMod \land V \in 𝒫 B) \to \neg \underset{˙}{0} \neq \underset{˙}{0}$
25	24	ralrimivw	$⊢ (M \in LMod \land V \in 𝒫 B) \to \forall v \in V \neg \underset{˙}{0} \neq \underset{˙}{0}$
26		rabeq0	$⊢ \{v \in V \| \underset{˙}{0} \neq \underset{˙}{0}\} = \emptyset \leftrightarrow \forall v \in V \neg \underset{˙}{0} \neq \underset{˙}{0}$
27	25 26	sylibr	$⊢ (M \in LMod \land V \in 𝒫 B) \to \{v \in V \| \underset{˙}{0} \neq \underset{˙}{0}\} = \emptyset$
28		0fin	$⊢ \emptyset \in Fin$
29	28	a1i	$⊢ (M \in LMod \land V \in 𝒫 B) \to \emptyset \in Fin$
30	27 29	eqeltrd	$⊢ (M \in LMod \land V \in 𝒫 B) \to \{v \in V \| \underset{˙}{0} \neq \underset{˙}{0}\} \in Fin$
31	22 30	eqeltrd	$⊢ (M \in LMod \land V \in 𝒫 B) \to F supp \underset{˙}{0} \in Fin$
32	5	funmpt2	$⊢ Fun F$
33	32	a1i	$⊢ (M \in LMod \land V \in 𝒫 B) \to Fun F$
34		funisfsupp	$⊢ (Fun F \land F \in (R^{V}) \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} (F) \leftrightarrow F supp \underset{˙}{0} \in Fin)$
35	33 14 20 34	syl3anc	$⊢ (M \in LMod \land V \in 𝒫 B) \to ({finSupp}_{\underset{˙}{0}} (F) \leftrightarrow F supp \underset{˙}{0} \in Fin)$
36	31 35	mpbird	$⊢ (M \in LMod \land V \in 𝒫 B) \to {finSupp}_{\underset{˙}{0}} (F)$
37	1 2 3 4 5	lincvalsc0	$⊢ (M \in LMod \land V \in 𝒫 B) \to F linC (M) V = Z$
38	14 36 37	3jca	$⊢ (M \in LMod \land V \in 𝒫 B) \to (F \in (R^{V}) \land {finSupp}_{\underset{˙}{0}} (F) \land F linC (M) V = Z)$

Metamath Proof Explorer

Theorem lcoc0

Proof