Metamath Proof Explorer

Theorem lindflbs

Description: Conditions for an independent family to be a basis. (Contributed by Thierry Arnoux, 21-Jul-2023)

Ref Expression
Hypotheses lindflbs.b 
|- B = ( Base ` W )
lindflbs.k 
|- K = ( Base ` F )
lindflbs.r 
|- S = ( Scalar ` W )
lindflbs.t 
|- .x. = ( .s ` W )
lindflbs.z 
|- O = ( 0g ` W )
lindflbs.y 
|- .0. = ( 0g ` S )
lindflbs.n 
|- N = ( LSpan ` W )
lindflbs.1 
|- ( ph -> W e. LMod )
lindflbs.2 
|- ( ph -> S e. NzRing )
lindflbs.3 
|- ( ph -> I e. V )
lindflbs.4 
|- ( ph -> F : I -1-1-> B )
Assertion lindflbs 
|- ( ph -> ( ran F e. ( LBasis ` W ) <-> ( F LIndF W /\ ( N ` ran F ) = B ) ) )

Proof

Step Hyp Ref Expression
1 lindflbs.b 
 |-  B = ( Base ` W )
2 lindflbs.k 
 |-  K = ( Base ` F )
3 lindflbs.r 
 |-  S = ( Scalar ` W )
4 lindflbs.t 
 |-  .x. = ( .s ` W )
5 lindflbs.z 
 |-  O = ( 0g ` W )
6 lindflbs.y 
 |-  .0. = ( 0g ` S )
7 lindflbs.n 
 |-  N = ( LSpan ` W )
8 lindflbs.1 
 |-  ( ph -> W e. LMod )
9 lindflbs.2 
 |-  ( ph -> S e. NzRing )
10 lindflbs.3 
 |-  ( ph -> I e. V )
11 lindflbs.4 
 |-  ( ph -> F : I -1-1-> B )
12 eqid 
 |-  ( LBasis ` W ) = ( LBasis ` W )
13 1 12 7 islbs4 
 |-  ( ran F e. ( LBasis ` W ) <-> ( ran F e. ( LIndS ` W ) /\ ( N ` ran F ) = B ) )
14 ssv 
 |-  ran F C_ _V
15 f1ssr 
 |-  ( ( F : I -1-1-> B /\ ran F C_ _V ) -> F : I -1-1-> _V )
16 11 14 15 sylancl 
 |-  ( ph -> F : I -1-1-> _V )
17 f1dm 
 |-  ( F : I -1-1-> B -> dom F = I )
18 f1eq2 
 |-  ( dom F = I -> ( F : dom F -1-1-> _V <-> F : I -1-1-> _V ) )
19 11 17 18 3syl 
 |-  ( ph -> ( F : dom F -1-1-> _V <-> F : I -1-1-> _V ) )
20 16 19 mpbird 
 |-  ( ph -> F : dom F -1-1-> _V )
21 3 islindf3 
 |-  ( ( W e. LMod /\ S e. NzRing ) -> ( F LIndF W <-> ( F : dom F -1-1-> _V /\ ran F e. ( LIndS ` W ) ) ) )
22 8 9 21 syl2anc 
 |-  ( ph -> ( F LIndF W <-> ( F : dom F -1-1-> _V /\ ran F e. ( LIndS ` W ) ) ) )
23 20 22 mpbirand 
 |-  ( ph -> ( F LIndF W <-> ran F e. ( LIndS ` W ) ) )
24 23 anbi1d 
 |-  ( ph -> ( ( F LIndF W /\ ( N ` ran F ) = B ) <-> ( ran F e. ( LIndS ` W ) /\ ( N ` ran F ) = B ) ) )
25 13 24 bitr4id 
 |-  ( ph -> ( ran F e. ( LBasis ` W ) <-> ( F LIndF W /\ ( N ` ran F ) = B ) ) )