| 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 ) ) ) |