| Step |
Hyp |
Ref |
Expression |
| 1 |
|
indlcim.f |
|- F = ( R freeLMod I ) |
| 2 |
|
indlcim.b |
|- B = ( Base ` F ) |
| 3 |
|
indlcim.c |
|- C = ( Base ` T ) |
| 4 |
|
indlcim.v |
|- .x. = ( .s ` T ) |
| 5 |
|
indlcim.n |
|- N = ( LSpan ` T ) |
| 6 |
|
indlcim.e |
|- E = ( x e. B |-> ( T gsum ( x oF .x. A ) ) ) |
| 7 |
|
indlcim.t |
|- ( ph -> T e. LMod ) |
| 8 |
|
indlcim.i |
|- ( ph -> I e. X ) |
| 9 |
|
indlcim.r |
|- ( ph -> R = ( Scalar ` T ) ) |
| 10 |
|
indlcim.a |
|- ( ph -> A : I -onto-> J ) |
| 11 |
|
indlcim.l |
|- ( ph -> A LIndF T ) |
| 12 |
|
indlcim.s |
|- ( ph -> ( N ` J ) = C ) |
| 13 |
|
fofn |
|- ( A : I -onto-> J -> A Fn I ) |
| 14 |
10 13
|
syl |
|- ( ph -> A Fn I ) |
| 15 |
3
|
lindff |
|- ( ( A LIndF T /\ T e. LMod ) -> A : dom A --> C ) |
| 16 |
11 7 15
|
syl2anc |
|- ( ph -> A : dom A --> C ) |
| 17 |
16
|
frnd |
|- ( ph -> ran A C_ C ) |
| 18 |
|
df-f |
|- ( A : I --> C <-> ( A Fn I /\ ran A C_ C ) ) |
| 19 |
14 17 18
|
sylanbrc |
|- ( ph -> A : I --> C ) |
| 20 |
1 2 3 4 6 7 8 9 19
|
frlmup1 |
|- ( ph -> E e. ( F LMHom T ) ) |
| 21 |
1 2 3 4 6 7 8 9 19
|
islindf5 |
|- ( ph -> ( A LIndF T <-> E : B -1-1-> C ) ) |
| 22 |
11 21
|
mpbid |
|- ( ph -> E : B -1-1-> C ) |
| 23 |
1 2 3 4 6 7 8 9 19 5
|
frlmup3 |
|- ( ph -> ran E = ( N ` ran A ) ) |
| 24 |
|
forn |
|- ( A : I -onto-> J -> ran A = J ) |
| 25 |
10 24
|
syl |
|- ( ph -> ran A = J ) |
| 26 |
25
|
fveq2d |
|- ( ph -> ( N ` ran A ) = ( N ` J ) ) |
| 27 |
23 26 12
|
3eqtrd |
|- ( ph -> ran E = C ) |
| 28 |
|
dff1o5 |
|- ( E : B -1-1-onto-> C <-> ( E : B -1-1-> C /\ ran E = C ) ) |
| 29 |
22 27 28
|
sylanbrc |
|- ( ph -> E : B -1-1-onto-> C ) |
| 30 |
2 3
|
islmim |
|- ( E e. ( F LMIso T ) <-> ( E e. ( F LMHom T ) /\ E : B -1-1-onto-> C ) ) |
| 31 |
20 29 30
|
sylanbrc |
|- ( ph -> E e. ( F LMIso T ) ) |