Metamath Proof Explorer

Theorem el0ldep

Description: A set containing the zero element of a module is always linearly dependent, if the underlying ring has at least two elements. (Contributed by AV, 13-Apr-2019) (Revised by AV, 27-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion el0ldep 
|- ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> S linDepS M )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` M ) = ( Base ` M )
2 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
3 eqid 
 |-  ( 0g ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) )
4 eqid 
 |-  ( 1r ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) )
5 eqeq1 
 |-  ( s = y -> ( s = ( 0g ` M ) <-> y = ( 0g ` M ) ) )
6 5 ifbid 
 |-  ( s = y -> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) = if ( y = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) )
7 6 cbvmptv 
 |-  ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) = ( y e. S |-> if ( y = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) )
8 1 2 3 4 7 mptcfsupp 
 |-  ( ( M e. LMod /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) )
9 8 3adant1r 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) )
10 simp1l 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> M e. LMod )
11 simp2 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> S e. ~P ( Base ` M ) )
12 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
13 eqid 
 |-  ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) = ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) )
14 1 2 3 4 12 13 linc0scn0 
 |-  ( ( M e. LMod /\ S e. ~P ( Base ` M ) ) -> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) S ) = ( 0g ` M ) )
15 10 11 14 syl2anc 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) S ) = ( 0g ` M ) )
16 simp3 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( 0g ` M ) e. S )
17 fveq2 
 |-  ( x = ( 0g ` M ) -> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) = ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` ( 0g ` M ) ) )
18 17 neeq1d 
 |-  ( x = ( 0g ` M ) -> ( ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) =/= ( 0g ` ( Scalar ` M ) ) <-> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` ( 0g ` M ) ) =/= ( 0g ` ( Scalar ` M ) ) ) )
19 18 adantl 
 |-  ( ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) /\ x = ( 0g ` M ) ) -> ( ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) =/= ( 0g ` ( Scalar ` M ) ) <-> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` ( 0g ` M ) ) =/= ( 0g ` ( Scalar ` M ) ) ) )
20 iftrue 
 |-  ( s = ( 0g ` M ) -> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) = ( 1r ` ( Scalar ` M ) ) )
21 fvexd 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( 1r ` ( Scalar ` M ) ) e. _V )
22 13 20 16 21 fvmptd3 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` ( 0g ` M ) ) = ( 1r ` ( Scalar ` M ) ) )
23 2 lmodring 
 |-  ( M e. LMod -> ( Scalar ` M ) e. Ring )
24 23 anim1i 
 |-  ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) -> ( ( Scalar ` M ) e. Ring /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) )
25 24 3ad2ant1 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( ( Scalar ` M ) e. Ring /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) )
26 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
27 26 4 3 ring1ne0 
 |-  ( ( ( Scalar ` M ) e. Ring /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) -> ( 1r ` ( Scalar ` M ) ) =/= ( 0g ` ( Scalar ` M ) ) )
28 25 27 syl 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( 1r ` ( Scalar ` M ) ) =/= ( 0g ` ( Scalar ` M ) ) )
29 22 28 eqnetrd 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` ( 0g ` M ) ) =/= ( 0g ` ( Scalar ` M ) ) )
30 16 19 29 rspcedvd 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> E. x e. S ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) =/= ( 0g ` ( Scalar ` M ) ) )
31 2 26 4 lmod1cl 
 |-  ( M e. LMod -> ( 1r ` ( Scalar ` M ) ) e. ( Base ` ( Scalar ` M ) ) )
32 2 26 3 lmod0cl 
 |-  ( M e. LMod -> ( 0g ` ( Scalar ` M ) ) e. ( Base ` ( Scalar ` M ) ) )
33 31 32 ifcld 
 |-  ( M e. LMod -> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) e. ( Base ` ( Scalar ` M ) ) )
34 33 adantr 
 |-  ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) -> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) e. ( Base ` ( Scalar ` M ) ) )
35 34 3ad2ant1 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) e. ( Base ` ( Scalar ` M ) ) )
36 35 adantr 
 |-  ( ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) /\ s e. S ) -> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) e. ( Base ` ( Scalar ` M ) ) )
37 36 fmpttd 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) : S --> ( Base ` ( Scalar ` M ) ) )
38 fvexd 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( Base ` ( Scalar ` M ) ) e. _V )
39 38 11 elmapd 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m S ) <-> ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) : S --> ( Base ` ( Scalar ` M ) ) ) )
40 37 39 mpbird 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m S ) )
41 breq1 
 |-  ( f = ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( f finSupp ( 0g ` ( Scalar ` M ) ) <-> ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) ) )
42 oveq1 
 |-  ( f = ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( f ( linC ` M ) S ) = ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) S ) )
43 42 eqeq1d 
 |-  ( f = ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( ( f ( linC ` M ) S ) = ( 0g ` M ) <-> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) S ) = ( 0g ` M ) ) )
44 fveq1 
 |-  ( f = ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( f ` x ) = ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) )
45 44 neeq1d 
 |-  ( f = ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( ( f ` x ) =/= ( 0g ` ( Scalar ` M ) ) <-> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) )
46 45 rexbidv 
 |-  ( f = ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( E. x e. S ( f ` x ) =/= ( 0g ` ( Scalar ` M ) ) <-> E. x e. S ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) )
47 41 43 46 3anbi123d 
 |-  ( f = ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) /\ E. x e. S ( f ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) <-> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) S ) = ( 0g ` M ) /\ E. x e. S ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) ) )
48 47 adantl 
 |-  ( ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) /\ f = ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ) -> ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) /\ E. x e. S ( f ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) <-> ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) S ) = ( 0g ` M ) /\ E. x e. S ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) ) )
49 40 48 rspcedv 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) S ) = ( 0g ` M ) /\ E. x e. S ( ( s e. S |-> if ( s = ( 0g ` M ) , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) -> E. f e. ( ( Base ` ( Scalar ` M ) ) ^m S ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) /\ E. x e. S ( f ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) ) )
50 9 15 30 49 mp3and 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> E. f e. ( ( Base ` ( Scalar ` M ) ) ^m S ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) /\ E. x e. S ( f ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) )
51 1 12 2 26 3 islindeps 
 |-  ( ( M e. LMod /\ S e. ~P ( Base ` M ) ) -> ( S linDepS M <-> E. f e. ( ( Base ` ( Scalar ` M ) ) ^m S ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) /\ E. x e. S ( f ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) ) )
52 10 11 51 syl2anc 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> ( S linDepS M <-> E. f e. ( ( Base ` ( Scalar ` M ) ) ^m S ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) S ) = ( 0g ` M ) /\ E. x e. S ( f ` x ) =/= ( 0g ` ( Scalar ` M ) ) ) ) )
53 50 52 mpbird 
 |-  ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` ( Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> S linDepS M )