snlindsntor

Description: A singleton is linearly independent iff it does not contain a torsion element. According to Wikipedia ("Torsion (algebra)", 15-Apr-2019, https://en.wikipedia.org/wiki/Torsion_(algebra) ): "An element m of a module M over a ring R is called atorsion element of the module if there exists a regular element r of the ring (an element that is neither a left nor a right zero divisor) that annihilates m, i.e., ( r .x. m ) = 0 . In an integral domain (a commutative ring without zero divisors), every nonzero element is regular, so a torsion element of a module over an integral domain is one annihilated by a nonzero element of the integral domain." Analogously, the definition in Lang p. 147 states that "An element x of [a module] E [over a ring R] is called atorsion element if there exists a e. R , a =/= 0 , such that a .x. x = 0 . This definition includes the zero element of the module. Some authors, however, exclude the zero element from the definition of torsion elements. (Contributed by AV, 14-Apr-2019) (Revised by AV, 27-Apr-2019)

	Ref	Expression
Hypotheses	snlindsntor.b	$⊢ B = {Base}_{M}$
	snlindsntor.r	$⊢ R = Scalar (M)$
	snlindsntor.s	$⊢ S = {Base}_{R}$
	snlindsntor.0	$⊢ \underset{˙}{0} = 0_{R}$
	snlindsntor.z	$⊢ Z = 0_{M}$
	snlindsntor.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
Assertion	snlindsntor	$⊢ (M \in LMod \land X \in B) \to (\forall s \in (S ∖ \{\underset{˙}{0}\}) s \underset{˙}{\cdot} X \neq Z \leftrightarrow \{X\} linIndS M)$

Proof

Step	Hyp	Ref	Expression
1		snlindsntor.b	$⊢ B = {Base}_{M}$
2		snlindsntor.r	$⊢ R = Scalar (M)$
3		snlindsntor.s	$⊢ S = {Base}_{R}$
4		snlindsntor.0	$⊢ \underset{˙}{0} = 0_{R}$
5		snlindsntor.z	$⊢ Z = 0_{M}$
6		snlindsntor.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
7		df-ne	$⊢ s \underset{˙}{\cdot} X \neq Z \leftrightarrow \neg s \underset{˙}{\cdot} X = Z$
8	7	ralbii	$⊢ \forall s \in (S ∖ \{\underset{˙}{0}\}) s \underset{˙}{\cdot} X \neq Z \leftrightarrow \forall s \in (S ∖ \{\underset{˙}{0}\}) \neg s \underset{˙}{\cdot} X = Z$
9		raldifsni	$⊢ \forall s \in (S ∖ \{\underset{˙}{0}\}) \neg s \underset{˙}{\cdot} X = Z \leftrightarrow \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})$
10	8 9	bitri	$⊢ \forall s \in (S ∖ \{\underset{˙}{0}\}) s \underset{˙}{\cdot} X \neq Z \leftrightarrow \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})$
11		simpl	$⊢ (M \in LMod \land X \in B) \to M \in LMod$
12	11	adantr	$⊢ ((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \to M \in LMod$
13	12	adantr	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to M \in LMod$
14	2	fveq2i	$⊢ {Base}_{R} = {Base}_{Scalar (M)}$
15	3 14	eqtri	$⊢ S = {Base}_{Scalar (M)}$
16	15	oveq1i	$⊢ S^{\{X\}} = {Base}_{Scalar (M)}^{\{X\}}$
17	16	eleq2i	$⊢ f \in (S^{\{X\}}) \leftrightarrow f \in ({Base}_{Scalar (M)}^{\{X\}})$
18	17	biimpi	$⊢ f \in (S^{\{X\}}) \to f \in ({Base}_{Scalar (M)}^{\{X\}})$
19	18	adantl	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to f \in ({Base}_{Scalar (M)}^{\{X\}})$
20		snelpwi	$⊢ X \in {Base}_{M} \to \{X\} \in 𝒫 {Base}_{M}$
21	20 1	eleq2s	$⊢ X \in B \to \{X\} \in 𝒫 {Base}_{M}$
22	21	ad3antlr	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to \{X\} \in 𝒫 {Base}_{M}$
23		lincval	$⊢ (M \in LMod \land f \in ({Base}_{Scalar (M)}^{\{X\}}) \land \{X\} \in 𝒫 {Base}_{M}) \to f linC (M) \{X\} = \underset{x \in \{X\}}{\sum_{M}} (f (x) \cdot_{M} x)$
24	13 19 22 23	syl3anc	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to f linC (M) \{X\} = \underset{x \in \{X\}}{\sum_{M}} (f (x) \cdot_{M} x)$
25	24	eqeq1d	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to (f linC (M) \{X\} = Z \leftrightarrow \underset{x \in \{X\}}{\sum_{M}} (f (x) \cdot_{M} x) = Z)$
26	25	anbi2d	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (f) \land \underset{x \in \{X\}}{\sum_{M}} (f (x) \cdot_{M} x) = Z))$
27		lmodgrp	$⊢ M \in LMod \to M \in Grp$
28		grpmnd	$⊢ M \in Grp \to M \in Mnd$
29	27 28	syl	$⊢ M \in LMod \to M \in Mnd$
30	29	ad3antrrr	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to M \in Mnd$
31		simpllr	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to X \in B$
32		elmapi	$⊢ f \in (S^{\{X\}}) \to f : \{X\} ⟶ S$
33	12	adantl	$⊢ (f : \{X\} ⟶ S \land ((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))) \to M \in LMod$
34		snidg	$⊢ X \in B \to X \in \{X\}$
35	34	adantl	$⊢ (M \in LMod \land X \in B) \to X \in \{X\}$
36	35	adantr	$⊢ ((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \to X \in \{X\}$
37		ffvelrn	$⊢ (f : \{X\} ⟶ S \land X \in \{X\}) \to f (X) \in S$
38	36 37	sylan2	$⊢ (f : \{X\} ⟶ S \land ((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))) \to f (X) \in S$
39		simprlr	$⊢ (f : \{X\} ⟶ S \land ((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))) \to X \in B$
40		eqid	$⊢ \cdot_{M} = \cdot_{M}$
41	1 2 40 3	lmodvscl	$⊢ (M \in LMod \land f (X) \in S \land X \in B) \to f (X) \cdot_{M} X \in B$
42	33 38 39 41	syl3anc	$⊢ (f : \{X\} ⟶ S \land ((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))) \to f (X) \cdot_{M} X \in B$
43	42	expcom	$⊢ ((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \to (f : \{X\} ⟶ S \to f (X) \cdot_{M} X \in B)$
44	32 43	syl5com	$⊢ f \in (S^{\{X\}}) \to (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \to f (X) \cdot_{M} X \in B)$
45	44	impcom	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to f (X) \cdot_{M} X \in B$
46		fveq2	$⊢ x = X \to f (x) = f (X)$
47		id	$⊢ x = X \to x = X$
48	46 47	oveq12d	$⊢ x = X \to f (x) \cdot_{M} x = f (X) \cdot_{M} X$
49	1 48	gsumsn	$⊢ (M \in Mnd \land X \in B \land f (X) \cdot_{M} X \in B) \to \underset{x \in \{X\}}{\sum_{M}} (f (x) \cdot_{M} x) = f (X) \cdot_{M} X$
50	30 31 45 49	syl3anc	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to \underset{x \in \{X\}}{\sum_{M}} (f (x) \cdot_{M} x) = f (X) \cdot_{M} X$
51	50	eqeq1d	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to (\underset{x \in \{X\}}{\sum_{M}} (f (x) \cdot_{M} x) = Z \leftrightarrow f (X) \cdot_{M} X = Z)$
52	34 37	sylan2	$⊢ (f : \{X\} ⟶ S \land X \in B) \to f (X) \in S$
53	52	expcom	$⊢ X \in B \to (f : \{X\} ⟶ S \to f (X) \in S)$
54	53	adantl	$⊢ (M \in LMod \land X \in B) \to (f : \{X\} ⟶ S \to f (X) \in S)$
55	6	oveqi	$⊢ f (X) \underset{˙}{\cdot} X = f (X) \cdot_{M} X$
56	55	eqeq1i	$⊢ f (X) \underset{˙}{\cdot} X = Z \leftrightarrow f (X) \cdot_{M} X = Z$
57		oveq1	$⊢ s = f (X) \to s \underset{˙}{\cdot} X = f (X) \underset{˙}{\cdot} X$
58	57	eqeq1d	$⊢ s = f (X) \to (s \underset{˙}{\cdot} X = Z \leftrightarrow f (X) \underset{˙}{\cdot} X = Z)$
59		eqeq1	$⊢ s = f (X) \to (s = \underset{˙}{0} \leftrightarrow f (X) = \underset{˙}{0})$
60	58 59	imbi12d	$⊢ s = f (X) \to ((s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}) \leftrightarrow (f (X) \underset{˙}{\cdot} X = Z \to f (X) = \underset{˙}{0}))$
61	60	rspcva	$⊢ (f (X) \in S \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \to (f (X) \underset{˙}{\cdot} X = Z \to f (X) = \underset{˙}{0})$
62	56 61	syl5bir	$⊢ (f (X) \in S \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \to (f (X) \cdot_{M} X = Z \to f (X) = \underset{˙}{0})$
63	62	ex	$⊢ f (X) \in S \to (\forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}) \to (f (X) \cdot_{M} X = Z \to f (X) = \underset{˙}{0}))$
64	32 54 63	syl56	$⊢ (M \in LMod \land X \in B) \to (f \in (S^{\{X\}}) \to (\forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}) \to (f (X) \cdot_{M} X = Z \to f (X) = \underset{˙}{0})))$
65	64	com23	$⊢ (M \in LMod \land X \in B) \to (\forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}) \to (f \in (S^{\{X\}}) \to (f (X) \cdot_{M} X = Z \to f (X) = \underset{˙}{0})))$
66	65	imp31	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to (f (X) \cdot_{M} X = Z \to f (X) = \underset{˙}{0})$
67	51 66	sylbid	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to (\underset{x \in \{X\}}{\sum_{M}} (f (x) \cdot_{M} x) = Z \to f (X) = \underset{˙}{0})$
68	67	adantld	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to (({finSupp}_{\underset{˙}{0}} (f) \land \underset{x \in \{X\}}{\sum_{M}} (f (x) \cdot_{M} x) = Z) \to f (X) = \underset{˙}{0})$
69	26 68	sylbid	$⊢ (((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \land f \in (S^{\{X\}})) \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0})$
70	69	ralrimiva	$⊢ ((M \in LMod \land X \in B) \land \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0})) \to \forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0})$
71	70	ex	$⊢ (M \in LMod \land X \in B) \to (\forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}) \to \forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0}))$
72		impexp	$⊢ (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0}) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (f) \to (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}))$
73	32	adantl	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to f : \{X\} ⟶ S$
74		snfi	$⊢ \{X\} \in Fin$
75	74	a1i	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to \{X\} \in Fin$
76	4	fvexi	$⊢ \underset{˙}{0} \in V$
77	76	a1i	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to \underset{˙}{0} \in V$
78	73 75 77	fdmfifsupp	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to {finSupp}_{\underset{˙}{0}} (f)$
79		pm2.27	$⊢ {finSupp}_{\underset{˙}{0}} (f) \to (({finSupp}_{\underset{˙}{0}} (f) \to (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0})) \to (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}))$
80	78 79	syl	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to (({finSupp}_{\underset{˙}{0}} (f) \to (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0})) \to (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}))$
81	72 80	syl5bi	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to ((({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0}) \to (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}))$
82	81	ralimdva	$⊢ (M \in LMod \land X \in B) \to (\forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0}) \to \forall f \in (S^{\{X\}}) (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}))$
83	1 2 3 4 5 6	snlindsntorlem	$⊢ (M \in LMod \land X \in B) \to (\forall f \in (S^{\{X\}}) (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}) \to \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))$
84	82 83	syld	$⊢ (M \in LMod \land X \in B) \to (\forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0}) \to \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))$
85	71 84	impbid	$⊢ (M \in LMod \land X \in B) \to (\forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}) \leftrightarrow \forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0}))$
86		fveqeq2	$⊢ y = X \to (f (y) = \underset{˙}{0} \leftrightarrow f (X) = \underset{˙}{0})$
87	86	ralsng	$⊢ X \in B \to (\forall y \in \{X\} f (y) = \underset{˙}{0} \leftrightarrow f (X) = \underset{˙}{0})$
88	87	adantl	$⊢ (M \in LMod \land X \in B) \to (\forall y \in \{X\} f (y) = \underset{˙}{0} \leftrightarrow f (X) = \underset{˙}{0})$
89	88	bicomd	$⊢ (M \in LMod \land X \in B) \to (f (X) = \underset{˙}{0} \leftrightarrow \forall y \in \{X\} f (y) = \underset{˙}{0})$
90	89	imbi2d	$⊢ (M \in LMod \land X \in B) \to ((({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to \forall y \in \{X\} f (y) = \underset{˙}{0}))$
91	90	ralbidv	$⊢ (M \in LMod \land X \in B) \to (\forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to f (X) = \underset{˙}{0}) \leftrightarrow \forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to \forall y \in \{X\} f (y) = \underset{˙}{0}))$
92		snelpwi	$⊢ X \in B \to \{X\} \in 𝒫 B$
93	92	adantl	$⊢ (M \in LMod \land X \in B) \to \{X\} \in 𝒫 B$
94	93	biantrurd	$⊢ (M \in LMod \land X \in B) \to (\forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to \forall y \in \{X\} f (y) = \underset{˙}{0}) \leftrightarrow (\{X\} \in 𝒫 B \land \forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to \forall y \in \{X\} f (y) = \underset{˙}{0})))$
95	85 91 94	3bitrd	$⊢ (M \in LMod \land X \in B) \to (\forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}) \leftrightarrow (\{X\} \in 𝒫 B \land \forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to \forall y \in \{X\} f (y) = \underset{˙}{0})))$
96	10 95	syl5bb	$⊢ (M \in LMod \land X \in B) \to (\forall s \in (S ∖ \{\underset{˙}{0}\}) s \underset{˙}{\cdot} X \neq Z \leftrightarrow (\{X\} \in 𝒫 B \land \forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to \forall y \in \{X\} f (y) = \underset{˙}{0})))$
97		snex	$⊢ \{X\} \in V$
98	1 5 2 3 4	islininds	$⊢ (\{X\} \in V \land M \in LMod) \to (\{X\} linIndS M \leftrightarrow (\{X\} \in 𝒫 B \land \forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to \forall y \in \{X\} f (y) = \underset{˙}{0})))$
99	97 11 98	sylancr	$⊢ (M \in LMod \land X \in B) \to (\{X\} linIndS M \leftrightarrow (\{X\} \in 𝒫 B \land \forall f \in (S^{\{X\}}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X\} = Z) \to \forall y \in \{X\} f (y) = \underset{˙}{0})))$
100	96 99	bitr4d	$⊢ (M \in LMod \land X \in B) \to (\forall s \in (S ∖ \{\underset{˙}{0}\}) s \underset{˙}{\cdot} X \neq Z \leftrightarrow \{X\} linIndS M)$

Metamath Proof Explorer

Theorem snlindsntor

Proof