Metamath Proof Explorer

Theorem isldepslvec2

Description: Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 holds, so that both definitions are equivalent (see theorem 1.6 in Roman p. 46 and the note in Roman p. 112: if a nontrivial linear combination of elements (where not all of the coefficients are 0) in an R-vector space is 0, then and only then each of the elements is a linear combination of the others. (Contributed by AV, 30-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses islindeps2.b 
|- B = ( Base ` M )
islindeps2.z 
|- Z = ( 0g ` M )
islindeps2.r 
|- R = ( Scalar ` M )
islindeps2.e 
|- E = ( Base ` R )
islindeps2.0 
|- .0. = ( 0g ` R )
Assertion isldepslvec2 
|- ( ( M e. LVec /\ S e. ~P B ) -> ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> S linDepS M ) )

Proof

Step Hyp Ref Expression
1 islindeps2.b 
 |-  B = ( Base ` M )
2 islindeps2.z 
 |-  Z = ( 0g ` M )
3 islindeps2.r 
 |-  R = ( Scalar ` M )
4 islindeps2.e 
 |-  E = ( Base ` R )
5 islindeps2.0 
 |-  .0. = ( 0g ` R )
6 lveclmod 
 |-  ( M e. LVec -> M e. LMod )
7 6 adantr 
 |-  ( ( M e. LVec /\ S e. ~P B ) -> M e. LMod )
8 simpr 
 |-  ( ( M e. LVec /\ S e. ~P B ) -> S e. ~P B )
9 3 lvecdrng 
 |-  ( M e. LVec -> R e. DivRing )
10 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
11 9 10 syl 
 |-  ( M e. LVec -> R e. NzRing )
12 11 adantr 
 |-  ( ( M e. LVec /\ S e. ~P B ) -> R e. NzRing )
13 1 2 3 4 5 islindeps2 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) -> S linDepS M ) )
14 7 8 12 13 syl3anc 
 |-  ( ( M e. LVec /\ S e. ~P B ) -> ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) -> S linDepS M ) )
15 1 2 3 4 5 islindeps 
 |-  ( ( M e. LVec /\ S e. ~P B ) -> ( S linDepS M <-> E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) ) )
16 df-3an 
 |-  ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) <-> ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ E. s e. S ( g ` s ) =/= .0. ) )
17 r19.42v 
 |-  ( E. s e. S ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) <-> ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ E. s e. S ( g ` s ) =/= .0. ) )
18 16 17 bitr4i 
 |-  ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) <-> E. s e. S ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
19 18 rexbii 
 |-  ( E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) <-> E. g e. ( E ^m S ) E. s e. S ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
20 rexcom 
 |-  ( E. g e. ( E ^m S ) E. s e. S ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) <-> E. s e. S E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
21 19 20 bitri 
 |-  ( E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) <-> E. s e. S E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
22 simplr 
 |-  ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) -> S e. ~P B )
23 6 ad2antrr 
 |-  ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) -> M e. LMod )
24 simpr 
 |-  ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) -> s e. S )
25 22 23 24 3jca 
 |-  ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) -> ( S e. ~P B /\ M e. LMod /\ s e. S ) )
26 25 ad2antrr 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( S e. ~P B /\ M e. LMod /\ s e. S ) )
27 simplr 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> g e. ( E ^m S ) )
28 elmapi 
 |-  ( g e. ( E ^m S ) -> g : S --> E )
29 ffvelrn 
 |-  ( ( g : S --> E /\ s e. S ) -> ( g ` s ) e. E )
30 28 24 29 syl2anr 
 |-  ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) -> ( g ` s ) e. E )
31 simpr 
 |-  ( ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) -> ( g ` s ) =/= .0. )
32 30 31 anim12i 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( ( g ` s ) e. E /\ ( g ` s ) =/= .0. ) )
33 9 ad2antrr 
 |-  ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) -> R e. DivRing )
34 33 ad2antrr 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> R e. DivRing )
35 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
36 4 35 5 drngunit 
 |-  ( R e. DivRing -> ( ( g ` s ) e. ( Unit ` R ) <-> ( ( g ` s ) e. E /\ ( g ` s ) =/= .0. ) ) )
37 34 36 syl 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( ( g ` s ) e. ( Unit ` R ) <-> ( ( g ` s ) e. E /\ ( g ` s ) =/= .0. ) ) )
38 32 37 mpbird 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( g ` s ) e. ( Unit ` R ) )
39 simpll 
 |-  ( ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) -> g finSupp .0. )
40 39 adantl 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> g finSupp .0. )
41 eqid 
 |-  ( invg ` R ) = ( invg ` R )
42 eqid 
 |-  ( invr ` R ) = ( invr ` R )
43 eqid 
 |-  ( .r ` R ) = ( .r ` R )
44 eqid 
 |-  ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) = ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) )
45 1 3 4 35 5 2 41 42 43 44 lincresunit2 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ s e. S ) /\ ( g e. ( E ^m S ) /\ ( g ` s ) e. ( Unit ` R ) /\ g finSupp .0. ) ) -> ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) finSupp .0. )
46 26 27 38 40 45 syl13anc 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) finSupp .0. )
47 simpll 
 |-  ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) -> M e. LVec )
48 22 47 24 3jca 
 |-  ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) -> ( S e. ~P B /\ M e. LVec /\ s e. S ) )
49 48 ad2antrr 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( S e. ~P B /\ M e. LVec /\ s e. S ) )
50 simprr 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( g ` s ) =/= .0. )
51 simplr 
 |-  ( ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) -> ( g ( linC ` M ) S ) = Z )
52 51 adantl 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( g ( linC ` M ) S ) = Z )
53 fveq2 
 |-  ( z = y -> ( g ` z ) = ( g ` y ) )
54 53 oveq2d 
 |-  ( z = y -> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) = ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` y ) ) )
55 54 cbvmptv 
 |-  ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) = ( y e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` y ) ) )
56 1 3 4 35 5 2 41 42 43 55 lincreslvec3 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ s e. S ) /\ ( g e. ( E ^m S ) /\ ( g ` s ) =/= .0. /\ g finSupp .0. ) /\ ( g ( linC ` M ) S ) = Z ) -> ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) ( linC ` M ) ( S \ { s } ) ) = s )
57 49 27 50 40 52 56 syl131anc 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) ( linC ` M ) ( S \ { s } ) ) = s )
58 1 3 4 35 5 2 41 42 43 44 lincresunit1 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ s e. S ) /\ ( g e. ( E ^m S ) /\ ( g ` s ) e. ( Unit ` R ) ) ) -> ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) e. ( E ^m ( S \ { s } ) ) )
59 26 27 38 58 syl12anc 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) e. ( E ^m ( S \ { s } ) ) )
60 breq1 
 |-  ( f = ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) -> ( f finSupp .0. <-> ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) finSupp .0. ) )
61 oveq1 
 |-  ( f = ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) -> ( f ( linC ` M ) ( S \ { s } ) ) = ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) ( linC ` M ) ( S \ { s } ) ) )
62 61 eqeq1d 
 |-  ( f = ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) -> ( ( f ( linC ` M ) ( S \ { s } ) ) = s <-> ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) ( linC ` M ) ( S \ { s } ) ) = s ) )
63 60 62 anbi12d 
 |-  ( f = ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) -> ( ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) finSupp .0. /\ ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) ( linC ` M ) ( S \ { s } ) ) = s ) ) )
64 63 adantl 
 |-  ( ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) /\ f = ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) ) -> ( ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) finSupp .0. /\ ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) ( linC ` M ) ( S \ { s } ) ) = s ) ) )
65 59 64 rspcedv 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> ( ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) finSupp .0. /\ ( ( z e. ( S \ { s } ) |-> ( ( ( invr ` R ) ` ( ( invg ` R ) ` ( g ` s ) ) ) ( .r ` R ) ( g ` z ) ) ) ( linC ` M ) ( S \ { s } ) ) = s ) -> E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) )
66 46 57 65 mp2and 
 |-  ( ( ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) /\ g e. ( E ^m S ) ) /\ ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) -> E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) )
67 66 rexlimdva2 
 |-  ( ( ( M e. LVec /\ S e. ~P B ) /\ s e. S ) -> ( E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) -> E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) )
68 67 reximdva 
 |-  ( ( M e. LVec /\ S e. ~P B ) -> ( E. s e. S E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) -> E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) )
69 21 68 syl5bi 
 |-  ( ( M e. LVec /\ S e. ~P B ) -> ( E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) -> E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) )
70 15 69 sylbid 
 |-  ( ( M e. LVec /\ S e. ~P B ) -> ( S linDepS M -> E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) )
71 14 70 impbid 
 |-  ( ( M e. LVec /\ S e. ~P B ) -> ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> S linDepS M ) )