Metamath Proof Explorer

Theorem islinds5

Description: A set is linearly independent if and only if it has no non-trivial representations of zero. (Contributed by Thierry Arnoux, 18-May-2023)

Ref Expression
Hypotheses islinds5.b 
|- B = ( Base ` W )
islinds5.k 
|- K = ( Base ` F )
islinds5.r 
|- F = ( Scalar ` W )
islinds5.t 
|- .x. = ( .s ` W )
islinds5.z 
|- O = ( 0g ` W )
islinds5.y 
|- .0. = ( 0g ` F )
Assertion islinds5 
|- ( ( W e. LMod /\ V C_ B ) -> ( V e. ( LIndS ` W ) <-> A. a e. ( K ^m V ) ( ( a finSupp .0. /\ ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O ) -> a = ( V X. { .0. } ) ) ) )

Proof

Step Hyp Ref Expression
1 islinds5.b 
 |-  B = ( Base ` W )
2 islinds5.k 
 |-  K = ( Base ` F )
3 islinds5.r 
 |-  F = ( Scalar ` W )
4 islinds5.t 
 |-  .x. = ( .s ` W )
5 islinds5.z 
 |-  O = ( 0g ` W )
6 islinds5.y 
 |-  .0. = ( 0g ` F )
7 1 islinds 
 |-  ( W e. LMod -> ( V e. ( LIndS ` W ) <-> ( V C_ B /\ ( _I |` V ) LIndF W ) ) )
8 7 baibd 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( V e. ( LIndS ` W ) <-> ( _I |` V ) LIndF W ) )
9 simpl 
 |-  ( ( W e. LMod /\ V C_ B ) -> W e. LMod )
10 1 fvexi 
 |-  B e. _V
11 10 a1i 
 |-  ( ( W e. LMod /\ V C_ B ) -> B e. _V )
12 simpr 
 |-  ( ( W e. LMod /\ V C_ B ) -> V C_ B )
13 11 12 ssexd 
 |-  ( ( W e. LMod /\ V C_ B ) -> V e. _V )
14 f1oi 
 |-  ( _I |` V ) : V -1-1-onto-> V
15 f1of 
 |-  ( ( _I |` V ) : V -1-1-onto-> V -> ( _I |` V ) : V --> V )
16 14 15 mp1i 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( _I |` V ) : V --> V )
17 16 12 fssd 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( _I |` V ) : V --> B )
18 eqid 
 |-  ( Base ` ( F freeLMod V ) ) = ( Base ` ( F freeLMod V ) )
19 1 3 4 5 6 18 islindf4 
 |-  ( ( W e. LMod /\ V e. _V /\ ( _I |` V ) : V --> B ) -> ( ( _I |` V ) LIndF W <-> A. a e. ( Base ` ( F freeLMod V ) ) ( ( W gsum ( a oF .x. ( _I |` V ) ) ) = O -> a = ( V X. { .0. } ) ) ) )
20 9 13 17 19 syl3anc 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( ( _I |` V ) LIndF W <-> A. a e. ( Base ` ( F freeLMod V ) ) ( ( W gsum ( a oF .x. ( _I |` V ) ) ) = O -> a = ( V X. { .0. } ) ) ) )
21 3 fvexi 
 |-  F e. _V
22 eqid 
 |-  ( F freeLMod V ) = ( F freeLMod V )
23 22 2 6 18 frlmelbas 
 |-  ( ( F e. _V /\ V e. _V ) -> ( a e. ( Base ` ( F freeLMod V ) ) <-> ( a e. ( K ^m V ) /\ a finSupp .0. ) ) )
24 21 13 23 sylancr 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( a e. ( Base ` ( F freeLMod V ) ) <-> ( a e. ( K ^m V ) /\ a finSupp .0. ) ) )
25 24 imbi1d 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( ( a e. ( Base ` ( F freeLMod V ) ) -> ( ( W gsum ( a oF .x. ( _I |` V ) ) ) = O -> a = ( V X. { .0. } ) ) ) <-> ( ( a e. ( K ^m V ) /\ a finSupp .0. ) -> ( ( W gsum ( a oF .x. ( _I |` V ) ) ) = O -> a = ( V X. { .0. } ) ) ) ) )
26 elmapfn 
 |-  ( a e. ( K ^m V ) -> a Fn V )
27 26 ad2antrl 
 |-  ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) -> a Fn V )
28 17 adantr 
 |-  ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) -> ( _I |` V ) : V --> B )
29 28 ffnd 
 |-  ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) -> ( _I |` V ) Fn V )
30 13 adantr 
 |-  ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) -> V e. _V )
31 inidm 
 |-  ( V i^i V ) = V
32 eqidd 
 |-  ( ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) /\ v e. V ) -> ( a ` v ) = ( a ` v ) )
33 fvresi 
 |-  ( v e. V -> ( ( _I |` V ) ` v ) = v )
34 33 adantl 
 |-  ( ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) /\ v e. V ) -> ( ( _I |` V ) ` v ) = v )
35 27 29 30 30 31 32 34 offval 
 |-  ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) -> ( a oF .x. ( _I |` V ) ) = ( v e. V |-> ( ( a ` v ) .x. v ) ) )
36 35 oveq2d 
 |-  ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) -> ( W gsum ( a oF .x. ( _I |` V ) ) ) = ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) )
37 36 eqeq1d 
 |-  ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) -> ( ( W gsum ( a oF .x. ( _I |` V ) ) ) = O <-> ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O ) )
38 37 imbi1d 
 |-  ( ( ( W e. LMod /\ V C_ B ) /\ ( a e. ( K ^m V ) /\ a finSupp .0. ) ) -> ( ( ( W gsum ( a oF .x. ( _I |` V ) ) ) = O -> a = ( V X. { .0. } ) ) <-> ( ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O -> a = ( V X. { .0. } ) ) ) )
39 38 pm5.74da 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( ( ( a e. ( K ^m V ) /\ a finSupp .0. ) -> ( ( W gsum ( a oF .x. ( _I |` V ) ) ) = O -> a = ( V X. { .0. } ) ) ) <-> ( ( a e. ( K ^m V ) /\ a finSupp .0. ) -> ( ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O -> a = ( V X. { .0. } ) ) ) ) )
40 impexp 
 |-  ( ( ( a e. ( K ^m V ) /\ a finSupp .0. ) -> ( ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O -> a = ( V X. { .0. } ) ) ) <-> ( a e. ( K ^m V ) -> ( a finSupp .0. -> ( ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O -> a = ( V X. { .0. } ) ) ) ) )
41 impexp 
 |-  ( ( ( a finSupp .0. /\ ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O ) -> a = ( V X. { .0. } ) ) <-> ( a finSupp .0. -> ( ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O -> a = ( V X. { .0. } ) ) ) )
42 41 imbi2i 
 |-  ( ( a e. ( K ^m V ) -> ( ( a finSupp .0. /\ ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O ) -> a = ( V X. { .0. } ) ) ) <-> ( a e. ( K ^m V ) -> ( a finSupp .0. -> ( ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O -> a = ( V X. { .0. } ) ) ) ) )
43 40 42 bitr4i 
 |-  ( ( ( a e. ( K ^m V ) /\ a finSupp .0. ) -> ( ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O -> a = ( V X. { .0. } ) ) ) <-> ( a e. ( K ^m V ) -> ( ( a finSupp .0. /\ ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O ) -> a = ( V X. { .0. } ) ) ) )
44 43 a1i 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( ( ( a e. ( K ^m V ) /\ a finSupp .0. ) -> ( ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O -> a = ( V X. { .0. } ) ) ) <-> ( a e. ( K ^m V ) -> ( ( a finSupp .0. /\ ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O ) -> a = ( V X. { .0. } ) ) ) ) )
45 25 39 44 3bitrd 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( ( a e. ( Base ` ( F freeLMod V ) ) -> ( ( W gsum ( a oF .x. ( _I |` V ) ) ) = O -> a = ( V X. { .0. } ) ) ) <-> ( a e. ( K ^m V ) -> ( ( a finSupp .0. /\ ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O ) -> a = ( V X. { .0. } ) ) ) ) )
46 45 ralbidv2 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( A. a e. ( Base ` ( F freeLMod V ) ) ( ( W gsum ( a oF .x. ( _I |` V ) ) ) = O -> a = ( V X. { .0. } ) ) <-> A. a e. ( K ^m V ) ( ( a finSupp .0. /\ ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O ) -> a = ( V X. { .0. } ) ) ) )
47 8 20 46 3bitrd 
 |-  ( ( W e. LMod /\ V C_ B ) -> ( V e. ( LIndS ` W ) <-> A. a e. ( K ^m V ) ( ( a finSupp .0. /\ ( W gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) = O ) -> a = ( V X. { .0. } ) ) ) )