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 
|- B = ( Base ` M )
snlindsntor.r 
|- R = ( Scalar ` M )
snlindsntor.s 
|- S = ( Base ` R )
snlindsntor.0 
|- .0. = ( 0g ` R )
snlindsntor.z 
|- Z = ( 0g ` M )
snlindsntor.t 
|- .x. = ( .s ` M )
Assertion snlindsntor 
|- ( ( M e. LMod /\ X e. B ) -> ( A. s e. ( S \ { .0. } ) ( s .x. X ) =/= Z <-> { 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 
 |-  .0. = ( 0g ` R )
5 snlindsntor.z 
 |-  Z = ( 0g ` M )
6 snlindsntor.t 
 |-  .x. = ( .s ` M )
7 df-ne 
 |-  ( ( s .x. X ) =/= Z <-> -. ( s .x. X ) = Z )
8 7 ralbii 
 |-  ( A. s e. ( S \ { .0. } ) ( s .x. X ) =/= Z <-> A. s e. ( S \ { .0. } ) -. ( s .x. X ) = Z )
9 raldifsni 
 |-  ( A. s e. ( S \ { .0. } ) -. ( s .x. X ) = Z <-> A. s e. S ( ( s .x. X ) = Z -> s = .0. ) )
10 8 9 bitri 
 |-  ( A. s e. ( S \ { .0. } ) ( s .x. X ) =/= Z <-> A. s e. S ( ( s .x. X ) = Z -> s = .0. ) )
11 simpl 
 |-  ( ( M e. LMod /\ X e. B ) -> M e. LMod )
12 11 adantr 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> M e. LMod )
13 12 adantr 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> M e. LMod )
14 2 fveq2i 
 |-  ( Base ` R ) = ( Base ` ( Scalar ` M ) )
15 3 14 eqtri 
 |-  S = ( Base ` ( Scalar ` M ) )
16 15 oveq1i 
 |-  ( S ^m { X } ) = ( ( Base ` ( Scalar ` M ) ) ^m { X } )
17 16 eleq2i 
 |-  ( f e. ( S ^m { X } ) <-> f e. ( ( Base ` ( Scalar ` M ) ) ^m { X } ) )
18 17 biimpi 
 |-  ( f e. ( S ^m { X } ) -> f e. ( ( Base ` ( Scalar ` M ) ) ^m { X } ) )
19 18 adantl 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> f e. ( ( Base ` ( Scalar ` M ) ) ^m { X } ) )
20 snelpwi 
 |-  ( X e. ( Base ` M ) -> { X } e. ~P ( Base ` M ) )
21 20 1 eleq2s 
 |-  ( X e. B -> { X } e. ~P ( Base ` M ) )
22 21 ad3antlr 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> { X } e. ~P ( Base ` M ) )
23 lincval 
 |-  ( ( M e. LMod /\ f e. ( ( Base ` ( Scalar ` M ) ) ^m { X } ) /\ { X } e. ~P ( Base ` M ) ) -> ( f ( linC ` M ) { X } ) = ( M gsum ( x e. { X } |-> ( ( f ` x ) ( .s ` M ) x ) ) ) )
24 13 19 22 23 syl3anc 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( f ( linC ` M ) { X } ) = ( M gsum ( x e. { X } |-> ( ( f ` x ) ( .s ` M ) x ) ) ) )
25 24 eqeq1d 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( ( f ( linC ` M ) { X } ) = Z <-> ( M gsum ( x e. { X } |-> ( ( f ` x ) ( .s ` M ) x ) ) ) = Z ) )
26 25 anbi2d 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) <-> ( f finSupp .0. /\ ( M gsum ( x e. { X } |-> ( ( f ` x ) ( .s ` M ) x ) ) ) = Z ) ) )
27 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
28 27 grpmndd 
 |-  ( M e. LMod -> M e. Mnd )
29 28 ad3antrrr 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> M e. Mnd )
30 simpllr 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> X e. B )
31 elmapi 
 |-  ( f e. ( S ^m { X } ) -> f : { X } --> S )
32 12 adantl 
 |-  ( ( f : { X } --> S /\ ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) ) -> M e. LMod )
33 snidg 
 |-  ( X e. B -> X e. { X } )
34 33 adantl 
 |-  ( ( M e. LMod /\ X e. B ) -> X e. { X } )
35 34 adantr 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> X e. { X } )
36 ffvelrn 
 |-  ( ( f : { X } --> S /\ X e. { X } ) -> ( f ` X ) e. S )
37 35 36 sylan2 
 |-  ( ( f : { X } --> S /\ ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) ) -> ( f ` X ) e. S )
38 simprlr 
 |-  ( ( f : { X } --> S /\ ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) ) -> X e. B )
39 eqid 
 |-  ( .s ` M ) = ( .s ` M )
40 1 2 39 3 lmodvscl 
 |-  ( ( M e. LMod /\ ( f ` X ) e. S /\ X e. B ) -> ( ( f ` X ) ( .s ` M ) X ) e. B )
41 32 37 38 40 syl3anc 
 |-  ( ( f : { X } --> S /\ ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) ) -> ( ( f ` X ) ( .s ` M ) X ) e. B )
42 41 expcom 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> ( f : { X } --> S -> ( ( f ` X ) ( .s ` M ) X ) e. B ) )
43 31 42 syl5com 
 |-  ( f e. ( S ^m { X } ) -> ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> ( ( f ` X ) ( .s ` M ) X ) e. B ) )
44 43 impcom 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( ( f ` X ) ( .s ` M ) X ) e. B )
45 fveq2 
 |-  ( x = X -> ( f ` x ) = ( f ` X ) )
46 id 
 |-  ( x = X -> x = X )
47 45 46 oveq12d 
 |-  ( x = X -> ( ( f ` x ) ( .s ` M ) x ) = ( ( f ` X ) ( .s ` M ) X ) )
48 1 47 gsumsn 
 |-  ( ( M e. Mnd /\ X e. B /\ ( ( f ` X ) ( .s ` M ) X ) e. B ) -> ( M gsum ( x e. { X } |-> ( ( f ` x ) ( .s ` M ) x ) ) ) = ( ( f ` X ) ( .s ` M ) X ) )
49 29 30 44 48 syl3anc 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( M gsum ( x e. { X } |-> ( ( f ` x ) ( .s ` M ) x ) ) ) = ( ( f ` X ) ( .s ` M ) X ) )
50 49 eqeq1d 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( ( M gsum ( x e. { X } |-> ( ( f ` x ) ( .s ` M ) x ) ) ) = Z <-> ( ( f ` X ) ( .s ` M ) X ) = Z ) )
51 33 36 sylan2 
 |-  ( ( f : { X } --> S /\ X e. B ) -> ( f ` X ) e. S )
52 51 expcom 
 |-  ( X e. B -> ( f : { X } --> S -> ( f ` X ) e. S ) )
53 52 adantl 
 |-  ( ( M e. LMod /\ X e. B ) -> ( f : { X } --> S -> ( f ` X ) e. S ) )
54 6 oveqi 
 |-  ( ( f ` X ) .x. X ) = ( ( f ` X ) ( .s ` M ) X )
55 54 eqeq1i 
 |-  ( ( ( f ` X ) .x. X ) = Z <-> ( ( f ` X ) ( .s ` M ) X ) = Z )
56 oveq1 
 |-  ( s = ( f ` X ) -> ( s .x. X ) = ( ( f ` X ) .x. X ) )
57 56 eqeq1d 
 |-  ( s = ( f ` X ) -> ( ( s .x. X ) = Z <-> ( ( f ` X ) .x. X ) = Z ) )
58 eqeq1 
 |-  ( s = ( f ` X ) -> ( s = .0. <-> ( f ` X ) = .0. ) )
59 57 58 imbi12d 
 |-  ( s = ( f ` X ) -> ( ( ( s .x. X ) = Z -> s = .0. ) <-> ( ( ( f ` X ) .x. X ) = Z -> ( f ` X ) = .0. ) ) )
60 59 rspcva 
 |-  ( ( ( f ` X ) e. S /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> ( ( ( f ` X ) .x. X ) = Z -> ( f ` X ) = .0. ) )
61 55 60 syl5bir 
 |-  ( ( ( f ` X ) e. S /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> ( ( ( f ` X ) ( .s ` M ) X ) = Z -> ( f ` X ) = .0. ) )
62 61 ex 
 |-  ( ( f ` X ) e. S -> ( A. s e. S ( ( s .x. X ) = Z -> s = .0. ) -> ( ( ( f ` X ) ( .s ` M ) X ) = Z -> ( f ` X ) = .0. ) ) )
63 31 53 62 syl56 
 |-  ( ( M e. LMod /\ X e. B ) -> ( f e. ( S ^m { X } ) -> ( A. s e. S ( ( s .x. X ) = Z -> s = .0. ) -> ( ( ( f ` X ) ( .s ` M ) X ) = Z -> ( f ` X ) = .0. ) ) ) )
64 63 com23 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. s e. S ( ( s .x. X ) = Z -> s = .0. ) -> ( f e. ( S ^m { X } ) -> ( ( ( f ` X ) ( .s ` M ) X ) = Z -> ( f ` X ) = .0. ) ) ) )
65 64 imp31 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( ( ( f ` X ) ( .s ` M ) X ) = Z -> ( f ` X ) = .0. ) )
66 50 65 sylbid 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( ( M gsum ( x e. { X } |-> ( ( f ` x ) ( .s ` M ) x ) ) ) = Z -> ( f ` X ) = .0. ) )
67 66 adantld 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( ( f finSupp .0. /\ ( M gsum ( x e. { X } |-> ( ( f ` x ) ( .s ` M ) x ) ) ) = Z ) -> ( f ` X ) = .0. ) )
68 26 67 sylbid 
 |-  ( ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) /\ f e. ( S ^m { X } ) ) -> ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) )
69 68 ralrimiva 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) )
70 69 ex 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. s e. S ( ( s .x. X ) = Z -> s = .0. ) -> A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) ) )
71 impexp 
 |-  ( ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) <-> ( f finSupp .0. -> ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) )
72 31 adantl 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> f : { X } --> S )
73 snfi 
 |-  { X } e. Fin
74 73 a1i 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> { X } e. Fin )
75 4 fvexi 
 |-  .0. e. _V
76 75 a1i 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> .0. e. _V )
77 72 74 76 fdmfifsupp 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> f finSupp .0. )
78 pm2.27 
 |-  ( f finSupp .0. -> ( ( f finSupp .0. -> ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) -> ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) )
79 77 78 syl 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> ( ( f finSupp .0. -> ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) -> ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) )
80 71 79 syl5bi 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> ( ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) -> ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) )
81 80 ralimdva 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) -> A. f e. ( S ^m { X } ) ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) )
82 1 2 3 4 5 6 snlindsntorlem 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. f e. ( S ^m { X } ) ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) -> A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) )
83 81 82 syld 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) -> A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) )
84 70 83 impbid 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. s e. S ( ( s .x. X ) = Z -> s = .0. ) <-> A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) ) )
85 fveqeq2 
 |-  ( y = X -> ( ( f ` y ) = .0. <-> ( f ` X ) = .0. ) )
86 85 ralsng 
 |-  ( X e. B -> ( A. y e. { X } ( f ` y ) = .0. <-> ( f ` X ) = .0. ) )
87 86 adantl 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. y e. { X } ( f ` y ) = .0. <-> ( f ` X ) = .0. ) )
88 87 bicomd 
 |-  ( ( M e. LMod /\ X e. B ) -> ( ( f ` X ) = .0. <-> A. y e. { X } ( f ` y ) = .0. ) )
89 88 imbi2d 
 |-  ( ( M e. LMod /\ X e. B ) -> ( ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) <-> ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> A. y e. { X } ( f ` y ) = .0. ) ) )
90 89 ralbidv 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) <-> A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> A. y e. { X } ( f ` y ) = .0. ) ) )
91 snelpwi 
 |-  ( X e. B -> { X } e. ~P B )
92 91 adantl 
 |-  ( ( M e. LMod /\ X e. B ) -> { X } e. ~P B )
93 92 biantrurd 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> A. y e. { X } ( f ` y ) = .0. ) <-> ( { X } e. ~P B /\ A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> A. y e. { X } ( f ` y ) = .0. ) ) ) )
94 84 90 93 3bitrd 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. s e. S ( ( s .x. X ) = Z -> s = .0. ) <-> ( { X } e. ~P B /\ A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> A. y e. { X } ( f ` y ) = .0. ) ) ) )
95 10 94 syl5bb 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. s e. ( S \ { .0. } ) ( s .x. X ) =/= Z <-> ( { X } e. ~P B /\ A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> A. y e. { X } ( f ` y ) = .0. ) ) ) )
96 snex 
 |-  { X } e. _V
97 1 5 2 3 4 islininds 
 |-  ( ( { X } e. _V /\ M e. LMod ) -> ( { X } linIndS M <-> ( { X } e. ~P B /\ A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> A. y e. { X } ( f ` y ) = .0. ) ) ) )
98 96 11 97 sylancr 
 |-  ( ( M e. LMod /\ X e. B ) -> ( { X } linIndS M <-> ( { X } e. ~P B /\ A. f e. ( S ^m { X } ) ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> A. y e. { X } ( f ` y ) = .0. ) ) ) )
99 95 98 bitr4d 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. s e. ( S \ { .0. } ) ( s .x. X ) =/= Z <-> { X } linIndS M ) )