lindsrng01

Description: Any subset of a module is always linearly independent if the underlying ring has at most one element. Since the underlying ring cannot be the empty set (see lmodsn0 ), this means that the underlying ring has only one element, so it is a zero ring. (Contributed by AV, 14-Apr-2019) (Revised by AV, 27-Apr-2019)

	Ref	Expression
Hypotheses	lindsrng01.b	$⊢ B = {Base}_{M}$
	lindsrng01.r	$⊢ R = Scalar (M)$
	lindsrng01.e	$⊢ E = {Base}_{R}$
Assertion	lindsrng01	$⊢ (M \in LMod \land (\|E\| = 0 \lor \|E\| = 1) \land S \in 𝒫 B) \to S linIndS M$

Proof

Step	Hyp	Ref	Expression
1		lindsrng01.b	$⊢ B = {Base}_{M}$
2		lindsrng01.r	$⊢ R = Scalar (M)$
3		lindsrng01.e	$⊢ E = {Base}_{R}$
4	2 3	lmodsn0	$⊢ M \in LMod \to E \neq \emptyset$
5	3	fvexi	$⊢ E \in V$
6		hasheq0	$⊢ E \in V \to (\|E\| = 0 \leftrightarrow E = \emptyset)$
7	5 6	ax-mp	$⊢ \|E\| = 0 \leftrightarrow E = \emptyset$
8		eqneqall	$⊢ E = \emptyset \to (E \neq \emptyset \to S linIndS M)$
9	8	com12	$⊢ E \neq \emptyset \to (E = \emptyset \to S linIndS M)$
10	7 9	syl5bi	$⊢ E \neq \emptyset \to (\|E\| = 0 \to S linIndS M)$
11	4 10	syl	$⊢ M \in LMod \to (\|E\| = 0 \to S linIndS M)$
12	11	adantr	$⊢ (M \in LMod \land S \in 𝒫 B) \to (\|E\| = 0 \to S linIndS M)$
13	12	com12	$⊢ \|E\| = 0 \to ((M \in LMod \land S \in 𝒫 B) \to S linIndS M)$
14	2	lmodring	$⊢ M \in LMod \to R \in Ring$
15	14	adantr	$⊢ (M \in LMod \land S \in 𝒫 B) \to R \in Ring$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	3 16	0ring	$⊢ (R \in Ring \land \|E\| = 1) \to E = \{0_{R}\}$
18	15 17	sylan	$⊢ ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1) \to E = \{0_{R}\}$
19		simpr	$⊢ (M \in LMod \land S \in 𝒫 B) \to S \in 𝒫 B$
20	19	adantr	$⊢ ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1) \to S \in 𝒫 B$
21	20	adantl	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to S \in 𝒫 B$
22		snex	$⊢ \{0_{R}\} \in V$
23	20 22	jctil	$⊢ ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1) \to (\{0_{R}\} \in V \land S \in 𝒫 B)$
24	23	adantl	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to (\{0_{R}\} \in V \land S \in 𝒫 B)$
25		elmapg	$⊢ (\{0_{R}\} \in V \land S \in 𝒫 B) \to (f \in ({\{0_{R}\}}^{S}) \leftrightarrow f : S ⟶ \{0_{R}\})$
26	24 25	syl	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to (f \in ({\{0_{R}\}}^{S}) \leftrightarrow f : S ⟶ \{0_{R}\})$
27		fvex	$⊢ 0_{R} \in V$
28	27	fconst2	$⊢ f : S ⟶ \{0_{R}\} \leftrightarrow f = S \times \{0_{R}\}$
29		fconstmpt	$⊢ S \times \{0_{R}\} = (x \in S ⟼ 0_{R})$
30	29	eqeq2i	$⊢ f = S \times \{0_{R}\} \leftrightarrow f = (x \in S ⟼ 0_{R})$
31	28 30	bitri	$⊢ f : S ⟶ \{0_{R}\} \leftrightarrow f = (x \in S ⟼ 0_{R})$
32		eqidd	$⊢ ((E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \land v \in S) \to (x \in S ⟼ 0_{R}) = (x \in S ⟼ 0_{R})$
33		eqidd	$⊢ (((E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \land v \in S) \land x = v) \to 0_{R} = 0_{R}$
34		simpr	$⊢ ((E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \land v \in S) \to v \in S$
35		fvexd	$⊢ ((E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \land v \in S) \to 0_{R} \in V$
36	32 33 34 35	fvmptd	$⊢ ((E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \land v \in S) \to (x \in S ⟼ 0_{R}) (v) = 0_{R}$
37	36	ralrimiva	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to \forall v \in S (x \in S ⟼ 0_{R}) (v) = 0_{R}$
38	37	a1d	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to (({finSupp}_{0_{R}} ((x \in S ⟼ 0_{R})) \land (x \in S ⟼ 0_{R}) linC (M) S = 0_{M}) \to \forall v \in S (x \in S ⟼ 0_{R}) (v) = 0_{R})$
39		breq1	$⊢ f = (x \in S ⟼ 0_{R}) \to ({finSupp}_{0_{R}} (f) \leftrightarrow {finSupp}_{0_{R}} ((x \in S ⟼ 0_{R})))$
40		oveq1	$⊢ f = (x \in S ⟼ 0_{R}) \to f linC (M) S = (x \in S ⟼ 0_{R}) linC (M) S$
41	40	eqeq1d	$⊢ f = (x \in S ⟼ 0_{R}) \to (f linC (M) S = 0_{M} \leftrightarrow (x \in S ⟼ 0_{R}) linC (M) S = 0_{M})$
42	39 41	anbi12d	$⊢ f = (x \in S ⟼ 0_{R}) \to (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \leftrightarrow ({finSupp}_{0_{R}} ((x \in S ⟼ 0_{R})) \land (x \in S ⟼ 0_{R}) linC (M) S = 0_{M}))$
43		fveq1	$⊢ f = (x \in S ⟼ 0_{R}) \to f (v) = (x \in S ⟼ 0_{R}) (v)$
44	43	eqeq1d	$⊢ f = (x \in S ⟼ 0_{R}) \to (f (v) = 0_{R} \leftrightarrow (x \in S ⟼ 0_{R}) (v) = 0_{R})$
45	44	ralbidv	$⊢ f = (x \in S ⟼ 0_{R}) \to (\forall v \in S f (v) = 0_{R} \leftrightarrow \forall v \in S (x \in S ⟼ 0_{R}) (v) = 0_{R})$
46	42 45	imbi12d	$⊢ f = (x \in S ⟼ 0_{R}) \to ((({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R}) \leftrightarrow (({finSupp}_{0_{R}} ((x \in S ⟼ 0_{R})) \land (x \in S ⟼ 0_{R}) linC (M) S = 0_{M}) \to \forall v \in S (x \in S ⟼ 0_{R}) (v) = 0_{R}))$
47	38 46	syl5ibrcom	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to (f = (x \in S ⟼ 0_{R}) \to (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R}))$
48	31 47	syl5bi	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to (f : S ⟶ \{0_{R}\} \to (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R}))$
49	26 48	sylbid	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to (f \in ({\{0_{R}\}}^{S}) \to (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R}))$
50	49	ralrimiv	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to \forall f \in ({\{0_{R}\}}^{S}) (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R})$
51		oveq1	$⊢ E = \{0_{R}\} \to E^{S} = {\{0_{R}\}}^{S}$
52	51	raleqdv	$⊢ E = \{0_{R}\} \to (\forall f \in (E^{S}) (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R}) \leftrightarrow \forall f \in ({\{0_{R}\}}^{S}) (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R}))$
53	52	adantr	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to (\forall f \in (E^{S}) (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R}) \leftrightarrow \forall f \in ({\{0_{R}\}}^{S}) (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R}))$
54	50 53	mpbird	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to \forall f \in (E^{S}) (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R})$
55		simpl	$⊢ ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1) \to (M \in LMod \land S \in 𝒫 B)$
56	55	ancomd	$⊢ ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1) \to (S \in 𝒫 B \land M \in LMod)$
57	56	adantl	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to (S \in 𝒫 B \land M \in LMod)$
58		eqid	$⊢ 0_{M} = 0_{M}$
59	1 58 2 3 16	islininds	$⊢ (S \in 𝒫 B \land M \in LMod) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R})))$
60	57 59	syl	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{0_{R}} (f) \land f linC (M) S = 0_{M}) \to \forall v \in S f (v) = 0_{R})))$
61	21 54 60	mpbir2and	$⊢ (E = \{0_{R}\} \land ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1)) \to S linIndS M$
62	18 61	mpancom	$⊢ ((M \in LMod \land S \in 𝒫 B) \land \|E\| = 1) \to S linIndS M$
63	62	expcom	$⊢ \|E\| = 1 \to ((M \in LMod \land S \in 𝒫 B) \to S linIndS M)$
64	13 63	jaoi	$⊢ (\|E\| = 0 \lor \|E\| = 1) \to ((M \in LMod \land S \in 𝒫 B) \to S linIndS M)$
65	64	expd	$⊢ (\|E\| = 0 \lor \|E\| = 1) \to (M \in LMod \to (S \in 𝒫 B \to S linIndS M))$
66	65	com12	$⊢ M \in LMod \to ((\|E\| = 0 \lor \|E\| = 1) \to (S \in 𝒫 B \to S linIndS M))$
67	66	3imp	$⊢ (M \in LMod \land (\|E\| = 0 \lor \|E\| = 1) \land S \in 𝒫 B) \to S linIndS M$

Metamath Proof Explorer

Theorem lindsrng01

Proof