Theorem snlindsntor 49093

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 a torsion 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., (𝑟 · 𝑚) = 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 a torsion element if there exists 𝑎 ∈ 𝑅, 𝑎 ≠ 0, such that 𝑎 · 𝑥 = 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.)

Hypotheses

Ref	Expression
snlindsntor.b	⊢ 𝐵 = (Base‘𝑀)
snlindsntor.r	⊢ 𝑅 = (Scalar‘𝑀)
snlindsntor.s	⊢ 𝑆 = (Base‘𝑅)
snlindsntor.0	⊢ 0 = (0g‘𝑅)
snlindsntor.z	⊢ 𝑍 = (0g‘𝑀)
snlindsntor.t	⊢ · = ( ·𝑠 ‘𝑀)

Assertion

Ref	Expression
snlindsntor	⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ {𝑋} linIndS 𝑀))

Distinct variable groups:   𝐵,𝑠   𝑀,𝑠   𝑆,𝑠   𝑋,𝑠   𝑍,𝑠   · ,𝑠   0 ,𝑠

Allowed substitution hint:   𝑅(𝑠)

Proof of Theorem snlindsntor

Dummy variables 𝑓 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ne 2958	. . . . 5 ⊢ ((𝑠 · 𝑋) ≠ 𝑍 ↔ ¬ (𝑠 · 𝑋) = 𝑍)
2	1	ralbii 3108	. . . 4 ⊢ (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ ∀𝑠 ∈ (𝑆 ∖ { 0 }) ¬ (𝑠 · 𝑋) = 𝑍)
3		raldifsni 4755	. . . 4 ⊢ (∀𝑠 ∈ (𝑆 ∖ { 0 }) ¬ (𝑠 · 𝑋) = 𝑍 ↔ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))
4	2, 3	bitri 277	. . 3 ⊢ (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))
5		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → 𝑀 ∈ LMod)
6	5	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → 𝑀 ∈ LMod)
7	6	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑀 ∈ LMod)
8		snlindsntor.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (Base‘𝑅)
9		snlindsntor.r	. . . . . . . . . . . . . . . 16 ⊢ 𝑅 = (Scalar‘𝑀)
10	9	fveq2i 6870	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑅) = (Base‘(Scalar‘𝑀))
11	8, 10	eqtri 2785	. . . . . . . . . . . . . 14 ⊢ 𝑆 = (Base‘(Scalar‘𝑀))
12	11	oveq1i 7406	. . . . . . . . . . . . 13 ⊢ (𝑆 ↑m {𝑋}) = ((Base‘(Scalar‘𝑀)) ↑m {𝑋})
13	12	eleq2i 2854	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (𝑆 ↑m {𝑋}) ↔ 𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑋}))
14	13	bilani 508	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑋}))
15		snelpwi 5411	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ (Base‘𝑀) → {𝑋} ∈ 𝒫 (Base‘𝑀))
16		snlindsntor.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑀)
17	15, 16	eleq2s 2880	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ 𝐵 → {𝑋} ∈ 𝒫 (Base‘𝑀))
18	17	ad3antlr 741	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → {𝑋} ∈ 𝒫 (Base‘𝑀))
19		lincval 49031	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ LMod ∧ 𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑋}) ∧ {𝑋} ∈ 𝒫 (Base‘𝑀)) → (𝑓( linC ‘𝑀){𝑋}) = (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))))
20	7, 14, 18, 19	syl3anc 1390	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → (𝑓( linC ‘𝑀){𝑋}) = (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))))
21	20	eqeq1d 2764	. . . . . . . . 9 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 ↔ (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))) = 𝑍))
22	21	anbi2d 639	. . . . . . . 8 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) ↔ (𝑓 finSupp 0 ∧ (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))) = 𝑍)))
23		lmodgrp 20934	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ LMod → 𝑀 ∈ Grp)
24	23	grpmndd 18988	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ LMod → 𝑀 ∈ Mnd)
25	24	ad3antrrr 740	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑀 ∈ Mnd)
26		simpllr 785	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑋 ∈ 𝐵)
27		elmapi 8830	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ (𝑆 ↑m {𝑋}) → 𝑓:{𝑋}⟶𝑆)
28	6	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → 𝑀 ∈ LMod)
29		snidg 4619	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ {𝑋})
30	29	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ {𝑋})
31	30	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → 𝑋 ∈ {𝑋})
32		ffvelcdm 7062	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓:{𝑋}⟶𝑆 ∧ 𝑋 ∈ {𝑋}) → (𝑓‘𝑋) ∈ 𝑆)
33	31, 32	sylan2 602	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → (𝑓‘𝑋) ∈ 𝑆)
34		simprlr 789	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → 𝑋 ∈ 𝐵)
35		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ ( ·𝑠 ‘𝑀) = ( ·𝑠 ‘𝑀)
36	16, 9, 35, 8	lmodvscl 20945	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ LMod ∧ (𝑓‘𝑋) ∈ 𝑆 ∧ 𝑋 ∈ 𝐵) → ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) ∈ 𝐵)
37	28, 33, 34, 36	syl3anc 1390	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) ∈ 𝐵)
38	37	expcom 417	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → (𝑓:{𝑋}⟶𝑆 → ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) ∈ 𝐵))
39	27, 38	syl5com 31	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ (𝑆 ↑m {𝑋}) → (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) ∈ 𝐵))
40	39	impcom 411	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) ∈ 𝐵)
41		fveq2 6867	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑓‘𝑥) = (𝑓‘𝑋))
42		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
43	41, 42	oveq12d 7414	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥) = ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋))
44	16, 43	gsumsn 19994	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) ∈ 𝐵) → (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))) = ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋))
45	25, 26, 40, 44	syl3anc 1390	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))) = ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋))
46	45	eqeq1d 2764	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))) = 𝑍 ↔ ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) = 𝑍))
47	29, 32	sylan2 602	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:{𝑋}⟶𝑆 ∧ 𝑋 ∈ 𝐵) → (𝑓‘𝑋) ∈ 𝑆)
48	47	expcom 417	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝐵 → (𝑓:{𝑋}⟶𝑆 → (𝑓‘𝑋) ∈ 𝑆))
49	48	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (𝑓:{𝑋}⟶𝑆 → (𝑓‘𝑋) ∈ 𝑆))
50		snlindsntor.t	. . . . . . . . . . . . . . . . 17 ⊢ · = ( ·𝑠 ‘𝑀)
51	50	oveqi 7409	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘𝑋) · 𝑋) = ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋)
52	51	eqeq1i 2767	. . . . . . . . . . . . . . 15 ⊢ (((𝑓‘𝑋) · 𝑋) = 𝑍 ↔ ((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) = 𝑍)
53		oveq1 7403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (𝑓‘𝑋) → (𝑠 · 𝑋) = ((𝑓‘𝑋) · 𝑋))
54	53	eqeq1d 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑓‘𝑋) → ((𝑠 · 𝑋) = 𝑍 ↔ ((𝑓‘𝑋) · 𝑋) = 𝑍))
55		eqeq1 2766	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑓‘𝑋) → (𝑠 = 0 ↔ (𝑓‘𝑋) = 0 ))
56	54, 55	imbi12d 346	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑓‘𝑋) → (((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) ↔ (((𝑓‘𝑋) · 𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )))
57	56	rspcva 3579	. . . . . . . . . . . . . . 15 ⊢ (((𝑓‘𝑋) ∈ 𝑆 ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → (((𝑓‘𝑋) · 𝑋) = 𝑍 → (𝑓‘𝑋) = 0 ))
58	52, 57	biimtrrid 245	. . . . . . . . . . . . . 14 ⊢ (((𝑓‘𝑋) ∈ 𝑆 ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → (((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 ))
59	58	ex 416	. . . . . . . . . . . . 13 ⊢ ((𝑓‘𝑋) ∈ 𝑆 → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → (((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )))
60	27, 49, 59	syl56 36	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (𝑓 ∈ (𝑆 ↑m {𝑋}) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → (((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 ))))
61	60	com23 86	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → (𝑓 ∈ (𝑆 ↑m {𝑋}) → (((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 ))))
62	61	imp31 421	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → (((𝑓‘𝑋)( ·𝑠 ‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 ))
63	46, 62	sylbid 242	. . . . . . . . 9 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))) = 𝑍 → (𝑓‘𝑋) = 0 ))
64	63	adantld 494	. . . . . . . 8 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓 finSupp 0 ∧ (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))) = 𝑍) → (𝑓‘𝑋) = 0 ))
65	22, 64	sylbid 242	. . . . . . 7 ⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ))
66	65	ralrimiva 3154	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ))
67	66	ex 416	. . . . 5 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 )))
68		impexp 454	. . . . . . . 8 ⊢ (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) ↔ (𝑓 finSupp 0 → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )))
69	27	adantl 485	. . . . . . . . . 10 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑓:{𝑋}⟶𝑆)
70		snfi 9024	. . . . . . . . . . 11 ⊢ {𝑋} ∈ Fin
71	70	a1i 11	. . . . . . . . . 10 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → {𝑋} ∈ Fin)
72		snlindsntor.0	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝑅)
73	72	fvexi 6881	. . . . . . . . . . 11 ⊢ 0 ∈ V
74	73	a1i 11	. . . . . . . . . 10 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 0 ∈ V)
75	69, 71, 74	fdmfifsupp 9321	. . . . . . . . 9 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑓 finSupp 0 )
76		pm2.27 42	. . . . . . . . 9 ⊢ (𝑓 finSupp 0 → ((𝑓 finSupp 0 → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )))
77	75, 76	syl 17	. . . . . . . 8 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓 finSupp 0 → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )))
78	68, 77	biimtrid 244	. . . . . . 7 ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )))
79	78	ralimdva 3174	. . . . . 6 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) → ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )))
80		snlindsntor.z	. . . . . . 7 ⊢ 𝑍 = (0g‘𝑀)
81	16, 9, 8, 72, 80, 50	snlindsntorlem 49092	. . . . . 6 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )))
82	79, 81	syld 47	. . . . 5 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )))
83	67, 82	impbid 214	. . . 4 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) ↔ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 )))
84		fveqeq2 6876	. . . . . . . . 9 ⊢ (𝑦 = 𝑋 → ((𝑓‘𝑦) = 0 ↔ (𝑓‘𝑋) = 0 ))
85	84	ralsng 4634	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐵 → (∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ↔ (𝑓‘𝑋) = 0 ))
86	85	adantl 485	. . . . . . 7 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ↔ (𝑓‘𝑋) = 0 ))
87	86	bicomd 225	. . . . . 6 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → ((𝑓‘𝑋) = 0 ↔ ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))
88	87	imbi2d 342	. . . . 5 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) ↔ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))
89	88	ralbidv 3185	. . . 4 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) ↔ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))
90		snelpwi 5411	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → {𝑋} ∈ 𝒫 𝐵)
91	90	adantl 485	. . . . 5 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → {𝑋} ∈ 𝒫 𝐵)
92	91	biantrurd 540	. . . 4 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ) ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))))
93	83, 89, 92	3bitrd 307	. . 3 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))))
94	4, 93	bitrid 285	. 2 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))))
95		snex 5396	. . 3 ⊢ {𝑋} ∈ V
96	16, 80, 9, 8, 72	islininds 49068	. . 3 ⊢ (({𝑋} ∈ V ∧ 𝑀 ∈ LMod) → ({𝑋} linIndS 𝑀 ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))))
97	95, 5, 96	sylancr 596	. 2 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → ({𝑋} linIndS 𝑀 ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))))
98	94, 97	bitr4d 284	1 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ {𝑋} linIndS 𝑀))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142   ≠ wne 2957  ∀wral 3076  Vcvv 3454   ∖ cdif 3901  𝒫 cpw 4555  {csn 4582   class class class wbr 5100   ↦ cmpt 5181  ⟶wf 6517  ‘cfv 6521  (class class class)co 7396   ↑_m cmap 8808  Fincfn 8927   finSupp cfsupp 9307  Basecbs 17245  Scalarcsca 17289   ·_𝑠 cvsca 17290  0_gc0g 17468   Σ_g cgsu 17469  Mndcmnd 18768  LModclmod 20927   linC clinc 49026   linIndS clininds 49062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-isom 6530  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-supp 8141  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-er 8678  df-map 8810  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fsupp 9308  df-oi 9458  df-card 9897  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-n0 12482  df-z 12569  df-uz 12840  df-fz 13513  df-fzo 13660  df-seq 14015  df-hash 14344  df-0g 17470  df-gsum 17471  df-mgm 18674  df-sgrp 18753  df-mnd 18769  df-grp 18978  df-mulg 19110  df-cntz 19357  df-lmod 20929  df-linc 49028  df-lininds 49064

This theorem is referenced by:  lindssnlvec  49108