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 27 grpmndd ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd )
29 28 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → 𝑀 ∈ Mnd )
30 simpllr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → 𝑋 ∈ 𝐵 )
31 elmapi ⊢ ( 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) → 𝑓 : { 𝑋 } ⟶ 𝑆 )
32 12 adantl ⊢ ( ( 𝑓 : { 𝑋 } ⟶ 𝑆 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ) → 𝑀 ∈ LMod )
33 snidg ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ { 𝑋 } )
34 33 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ { 𝑋 } )
35 34 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) → 𝑋 ∈ { 𝑋 } )
36 ffvelcdm ⊢ ( ( 𝑓 : { 𝑋 } ⟶ 𝑆 ∧ 𝑋 ∈ { 𝑋 } ) → ( 𝑓 ‘ 𝑋 ) ∈ 𝑆 )
37 35 36 sylan2 ⊢ ( ( 𝑓 : { 𝑋 } ⟶ 𝑆 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ) → ( 𝑓 ‘ 𝑋 ) ∈ 𝑆 )
38 simprlr ⊢ ( ( 𝑓 : { 𝑋 } ⟶ 𝑆 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ) → 𝑋 ∈ 𝐵 )
39 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
40 1 2 39 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑓 ‘ 𝑋 ) ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ 𝐵 )
41 32 37 38 40 syl3anc ⊢ ( ( 𝑓 : { 𝑋 } ⟶ 𝑆 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ) → ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ 𝐵 )
42 41 expcom ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) → ( 𝑓 : { 𝑋 } ⟶ 𝑆 → ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ 𝐵 ) )
43 31 42 syl5com ⊢ ( 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) → ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) → ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ 𝐵 ) )
44 43 impcom ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ 𝐵 )
45 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑋 ) )
46 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
47 45 46 oveq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) )
48 1 47 gsumsn ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ 𝐵 ) → ( 𝑀 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) )
49 29 30 44 48 syl3anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → ( 𝑀 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) )
50 49 eqeq1d ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → ( ( 𝑀 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = 𝑍 ↔ ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = 𝑍 ) )
51 33 36 sylan2 ⊢ ( ( 𝑓 : { 𝑋 } ⟶ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑓 ‘ 𝑋 ) ∈ 𝑆 )
52 51 expcom ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑓 : { 𝑋 } ⟶ 𝑆 → ( 𝑓 ‘ 𝑋 ) ∈ 𝑆 ) )
53 52 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( 𝑓 : { 𝑋 } ⟶ 𝑆 → ( 𝑓 ‘ 𝑋 ) ∈ 𝑆 ) )
54 6 oveqi ⊢ ( ( 𝑓 ‘ 𝑋 ) · 𝑋 ) = ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 )
55 54 eqeq1i ⊢ ( ( ( 𝑓 ‘ 𝑋 ) · 𝑋 ) = 𝑍 ↔ ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = 𝑍 )
56 oveq1 ⊢ ( 𝑠 = ( 𝑓 ‘ 𝑋 ) → ( 𝑠 · 𝑋 ) = ( ( 𝑓 ‘ 𝑋 ) · 𝑋 ) )
57 56 eqeq1d ⊢ ( 𝑠 = ( 𝑓 ‘ 𝑋 ) → ( ( 𝑠 · 𝑋 ) = 𝑍 ↔ ( ( 𝑓 ‘ 𝑋 ) · 𝑋 ) = 𝑍 ) )
58 eqeq1 ⊢ ( 𝑠 = ( 𝑓 ‘ 𝑋 ) → ( 𝑠 = 0 ↔ ( 𝑓 ‘ 𝑋 ) = 0 ) )
59 57 58 imbi12d ⊢ ( 𝑠 = ( 𝑓 ‘ 𝑋 ) → ( ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ↔ ( ( ( 𝑓 ‘ 𝑋 ) · 𝑋 ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) )
60 59 rspcva ⊢ ( ( ( 𝑓 ‘ 𝑋 ) ∈ 𝑆 ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) → ( ( ( 𝑓 ‘ 𝑋 ) · 𝑋 ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) )
61 55 60 biimtrrid ⊢ ( ( ( 𝑓 ‘ 𝑋 ) ∈ 𝑆 ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) → ( ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) )
62 61 ex ⊢ ( ( 𝑓 ‘ 𝑋 ) ∈ 𝑆 → ( ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) → ( ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) )
63 31 53 62 syl56 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) → ( ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) → ( ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) ) )
64 63 com23 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) → ( 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) → ( ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) ) )
65 64 imp31 ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → ( ( ( 𝑓 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) )
66 50 65 sylbid ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → ( ( 𝑀 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) )
67 66 adantld ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → ( ( 𝑓 finSupp 0 ∧ ( 𝑀 Σg ( 𝑥 ∈ { 𝑋 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) )
68 26 67 sylbid ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) )
69 68 ralrimiva ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) → ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) )
70 69 ex ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) → ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) ) )
71 impexp ⊢ ( ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) ↔ ( 𝑓 finSupp 0 → ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) )
72 31 adantl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → 𝑓 : { 𝑋 } ⟶ 𝑆 )
73 snfi ⊢ { 𝑋 } ∈ Fin
74 73 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → { 𝑋 } ∈ Fin )
75 4 fvexi ⊢ 0 ∈ V
76 75 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → 0 ∈ V )
77 72 74 76 fdmfifsupp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → 𝑓 finSupp 0 )
78 pm2.27 ⊢ ( 𝑓 finSupp 0 → ( ( 𝑓 finSupp 0 → ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) )
79 77 78 syl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → ( ( 𝑓 finSupp 0 → ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) )
80 71 79 biimtrid ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ) → ( ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) → ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) )
81 80 ralimdva ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) → ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ) )
82 1 2 3 4 5 6 snlindsntorlem ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) → ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) )
83 81 82 syld ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) → ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) )
84 70 83 impbid ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ↔ ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) ) )
85 fveqeq2 ⊢ ( 𝑦 = 𝑋 → ( ( 𝑓 ‘ 𝑦 ) = 0 ↔ ( 𝑓 ‘ 𝑋 ) = 0 ) )
86 85 ralsng ⊢ ( 𝑋 ∈ 𝐵 → ( ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ↔ ( 𝑓 ‘ 𝑋 ) = 0 ) )
87 86 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ↔ ( 𝑓 ‘ 𝑋 ) = 0 ) )
88 87 bicomd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑓 ‘ 𝑋 ) = 0 ↔ ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ) )
89 88 imbi2d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) ↔ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ) ) )
90 89 ralbidv ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ( 𝑓 ‘ 𝑋 ) = 0 ) ↔ ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ) ) )
91 snelpwi ⊢ ( 𝑋 ∈ 𝐵 → { 𝑋 } ∈ 𝒫 𝐵 )
92 91 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → { 𝑋 } ∈ 𝒫 𝐵 )
93 92 biantrurd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ) ↔ ( { 𝑋 } ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ) ) ) )
94 84 90 93 3bitrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ↔ ( { 𝑋 } ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ) ) ) )
95 10 94 bitrid ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑠 ∈ ( 𝑆 ∖ { 0 } ) ( 𝑠 · 𝑋 ) ≠ 𝑍 ↔ ( { 𝑋 } ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ) ) ) )
96 snex ⊢ { 𝑋 } ∈ V
97 1 5 2 3 4 islininds ⊢ ( ( { 𝑋 } ∈ V ∧ 𝑀 ∈ LMod ) → ( { 𝑋 } linIndS 𝑀 ↔ ( { 𝑋 } ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ) ) ) )
98 96 11 97 sylancr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( { 𝑋 } linIndS 𝑀 ↔ ( { 𝑋 } ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) → ∀ 𝑦 ∈ { 𝑋 } ( 𝑓 ‘ 𝑦 ) = 0 ) ) ) )
99 95 98 bitr4d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑠 ∈ ( 𝑆 ∖ { 0 } ) ( 𝑠 · 𝑋 ) ≠ 𝑍 ↔ { 𝑋 } linIndS 𝑀 ) )