lcosn0

Description: Properties of a linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lincval1.b	$⊢ B = {Base}_{M}$
	lincval1.s	$⊢ S = Scalar (M)$
	lincval1.r	$⊢ R = {Base}_{S}$
	lincval1.f	$⊢ F = \{⟨V, 0_{S}⟩\}$
Assertion	lcosn0	$⊢ (M \in LMod \land V \in B) \to (F \in (R^{\{V\}}) \land {finSupp}_{0_{S}} (F) \land F linC (M) \{V\} = 0_{M})$

Step	Hyp	Ref	Expression
1		lincval1.b	$⊢ B = {Base}_{M}$
2		lincval1.s	$⊢ S = Scalar (M)$
3		lincval1.r	$⊢ R = {Base}_{S}$
4		lincval1.f	$⊢ F = \{⟨V, 0_{S}⟩\}$
5		simpr	$⊢ (M \in LMod \land V \in B) \to V \in B$
6		eqid	$⊢ 0_{S} = 0_{S}$
7	2 3 6	lmod0cl	$⊢ M \in LMod \to 0_{S} \in R$
8	7	adantr	$⊢ (M \in LMod \land V \in B) \to 0_{S} \in R$
9	3	fvexi	$⊢ R \in V$
10	9	a1i	$⊢ (M \in LMod \land V \in B) \to R \in V$
11	4	mapsnop	$⊢ (V \in B \land 0_{S} \in R \land R \in V) \to F \in (R^{\{V\}})$
12	5 8 10 11	syl3anc	$⊢ (M \in LMod \land V \in B) \to F \in (R^{\{V\}})$
13		elmapi	$⊢ F \in (R^{\{V\}}) \to F : \{V\} ⟶ R$
14	12 13	syl	$⊢ (M \in LMod \land V \in B) \to F : \{V\} ⟶ R$
15		snfi	$⊢ \{V\} \in Fin$
16	15	a1i	$⊢ (M \in LMod \land V \in B) \to \{V\} \in Fin$
17		fvex	$⊢ 0_{S} \in V$
18	17	a1i	$⊢ (M \in LMod \land V \in B) \to 0_{S} \in V$
19	14 16 18	fdmfifsupp	$⊢ (M \in LMod \land V \in B) \to {finSupp}_{0_{S}} (F)$
20	1 2 3 4	lincval1	$⊢ (M \in LMod \land V \in B) \to F linC (M) \{V\} = 0_{M}$
21	12 19 20	3jca	$⊢ (M \in LMod \land V \in B) \to (F \in (R^{\{V\}}) \land {finSupp}_{0_{S}} (F) \land F linC (M) \{V\} = 0_{M})$

Metamath Proof Explorer