linindslinci

Description: The implications of being a linearly independent subset and a linear combination of this subset being 0. (Contributed by AV, 24-Apr-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	islininds.b	$⊢ B = {Base}_{M}$
	islininds.z	$⊢ Z = 0_{M}$
	islininds.r	$⊢ R = Scalar (M)$
	islininds.e	$⊢ E = {Base}_{R}$
	islininds.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	linindslinci	$⊢ (S linIndS M \land (F \in (E^{S}) \land {finSupp}_{\underset{˙}{0}} (F) \land F linC (M) S = Z)) \to \forall x \in S F (x) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		islininds.b	$⊢ B = {Base}_{M}$
2		islininds.z	$⊢ Z = 0_{M}$
3		islininds.r	$⊢ R = Scalar (M)$
4		islininds.e	$⊢ E = {Base}_{R}$
5		islininds.0	$⊢ \underset{˙}{0} = 0_{R}$
6	1 2 3 4 5	linindsi	$⊢ S linIndS M \to (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))$
7		breq1	$⊢ f = F \to ({finSupp}_{\underset{˙}{0}} (f) \leftrightarrow {finSupp}_{\underset{˙}{0}} (F))$
8		oveq1	$⊢ f = F \to f linC (M) S = F linC (M) S$
9	8	eqeq1d	$⊢ f = F \to (f linC (M) S = Z \leftrightarrow F linC (M) S = Z)$
10	7 9	anbi12d	$⊢ f = F \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (F) \land F linC (M) S = Z))$
11		fveq1	$⊢ f = F \to f (x) = F (x)$
12	11	eqeq1d	$⊢ f = F \to (f (x) = \underset{˙}{0} \leftrightarrow F (x) = \underset{˙}{0})$
13	12	ralbidv	$⊢ f = F \to (\forall x \in S f (x) = \underset{˙}{0} \leftrightarrow \forall x \in S F (x) = \underset{˙}{0})$
14	10 13	imbi12d	$⊢ f = F \to ((({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (F) \land F linC (M) S = Z) \to \forall x \in S F (x) = \underset{˙}{0}))$
15	14	rspcv	$⊢ F \in (E^{S}) \to (\forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to (({finSupp}_{\underset{˙}{0}} (F) \land F linC (M) S = Z) \to \forall x \in S F (x) = \underset{˙}{0}))$
16	15	com23	$⊢ F \in (E^{S}) \to (({finSupp}_{\underset{˙}{0}} (F) \land F linC (M) S = Z) \to (\forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to \forall x \in S F (x) = \underset{˙}{0}))$
17	16	3impib	$⊢ (F \in (E^{S}) \land {finSupp}_{\underset{˙}{0}} (F) \land F linC (M) S = Z) \to (\forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to \forall x \in S F (x) = \underset{˙}{0})$
18	17	com12	$⊢ \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to ((F \in (E^{S}) \land {finSupp}_{\underset{˙}{0}} (F) \land F linC (M) S = Z) \to \forall x \in S F (x) = \underset{˙}{0})$
19	6 18	simpl2im	$⊢ S linIndS M \to ((F \in (E^{S}) \land {finSupp}_{\underset{˙}{0}} (F) \land F linC (M) S = Z) \to \forall x \in S F (x) = \underset{˙}{0})$
20	19	imp	$⊢ (S linIndS M \land (F \in (E^{S}) \land {finSupp}_{\underset{˙}{0}} (F) \land F linC (M) S = Z)) \to \forall x \in S F (x) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem linindslinci

Proof