Metamath Proof Explorer

Theorem islbs5

Description: An equivalent formulation of the basis predicate in a vector space, using a function F for generating the base. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses islbs5.b 
|- B = ( Base ` W )
islbs5.k 
|- K = ( Base ` S )
islbs5.r 
|- S = ( Scalar ` W )
islbs5.t 
|- .x. = ( .s ` W )
islbs5.z 
|- O = ( 0g ` W )
islbs5.y 
|- .0. = ( 0g ` S )
islbs5.j 
|- J = ( LBasis ` W )
islbs5.n 
|- N = ( LSpan ` W )
islbs5.w 
|- ( ph -> W e. LMod )
islbs5.s 
|- ( ph -> S e. NzRing )
islbs5.i 
|- ( ph -> I e. V )
islbs5.f 
|- ( ph -> F : I -1-1-> B )
Assertion islbs5 
|- ( ph -> ( ran F e. ( LBasis ` W ) <-> ( A. a e. ( K ^m I ) ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) /\ ( N ` ran F ) = B ) ) )

Proof

Step Hyp Ref Expression
1 islbs5.b 
 |-  B = ( Base ` W )
2 islbs5.k 
 |-  K = ( Base ` S )
3 islbs5.r 
 |-  S = ( Scalar ` W )
4 islbs5.t 
 |-  .x. = ( .s ` W )
5 islbs5.z 
 |-  O = ( 0g ` W )
6 islbs5.y 
 |-  .0. = ( 0g ` S )
7 islbs5.j 
 |-  J = ( LBasis ` W )
8 islbs5.n 
 |-  N = ( LSpan ` W )
9 islbs5.w 
 |-  ( ph -> W e. LMod )
10 islbs5.s 
 |-  ( ph -> S e. NzRing )
11 islbs5.i 
 |-  ( ph -> I e. V )
12 islbs5.f 
 |-  ( ph -> F : I -1-1-> B )
13 eqid 
 |-  ( Base ` F ) = ( Base ` F )
14 1 13 3 4 5 6 8 9 10 11 12 lindflbs 
 |-  ( ph -> ( ran F e. ( LBasis ` W ) <-> ( F LIndF W /\ ( N ` ran F ) = B ) ) )
15 f1f 
 |-  ( F : I -1-1-> B -> F : I --> B )
16 12 15 syl 
 |-  ( ph -> F : I --> B )
17 eqid 
 |-  ( Base ` ( S freeLMod I ) ) = ( Base ` ( S freeLMod I ) )
18 1 3 4 5 6 17 islindf4 
 |-  ( ( W e. LMod /\ I e. V /\ F : I --> B ) -> ( F LIndF W <-> A. a e. ( Base ` ( S freeLMod I ) ) ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) )
19 9 11 16 18 syl3anc 
 |-  ( ph -> ( F LIndF W <-> A. a e. ( Base ` ( S freeLMod I ) ) ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) )
20 10 elexd 
 |-  ( ph -> S e. _V )
21 eqid 
 |-  ( S freeLMod I ) = ( S freeLMod I )
22 21 2 6 17 frlmelbas 
 |-  ( ( S e. _V /\ I e. V ) -> ( a e. ( Base ` ( S freeLMod I ) ) <-> ( a e. ( K ^m I ) /\ a finSupp .0. ) ) )
23 20 11 22 syl2anc 
 |-  ( ph -> ( a e. ( Base ` ( S freeLMod I ) ) <-> ( a e. ( K ^m I ) /\ a finSupp .0. ) ) )
24 23 imbi1d 
 |-  ( ph -> ( ( a e. ( Base ` ( S freeLMod I ) ) -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) <-> ( ( a e. ( K ^m I ) /\ a finSupp .0. ) -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) ) )
25 impexp 
 |-  ( ( ( a e. ( K ^m I ) /\ a finSupp .0. ) -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) <-> ( a e. ( K ^m I ) -> ( a finSupp .0. -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) ) )
26 impexp 
 |-  ( ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) <-> ( a finSupp .0. -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) )
27 26 a1i 
 |-  ( ph -> ( ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) <-> ( a finSupp .0. -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) ) )
28 27 bicomd 
 |-  ( ph -> ( ( a finSupp .0. -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) <-> ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) ) )
29 28 imbi2d 
 |-  ( ph -> ( ( a e. ( K ^m I ) -> ( a finSupp .0. -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) ) <-> ( a e. ( K ^m I ) -> ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) ) ) )
30 25 29 bitrid 
 |-  ( ph -> ( ( ( a e. ( K ^m I ) /\ a finSupp .0. ) -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) <-> ( a e. ( K ^m I ) -> ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) ) ) )
31 24 30 bitrd 
 |-  ( ph -> ( ( a e. ( Base ` ( S freeLMod I ) ) -> ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) ) <-> ( a e. ( K ^m I ) -> ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) ) ) )
32 31 ralbidv2 
 |-  ( ph -> ( A. a e. ( Base ` ( S freeLMod I ) ) ( ( W gsum ( a oF .x. F ) ) = O -> a = ( I X. { .0. } ) ) <-> A. a e. ( K ^m I ) ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) ) )
33 19 32 bitrd 
 |-  ( ph -> ( F LIndF W <-> A. a e. ( K ^m I ) ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) ) )
34 33 anbi1d 
 |-  ( ph -> ( ( F LIndF W /\ ( N ` ran F ) = B ) <-> ( A. a e. ( K ^m I ) ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) /\ ( N ` ran F ) = B ) ) )
35 14 34 bitrd 
 |-  ( ph -> ( ran F e. ( LBasis ` W ) <-> ( A. a e. ( K ^m I ) ( ( a finSupp .0. /\ ( W gsum ( a oF .x. F ) ) = O ) -> a = ( I X. { .0. } ) ) /\ ( N ` ran F ) = B ) ) )