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