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	27	grpmndd	$⊢ M \in LMod \to M \in Mnd$
29	28	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$
30		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$
31		elmapi	$⊢ f \in (S^{\{X\}}) \to f : \{X\} ⟶ S$
32	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$
33		snidg	$⊢ X \in B \to X \in \{X\}$
34	33	adantl	$⊢ (M \in LMod \land X \in B) \to X \in \{X\}$
35	34	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\}$
36		ffvelrn	$⊢ (f : \{X\} ⟶ S \land X \in \{X\}) \to f (X) \in S$
37	35 36	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$
38		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$
39		eqid	$⊢ \cdot_{M} = \cdot_{M}$
40	1 2 39 3	lmodvscl	$⊢ (M \in LMod \land f (X) \in S \land X \in B) \to f (X) \cdot_{M} X \in B$
41	32 37 38 40	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$
42	41	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)$
43	31 42	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)$
44	43	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$
45		fveq2	$⊢ x = X \to f (x) = f (X)$
46		id	$⊢ x = X \to x = X$
47	45 46	oveq12d	$⊢ x = X \to f (x) \cdot_{M} x = f (X) \cdot_{M} X$
48	1 47	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$
49	29 30 44 48	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$
50	49	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)$
51	33 36	sylan2	$⊢ (f : \{X\} ⟶ S \land X \in B) \to f (X) \in S$
52	51	expcom	$⊢ X \in B \to (f : \{X\} ⟶ S \to f (X) \in S)$
53	52	adantl	$⊢ (M \in LMod \land X \in B) \to (f : \{X\} ⟶ S \to f (X) \in S)$
54	6	oveqi	$⊢ f (X) \underset{˙}{\cdot} X = f (X) \cdot_{M} X$
55	54	eqeq1i	$⊢ f (X) \underset{˙}{\cdot} X = Z \leftrightarrow f (X) \cdot_{M} X = Z$
56		oveq1	$⊢ s = f (X) \to s \underset{˙}{\cdot} X = f (X) \underset{˙}{\cdot} X$
57	56	eqeq1d	$⊢ s = f (X) \to (s \underset{˙}{\cdot} X = Z \leftrightarrow f (X) \underset{˙}{\cdot} X = Z)$
58		eqeq1	$⊢ s = f (X) \to (s = \underset{˙}{0} \leftrightarrow f (X) = \underset{˙}{0})$
59	57 58	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}))$
60	59	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})$
61	55 60	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})$
62	61	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}))$
63	31 53 62	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})))$
64	63	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})))$
65	64	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})$
66	50 65	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})$
67	66	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})$
68	26 67	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})$
69	68	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})$
70	69	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}))$
71		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}))$
72	31	adantl	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to f : \{X\} ⟶ S$
73		snfi	$⊢ \{X\} \in Fin$
74	73	a1i	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to \{X\} \in Fin$
75	4	fvexi	$⊢ \underset{˙}{0} \in V$
76	75	a1i	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to \underset{˙}{0} \in V$
77	72 74 76	fdmfifsupp	$⊢ ((M \in LMod \land X \in B) \land f \in (S^{\{X\}})) \to {finSupp}_{\underset{˙}{0}} (f)$
78		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}))$
79	77 78	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}))$
80	71 79	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}))$
81	80	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}))$
82	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}))$
83	81 82	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}))$
84	70 83	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}))$
85		fveqeq2	$⊢ y = X \to (f (y) = \underset{˙}{0} \leftrightarrow f (X) = \underset{˙}{0})$
86	85	ralsng	$⊢ X \in B \to (\forall y \in \{X\} f (y) = \underset{˙}{0} \leftrightarrow f (X) = \underset{˙}{0})$
87	86	adantl	$⊢ (M \in LMod \land X \in B) \to (\forall y \in \{X\} f (y) = \underset{˙}{0} \leftrightarrow f (X) = \underset{˙}{0})$
88	87	bicomd	$⊢ (M \in LMod \land X \in B) \to (f (X) = \underset{˙}{0} \leftrightarrow \forall y \in \{X\} f (y) = \underset{˙}{0})$
89	88	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}))$
90	89	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}))$
91		snelpwi	$⊢ X \in B \to \{X\} \in 𝒫 B$
92	91	adantl	$⊢ (M \in LMod \land X \in B) \to \{X\} \in 𝒫 B$
93	92	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})))$
94	84 90 93	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})))$
95	10 94	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})))$
96		snex	$⊢ \{X\} \in V$
97	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})))$
98	96 11 97	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})))$
99	95 98	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