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