Metamath Proof Explorer

Theorem lindsrng01

Description: Any subset of a module is always linearly independent if the underlying ring has at most one element. Since the underlying ring cannot be the empty set (see lmodsn0 ), this means that the underlying ring has only one element, so it is a zero ring. (Contributed by AV, 14-Apr-2019) (Revised by AV, 27-Apr-2019)

Ref Expression
Hypotheses lindsrng01.b 
|- B = ( Base ` M )
lindsrng01.r 
|- R = ( Scalar ` M )
lindsrng01.e 
|- E = ( Base ` R )
Assertion lindsrng01 
|- ( ( M e. LMod /\ ( ( # ` E ) = 0 \/ ( # ` E ) = 1 ) /\ S e. ~P B ) -> S linIndS M )

Proof

Step Hyp Ref Expression
1 lindsrng01.b 
 |-  B = ( Base ` M )
2 lindsrng01.r 
 |-  R = ( Scalar ` M )
3 lindsrng01.e 
 |-  E = ( Base ` R )
4 2 3 lmodsn0 
 |-  ( M e. LMod -> E =/= (/) )
5 3 fvexi 
 |-  E e. _V
6 hasheq0 
 |-  ( E e. _V -> ( ( # ` E ) = 0 <-> E = (/) ) )
7 5 6 ax-mp 
 |-  ( ( # ` E ) = 0 <-> E = (/) )
8 eqneqall 
 |-  ( E = (/) -> ( E =/= (/) -> S linIndS M ) )
9 8 com12 
 |-  ( E =/= (/) -> ( E = (/) -> S linIndS M ) )
10 7 9 syl5bi 
 |-  ( E =/= (/) -> ( ( # ` E ) = 0 -> S linIndS M ) )
11 4 10 syl 
 |-  ( M e. LMod -> ( ( # ` E ) = 0 -> S linIndS M ) )
12 11 adantr 
 |-  ( ( M e. LMod /\ S e. ~P B ) -> ( ( # ` E ) = 0 -> S linIndS M ) )
13 12 com12 
 |-  ( ( # ` E ) = 0 -> ( ( M e. LMod /\ S e. ~P B ) -> S linIndS M ) )
14 2 lmodring 
 |-  ( M e. LMod -> R e. Ring )
15 14 adantr 
 |-  ( ( M e. LMod /\ S e. ~P B ) -> R e. Ring )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 3 16 0ring 
 |-  ( ( R e. Ring /\ ( # ` E ) = 1 ) -> E = { ( 0g ` R ) } )
18 15 17 sylan 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) -> E = { ( 0g ` R ) } )
19 simpr 
 |-  ( ( M e. LMod /\ S e. ~P B ) -> S e. ~P B )
20 19 adantr 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) -> S e. ~P B )
21 20 adantl 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> S e. ~P B )
22 snex 
 |-  { ( 0g ` R ) } e. _V
23 20 22 jctil 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) -> ( { ( 0g ` R ) } e. _V /\ S e. ~P B ) )
24 23 adantl 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> ( { ( 0g ` R ) } e. _V /\ S e. ~P B ) )
25 elmapg 
 |-  ( ( { ( 0g ` R ) } e. _V /\ S e. ~P B ) -> ( f e. ( { ( 0g ` R ) } ^m S ) <-> f : S --> { ( 0g ` R ) } ) )
26 24 25 syl 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> ( f e. ( { ( 0g ` R ) } ^m S ) <-> f : S --> { ( 0g ` R ) } ) )
27 fvex 
 |-  ( 0g ` R ) e. _V
28 27 fconst2 
 |-  ( f : S --> { ( 0g ` R ) } <-> f = ( S X. { ( 0g ` R ) } ) )
29 fconstmpt 
 |-  ( S X. { ( 0g ` R ) } ) = ( x e. S |-> ( 0g ` R ) )
30 29 eqeq2i 
 |-  ( f = ( S X. { ( 0g ` R ) } ) <-> f = ( x e. S |-> ( 0g ` R ) ) )
31 28 30 bitri 
 |-  ( f : S --> { ( 0g ` R ) } <-> f = ( x e. S |-> ( 0g ` R ) ) )
32 eqidd 
 |-  ( ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) /\ v e. S ) -> ( x e. S |-> ( 0g ` R ) ) = ( x e. S |-> ( 0g ` R ) ) )
33 eqidd 
 |-  ( ( ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) /\ v e. S ) /\ x = v ) -> ( 0g ` R ) = ( 0g ` R ) )
34 simpr 
 |-  ( ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) /\ v e. S ) -> v e. S )
35 fvexd 
 |-  ( ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) /\ v e. S ) -> ( 0g ` R ) e. _V )
36 32 33 34 35 fvmptd 
 |-  ( ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) /\ v e. S ) -> ( ( x e. S |-> ( 0g ` R ) ) ` v ) = ( 0g ` R ) )
37 36 ralrimiva 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> A. v e. S ( ( x e. S |-> ( 0g ` R ) ) ` v ) = ( 0g ` R ) )
38 37 a1d 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> ( ( ( x e. S |-> ( 0g ` R ) ) finSupp ( 0g ` R ) /\ ( ( x e. S |-> ( 0g ` R ) ) ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( ( x e. S |-> ( 0g ` R ) ) ` v ) = ( 0g ` R ) ) )
39 breq1 
 |-  ( f = ( x e. S |-> ( 0g ` R ) ) -> ( f finSupp ( 0g ` R ) <-> ( x e. S |-> ( 0g ` R ) ) finSupp ( 0g ` R ) ) )
40 oveq1 
 |-  ( f = ( x e. S |-> ( 0g ` R ) ) -> ( f ( linC ` M ) S ) = ( ( x e. S |-> ( 0g ` R ) ) ( linC ` M ) S ) )
41 40 eqeq1d 
 |-  ( f = ( x e. S |-> ( 0g ` R ) ) -> ( ( f ( linC ` M ) S ) = ( 0g ` M ) <-> ( ( x e. S |-> ( 0g ` R ) ) ( linC ` M ) S ) = ( 0g ` M ) ) )
42 39 41 anbi12d 
 |-  ( f = ( x e. S |-> ( 0g ` R ) ) -> ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) <-> ( ( x e. S |-> ( 0g ` R ) ) finSupp ( 0g ` R ) /\ ( ( x e. S |-> ( 0g ` R ) ) ( linC ` M ) S ) = ( 0g ` M ) ) ) )
43 fveq1 
 |-  ( f = ( x e. S |-> ( 0g ` R ) ) -> ( f ` v ) = ( ( x e. S |-> ( 0g ` R ) ) ` v ) )
44 43 eqeq1d 
 |-  ( f = ( x e. S |-> ( 0g ` R ) ) -> ( ( f ` v ) = ( 0g ` R ) <-> ( ( x e. S |-> ( 0g ` R ) ) ` v ) = ( 0g ` R ) ) )
45 44 ralbidv 
 |-  ( f = ( x e. S |-> ( 0g ` R ) ) -> ( A. v e. S ( f ` v ) = ( 0g ` R ) <-> A. v e. S ( ( x e. S |-> ( 0g ` R ) ) ` v ) = ( 0g ` R ) ) )
46 42 45 imbi12d 
 |-  ( f = ( x e. S |-> ( 0g ` R ) ) -> ( ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) <-> ( ( ( x e. S |-> ( 0g ` R ) ) finSupp ( 0g ` R ) /\ ( ( x e. S |-> ( 0g ` R ) ) ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( ( x e. S |-> ( 0g ` R ) ) ` v ) = ( 0g ` R ) ) ) )
47 38 46 syl5ibrcom 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> ( f = ( x e. S |-> ( 0g ` R ) ) -> ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) ) )
48 31 47 syl5bi 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> ( f : S --> { ( 0g ` R ) } -> ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) ) )
49 26 48 sylbid 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> ( f e. ( { ( 0g ` R ) } ^m S ) -> ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) ) )
50 49 ralrimiv 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> A. f e. ( { ( 0g ` R ) } ^m S ) ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) )
51 oveq1 
 |-  ( E = { ( 0g ` R ) } -> ( E ^m S ) = ( { ( 0g ` R ) } ^m S ) )
52 51 raleqdv 
 |-  ( E = { ( 0g ` R ) } -> ( A. f e. ( E ^m S ) ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) <-> A. f e. ( { ( 0g ` R ) } ^m S ) ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) ) )
53 52 adantr 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> ( A. f e. ( E ^m S ) ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) <-> A. f e. ( { ( 0g ` R ) } ^m S ) ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) ) )
54 50 53 mpbird 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> A. f e. ( E ^m S ) ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) )
55 simpl 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) -> ( M e. LMod /\ S e. ~P B ) )
56 55 ancomd 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) -> ( S e. ~P B /\ M e. LMod ) )
57 56 adantl 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> ( S e. ~P B /\ M e. LMod ) )
58 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
59 1 58 2 3 16 islininds 
 |-  ( ( S e. ~P B /\ M e. LMod ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) ) ) )
60 57 59 syl 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp ( 0g ` R ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) ) -> A. v e. S ( f ` v ) = ( 0g ` R ) ) ) ) )
61 21 54 60 mpbir2and 
 |-  ( ( E = { ( 0g ` R ) } /\ ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) ) -> S linIndS M )
62 18 61 mpancom 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( # ` E ) = 1 ) -> S linIndS M )
63 62 expcom 
 |-  ( ( # ` E ) = 1 -> ( ( M e. LMod /\ S e. ~P B ) -> S linIndS M ) )
64 13 63 jaoi 
 |-  ( ( ( # ` E ) = 0 \/ ( # ` E ) = 1 ) -> ( ( M e. LMod /\ S e. ~P B ) -> S linIndS M ) )
65 64 expd 
 |-  ( ( ( # ` E ) = 0 \/ ( # ` E ) = 1 ) -> ( M e. LMod -> ( S e. ~P B -> S linIndS M ) ) )
66 65 com12 
 |-  ( M e. LMod -> ( ( ( # ` E ) = 0 \/ ( # ` E ) = 1 ) -> ( S e. ~P B -> S linIndS M ) ) )
67 66 3imp 
 |-  ( ( M e. LMod /\ ( ( # ` E ) = 0 \/ ( # ` E ) = 1 ) /\ S e. ~P B ) -> S linIndS M )