isldepslvec2

Description: Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 holds, so that both definitions are equivalent (see theorem 1.6 in Roman p. 46 and the note in Roman p. 112: if a nontrivial linear combination of elements (where not all of the coefficients are 0) in an R-vector space is 0, then and only then each of the elements is a linear combination of the others. (Contributed by AV, 30-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	islindeps2.b	$⊢ B = {Base}_{M}$
	islindeps2.z	$⊢ Z = 0_{M}$
	islindeps2.r	$⊢ R = Scalar (M)$
	islindeps2.e	$⊢ E = {Base}_{R}$
	islindeps2.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	isldepslvec2	$⊢ (M \in LVec \land S \in 𝒫 B) \to (\exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow S linDepS M)$

Proof

Step	Hyp	Ref	Expression
1		islindeps2.b	$⊢ B = {Base}_{M}$
2		islindeps2.z	$⊢ Z = 0_{M}$
3		islindeps2.r	$⊢ R = Scalar (M)$
4		islindeps2.e	$⊢ E = {Base}_{R}$
5		islindeps2.0	$⊢ \underset{˙}{0} = 0_{R}$
6		lveclmod	$⊢ M \in LVec \to M \in LMod$
7	6	adantr	$⊢ (M \in LVec \land S \in 𝒫 B) \to M \in LMod$
8		simpr	$⊢ (M \in LVec \land S \in 𝒫 B) \to S \in 𝒫 B$
9	3	lvecdrng	$⊢ M \in LVec \to R \in DivRing$
10		drngnzr	$⊢ R \in DivRing \to R \in NzRing$
11	9 10	syl	$⊢ M \in LVec \to R \in NzRing$
12	11	adantr	$⊢ (M \in LVec \land S \in 𝒫 B) \to R \in NzRing$
13	1 2 3 4 5	islindeps2	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (\exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \to S linDepS M)$
14	7 8 12 13	syl3anc	$⊢ (M \in LVec \land S \in 𝒫 B) \to (\exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \to S linDepS M)$
15	1 2 3 4 5	islindeps	$⊢ (M \in LVec \land S \in 𝒫 B) \to (S linDepS M \leftrightarrow \exists g \in (E^{S}) ({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z \land \exists s \in S g (s) \neq \underset{˙}{0}))$
16		df-3an	$⊢ ({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z \land \exists s \in S g (s) \neq \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land \exists s \in S g (s) \neq \underset{˙}{0})$
17		r19.42v	$⊢ \exists s \in S (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land \exists s \in S g (s) \neq \underset{˙}{0})$
18	16 17	bitr4i	$⊢ ({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z \land \exists s \in S g (s) \neq \underset{˙}{0}) \leftrightarrow \exists s \in S (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})$
19	18	rexbii	$⊢ \exists g \in (E^{S}) ({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z \land \exists s \in S g (s) \neq \underset{˙}{0}) \leftrightarrow \exists g \in (E^{S}) \exists s \in S (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})$
20		rexcom	$⊢ \exists g \in (E^{S}) \exists s \in S (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}) \leftrightarrow \exists s \in S \exists g \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})$
21	19 20	bitri	$⊢ \exists g \in (E^{S}) ({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z \land \exists s \in S g (s) \neq \underset{˙}{0}) \leftrightarrow \exists s \in S \exists g \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})$
22		simplr	$⊢ ((M \in LVec \land S \in 𝒫 B) \land s \in S) \to S \in 𝒫 B$
23	6	ad2antrr	$⊢ ((M \in LVec \land S \in 𝒫 B) \land s \in S) \to M \in LMod$
24		simpr	$⊢ ((M \in LVec \land S \in 𝒫 B) \land s \in S) \to s \in S$
25	22 23 24	3jca	$⊢ ((M \in LVec \land S \in 𝒫 B) \land s \in S) \to (S \in 𝒫 B \land M \in LMod \land s \in S)$
26	25	ad2antrr	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to (S \in 𝒫 B \land M \in LMod \land s \in S)$
27		simplr	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to g \in (E^{S})$
28		elmapi	$⊢ g \in (E^{S}) \to g : S ⟶ E$
29		ffvelrn	$⊢ (g : S ⟶ E \land s \in S) \to g (s) \in E$
30	28 24 29	syl2anr	$⊢ (((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \to g (s) \in E$
31		simpr	$⊢ (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}) \to g (s) \neq \underset{˙}{0}$
32	30 31	anim12i	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to (g (s) \in E \land g (s) \neq \underset{˙}{0})$
33	9	ad2antrr	$⊢ ((M \in LVec \land S \in 𝒫 B) \land s \in S) \to R \in DivRing$
34	33	ad2antrr	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to R \in DivRing$
35		eqid	$⊢ Unit (R) = Unit (R)$
36	4 35 5	drngunit	$⊢ R \in DivRing \to (g (s) \in Unit (R) \leftrightarrow (g (s) \in E \land g (s) \neq \underset{˙}{0}))$
37	34 36	syl	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to (g (s) \in Unit (R) \leftrightarrow (g (s) \in E \land g (s) \neq \underset{˙}{0}))$
38	32 37	mpbird	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to g (s) \in Unit (R)$
39		simpll	$⊢ (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}) \to {finSupp}_{\underset{˙}{0}} (g)$
40	39	adantl	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} (g)$
41		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
42		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
43		eqid	$⊢ \cdot_{R} = \cdot_{R}$
44		eqid	$⊢ (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) = (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z))$
45	1 3 4 35 5 2 41 42 43 44	lincresunit2	$⊢ ((S \in 𝒫 B \land M \in LMod \land s \in S) \land (g \in (E^{S}) \land g (s) \in Unit (R) \land {finSupp}_{\underset{˙}{0}} (g))) \to {finSupp}_{\underset{˙}{0}} ((z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)))$
46	26 27 38 40 45	syl13anc	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} ((z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)))$
47		simpll	$⊢ ((M \in LVec \land S \in 𝒫 B) \land s \in S) \to M \in LVec$
48	22 47 24	3jca	$⊢ ((M \in LVec \land S \in 𝒫 B) \land s \in S) \to (S \in 𝒫 B \land M \in LVec \land s \in S)$
49	48	ad2antrr	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to (S \in 𝒫 B \land M \in LVec \land s \in S)$
50		simprr	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to g (s) \neq \underset{˙}{0}$
51		simplr	$⊢ (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}) \to g linC (M) S = Z$
52	51	adantl	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to g linC (M) S = Z$
53		fveq2	$⊢ z = y \to g (z) = g (y)$
54	53	oveq2d	$⊢ z = y \to {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z) = {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (y)$
55	54	cbvmptv	$⊢ (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) = (y \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (y))$
56	1 3 4 35 5 2 41 42 43 55	lincreslvec3	$⊢ ((S \in 𝒫 B \land M \in LVec \land s \in S) \land (g \in (E^{S}) \land g (s) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (g)) \land g linC (M) S = Z) \to (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) linC (M) (S ∖ \{s\}) = s$
57	49 27 50 40 52 56	syl131anc	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) linC (M) (S ∖ \{s\}) = s$
58	1 3 4 35 5 2 41 42 43 44	lincresunit1	$⊢ ((S \in 𝒫 B \land M \in LMod \land s \in S) \land (g \in (E^{S}) \land g (s) \in Unit (R))) \to (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) \in (E^{(S ∖ \{s\})})$
59	26 27 38 58	syl12anc	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) \in (E^{(S ∖ \{s\})})$
60		breq1	$⊢ f = (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) \to ({finSupp}_{\underset{˙}{0}} (f) \leftrightarrow {finSupp}_{\underset{˙}{0}} ((z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z))))$
61		oveq1	$⊢ f = (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) \to f linC (M) (S ∖ \{s\}) = (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) linC (M) (S ∖ \{s\})$
62	61	eqeq1d	$⊢ f = (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) \to (f linC (M) (S ∖ \{s\}) = s \leftrightarrow (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) linC (M) (S ∖ \{s\}) = s)$
63	60 62	anbi12d	$⊢ f = (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow ({finSupp}_{\underset{˙}{0}} ((z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z))) \land (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) linC (M) (S ∖ \{s\}) = s))$
64	63	adantl	$⊢ (((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \land f = (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z))) \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow ({finSupp}_{\underset{˙}{0}} ((z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z))) \land (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) linC (M) (S ∖ \{s\}) = s))$
65	59 64	rspcedv	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to (({finSupp}_{\underset{˙}{0}} ((z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z))) \land (z \in (S ∖ \{s\}) ⟼ {inv}_{r} (R) ({inv}_{g} (R) (g (s))) \cdot_{R} g (z)) linC (M) (S ∖ \{s\}) = s) \to \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s))$
66	46 57 65	mp2and	$⊢ ((((M \in LVec \land S \in 𝒫 B) \land s \in S) \land g \in (E^{S})) \land (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})) \to \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)$
67	66	rexlimdva2	$⊢ ((M \in LVec \land S \in 𝒫 B) \land s \in S) \to (\exists g \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}) \to \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s))$
68	67	reximdva	$⊢ (M \in LVec \land S \in 𝒫 B) \to (\exists s \in S \exists g \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}) \to \exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s))$
69	21 68	syl5bi	$⊢ (M \in LVec \land S \in 𝒫 B) \to (\exists g \in (E^{S}) ({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z \land \exists s \in S g (s) \neq \underset{˙}{0}) \to \exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s))$
70	15 69	sylbid	$⊢ (M \in LVec \land S \in 𝒫 B) \to (S linDepS M \to \exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s))$
71	14 70	impbid	$⊢ (M \in LVec \land S \in 𝒫 B) \to (\exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow S linDepS M)$

Metamath Proof Explorer

Theorem isldepslvec2

Proof