islindeps2

Description: Conditions for being a linearly dependent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-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	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)$

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		id	$⊢ (M \in LMod \land S \in 𝒫 B) \to (M \in LMod \land S \in 𝒫 B)$
7	6	3adant3	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (M \in LMod \land S \in 𝒫 B)$
8	7	ad3antrrr	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to (M \in LMod \land S \in 𝒫 B)$
9		nzrring	$⊢ R \in NzRing \to R \in Ring$
10		eqid	$⊢ 1_{R} = 1_{R}$
11	4 10	ringidcl	$⊢ R \in Ring \to 1_{R} \in E$
12	9 11	syl	$⊢ R \in NzRing \to 1_{R} \in E$
13	12	3ad2ant3	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to 1_{R} \in E$
14	13	ad3antrrr	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to 1_{R} \in E$
15		simpllr	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to s \in S$
16		simplr	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to f \in (E^{(S ∖ \{s\})})$
17	14 15 16	3jca	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to (1_{R} \in E \land s \in S \land f \in (E^{(S ∖ \{s\})}))$
18		simprl	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to {finSupp}_{\underset{˙}{0}} (f)$
19		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
20		eqid	$⊢ (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z)))$
21	1 3 4 5 2 19 20	lincext2	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (1_{R} \in E \land s \in S \land f \in (E^{(S ∖ \{s\})})) \land {finSupp}_{\underset{˙}{0}} (f)) \to {finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))))$
22	8 17 18 21	syl3anc	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to {finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))))$
23		simpl1	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to M \in LMod$
24		elelpwi	$⊢ (s \in S \land S \in 𝒫 B) \to s \in B$
25	24	expcom	$⊢ S \in 𝒫 B \to (s \in S \to s \in B)$
26	25	3ad2ant2	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (s \in S \to s \in B)$
27	26	imp	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to s \in B$
28		eqid	$⊢ \cdot_{M} = \cdot_{M}$
29	1 3 28 10	lmodvs1	$⊢ (M \in LMod \land s \in B) \to 1_{R} \cdot_{M} s = s$
30	23 27 29	syl2anc	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to 1_{R} \cdot_{M} s = s$
31	30	adantr	$⊢ (((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \to 1_{R} \cdot_{M} s = s$
32		id	$⊢ f linC (M) (S ∖ \{s\}) = s \to f linC (M) (S ∖ \{s\}) = s$
33	32	eqcomd	$⊢ f linC (M) (S ∖ \{s\}) = s \to s = f linC (M) (S ∖ \{s\})$
34	33	adantl	$⊢ ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \to s = f linC (M) (S ∖ \{s\})$
35	31 34	sylan9eq	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to 1_{R} \cdot_{M} s = f linC (M) (S ∖ \{s\})$
36	1 3 4 5 2 19 20	lincext3	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (1_{R} \in E \land s \in S \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land 1_{R} \cdot_{M} s = f linC (M) (S ∖ \{s\}))) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) linC (M) S = Z$
37	8 17 18 35 36	syl112anc	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) linC (M) S = Z$
38	22 37	jca	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to ({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z)))) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) linC (M) S = Z)$
39		eqidd	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z)))$
40		iftrue	$⊢ z = s \to if (z = s, {inv}_{g} (R) (1_{R}), f (z)) = {inv}_{g} (R) (1_{R})$
41	40	adantl	$⊢ (((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land z = s) \to if (z = s, {inv}_{g} (R) (1_{R}), f (z)) = {inv}_{g} (R) (1_{R})$
42		simpr	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to s \in S$
43		fvexd	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to {inv}_{g} (R) (1_{R}) \in V$
44	39 41 42 43	fvmptd	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) (s) = {inv}_{g} (R) (1_{R})$
45		nzrneg1ne0	$⊢ R \in NzRing \to {inv}_{g} (R) (1_{R}) \neq 0_{R}$
46	5	a1i	$⊢ R \in NzRing \to \underset{˙}{0} = 0_{R}$
47	45 46	neeqtrrd	$⊢ R \in NzRing \to {inv}_{g} (R) (1_{R}) \neq \underset{˙}{0}$
48	47	3ad2ant3	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to {inv}_{g} (R) (1_{R}) \neq \underset{˙}{0}$
49	48	adantr	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to {inv}_{g} (R) (1_{R}) \neq \underset{˙}{0}$
50	44 49	eqnetrd	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) (s) \neq \underset{˙}{0}$
51	50	adantr	$⊢ (((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) (s) \neq \underset{˙}{0}$
52	51	adantr	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) (s) \neq \underset{˙}{0}$
53	1 3 4 5 2 19 20	lincext1	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (1_{R} \in E \land s \in S \land f \in (E^{(S ∖ \{s\})}))) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) \in (E^{S})$
54	8 17 53	syl2anc	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) \in (E^{S})$
55		breq1	$⊢ g = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) \to ({finSupp}_{\underset{˙}{0}} (g) \leftrightarrow {finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z)))))$
56		oveq1	$⊢ g = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) \to g linC (M) S = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) linC (M) S$
57	56	eqeq1d	$⊢ g = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) \to (g linC (M) S = Z \leftrightarrow (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) linC (M) S = Z)$
58	55 57	anbi12d	$⊢ g = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) \to (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \leftrightarrow ({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z)))) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) linC (M) S = Z))$
59		fveq1	$⊢ g = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) \to g (s) = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) (s)$
60	59	neeq1d	$⊢ g = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) \to (g (s) \neq \underset{˙}{0} \leftrightarrow (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) (s) \neq \underset{˙}{0})$
61	58 60	anbi12d	$⊢ g = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) \to ((({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z)))) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) linC (M) S = Z) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) (s) \neq \underset{˙}{0}))$
62	61	adantl	$⊢ (((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \land g = (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z)))) \to ((({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z)))) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) linC (M) S = Z) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) (s) \neq \underset{˙}{0}))$
63	54 62	rspcedv	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to ((({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z)))) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) linC (M) S = Z) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (1_{R}), f (z))) (s) \neq \underset{˙}{0}) \to \exists g \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}))$
64	38 52 63	mp2and	$⊢ ((((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \land f \in (E^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \to \exists g \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0})$
65	64	rexlimdva2	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land s \in S) \to (\exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \to \exists g \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (g) \land g linC (M) S = Z) \land g (s) \neq \underset{˙}{0}))$
66	65	reximdva	$⊢ (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 \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}))$
67	66	imp	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land \exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \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})$
68		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})$
69		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})$
70	68 69	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})$
71	70	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})$
72		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})$
73	71 72	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})$
74	67 73	sylibr	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land \exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s)) \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})$
75	1 2 3 4 5	islindeps	$⊢ (M \in LMod \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}))$
76	75	3adant3	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \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}))$
77	76	adantr	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land \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 \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}))$
78	74 77	mpbird	$⊢ ((M \in LMod \land S \in 𝒫 B \land R \in NzRing) \land \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$
79	78	ex	$⊢ (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)$

Metamath Proof Explorer

Theorem islindeps2

Proof