Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
snlindsntor.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
snlindsntor.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
snlindsntor.0 ⊢ 0 = ( 0g ‘ 𝑅 )
snlindsntor.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
snlindsntor.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
Assertion snlindsntor ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑠 ∈ ( 𝑆 ∖ { 0 } ) ( 𝑠 · 𝑋 ) ≠ 𝑍 ↔ { 𝑋 } linIndS 𝑀 ) )

Proof

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