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 bilani 
 |-  ( ( ( ( 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 } ) )
19 snelpwi 
 |-  ( X e. ( Base ` M ) -> { X } e. ~P ( Base ` M ) )
20 19 1 eleq2s 
 |-  ( X e. B -> { X } e. ~P ( Base ` M ) )
21 20 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 ) )
22 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 ) ) ) )
23 13 18 21 22 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 ) ) ) )
24 23 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 ) )
25 24 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 ) ) )
26 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
27 26 grpmndd 
 |-  ( M e. LMod -> M e. Mnd )
28 27 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 )
29 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 )
30 elmapi 
 |-  ( f e. ( S ^m { X } ) -> f : { X } --> S )
31 12 adantl 
 |-  ( ( f : { X } --> S /\ ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) ) -> M e. LMod )
32 snidg 
 |-  ( X e. B -> X e. { X } )
33 32 adantl 
 |-  ( ( M e. LMod /\ X e. B ) -> X e. { X } )
34 33 adantr 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> X e. { X } )
35 ffvelcdm 
 |-  ( ( f : { X } --> S /\ X e. { X } ) -> ( f ` X ) e. S )
36 34 35 sylan2 
 |-  ( ( f : { X } --> S /\ ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) ) -> ( f ` X ) e. S )
37 simprlr 
 |-  ( ( f : { X } --> S /\ ( ( M e. LMod /\ X e. B ) /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) ) -> X e. B )
38 eqid 
 |-  ( .s ` M ) = ( .s ` M )
39 1 2 38 3 lmodvscl 
 |-  ( ( M e. LMod /\ ( f ` X ) e. S /\ X e. B ) -> ( ( f ` X ) ( .s ` M ) X ) e. B )
40 31 36 37 39 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 )
41 40 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 ) )
42 30 41 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 ) )
43 42 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 )
44 fveq2 
 |-  ( x = X -> ( f ` x ) = ( f ` X ) )
45 id 
 |-  ( x = X -> x = X )
46 44 45 oveq12d 
 |-  ( x = X -> ( ( f ` x ) ( .s ` M ) x ) = ( ( f ` X ) ( .s ` M ) X ) )
47 1 46 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 ) )
48 28 29 43 47 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 ) )
49 48 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 ) )
50 32 35 sylan2 
 |-  ( ( f : { X } --> S /\ X e. B ) -> ( f ` X ) e. S )
51 50 expcom 
 |-  ( X e. B -> ( f : { X } --> S -> ( f ` X ) e. S ) )
52 51 adantl 
 |-  ( ( M e. LMod /\ X e. B ) -> ( f : { X } --> S -> ( f ` X ) e. S ) )
53 6 oveqi 
 |-  ( ( f ` X ) .x. X ) = ( ( f ` X ) ( .s ` M ) X )
54 53 eqeq1i 
 |-  ( ( ( f ` X ) .x. X ) = Z <-> ( ( f ` X ) ( .s ` M ) X ) = Z )
55 oveq1 
 |-  ( s = ( f ` X ) -> ( s .x. X ) = ( ( f ` X ) .x. X ) )
56 55 eqeq1d 
 |-  ( s = ( f ` X ) -> ( ( s .x. X ) = Z <-> ( ( f ` X ) .x. X ) = Z ) )
57 eqeq1 
 |-  ( s = ( f ` X ) -> ( s = .0. <-> ( f ` X ) = .0. ) )
58 56 57 imbi12d 
 |-  ( s = ( f ` X ) -> ( ( ( s .x. X ) = Z -> s = .0. ) <-> ( ( ( f ` X ) .x. X ) = Z -> ( f ` X ) = .0. ) ) )
59 58 rspcva 
 |-  ( ( ( f ` X ) e. S /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> ( ( ( f ` X ) .x. X ) = Z -> ( f ` X ) = .0. ) )
60 54 59 biimtrrid 
 |-  ( ( ( f ` X ) e. S /\ A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) -> ( ( ( f ` X ) ( .s ` M ) X ) = Z -> ( f ` X ) = .0. ) )
61 60 ex 
 |-  ( ( f ` X ) e. S -> ( A. s e. S ( ( s .x. X ) = Z -> s = .0. ) -> ( ( ( f ` X ) ( .s ` M ) X ) = Z -> ( f ` X ) = .0. ) ) )
62 30 52 61 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. ) ) ) )
63 62 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. ) ) ) )
64 63 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. ) )
65 49 64 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. ) )
66 65 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. ) )
67 25 66 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. ) )
68 67 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. ) )
69 68 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. ) ) )
70 impexp 
 |-  ( ( ( f finSupp .0. /\ ( f ( linC ` M ) { X } ) = Z ) -> ( f ` X ) = .0. ) <-> ( f finSupp .0. -> ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) )
71 30 adantl 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> f : { X } --> S )
72 snfi 
 |-  { X } e. Fin
73 72 a1i 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> { X } e. Fin )
74 4 fvexi 
 |-  .0. e. _V
75 74 a1i 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> .0. e. _V )
76 71 73 75 fdmfifsupp 
 |-  ( ( ( M e. LMod /\ X e. B ) /\ f e. ( S ^m { X } ) ) -> f finSupp .0. )
77 pm2.27 
 |-  ( f finSupp .0. -> ( ( f finSupp .0. -> ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) -> ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) ) )
78 76 77 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. ) ) )
79 70 78 biimtrid 
 |-  ( ( ( 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 79 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. ) ) )
81 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. ) ) )
82 80 81 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. ) ) )
83 69 82 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. ) ) )
84 fveqeq2 
 |-  ( y = X -> ( ( f ` y ) = .0. <-> ( f ` X ) = .0. ) )
85 84 ralsng 
 |-  ( X e. B -> ( A. y e. { X } ( f ` y ) = .0. <-> ( f ` X ) = .0. ) )
86 85 adantl 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. y e. { X } ( f ` y ) = .0. <-> ( f ` X ) = .0. ) )
87 86 bicomd 
 |-  ( ( M e. LMod /\ X e. B ) -> ( ( f ` X ) = .0. <-> A. y e. { X } ( f ` y ) = .0. ) )
88 87 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. ) ) )
89 88 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. ) ) )
90 snelpwi 
 |-  ( X e. B -> { X } e. ~P B )
91 90 adantl 
 |-  ( ( M e. LMod /\ X e. B ) -> { X } e. ~P B )
92 91 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. ) ) ) )
93 83 89 92 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. ) ) ) )
94 10 93 bitrid 
 |-  ( ( 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. ) ) ) )
95 snex 
 |-  { X } e. _V
96 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. ) ) ) )
97 95 11 96 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. ) ) ) )
98 94 97 bitr4d 
 |-  ( ( M e. LMod /\ X e. B ) -> ( A. s e. ( S \ { .0. } ) ( s .x. X ) =/= Z <-> { X } linIndS M ) )