Metamath Proof Explorer

Theorem lmimlbs

Description: The isomorphic image of a basis is a basis. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses lmimlbs.j 
|- J = ( LBasis ` S )
lmimlbs.k 
|- K = ( LBasis ` T )
Assertion lmimlbs 
|- ( ( F e. ( S LMIso T ) /\ B e. J ) -> ( F " B ) e. K )

Proof

Step Hyp Ref Expression
1 lmimlbs.j 
 |-  J = ( LBasis ` S )
2 lmimlbs.k 
 |-  K = ( LBasis ` T )
3 lmimlmhm 
 |-  ( F e. ( S LMIso T ) -> F e. ( S LMHom T ) )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 eqid 
 |-  ( Base ` T ) = ( Base ` T )
6 4 5 lmimf1o 
 |-  ( F e. ( S LMIso T ) -> F : ( Base ` S ) -1-1-onto-> ( Base ` T ) )
7 f1of1 
 |-  ( F : ( Base ` S ) -1-1-onto-> ( Base ` T ) -> F : ( Base ` S ) -1-1-> ( Base ` T ) )
8 6 7 syl 
 |-  ( F e. ( S LMIso T ) -> F : ( Base ` S ) -1-1-> ( Base ` T ) )
9 1 lbslinds 
 |-  J C_ ( LIndS ` S )
10 9 sseli 
 |-  ( B e. J -> B e. ( LIndS ` S ) )
11 4 5 lindsmm2 
 |-  ( ( F e. ( S LMHom T ) /\ F : ( Base ` S ) -1-1-> ( Base ` T ) /\ B e. ( LIndS ` S ) ) -> ( F " B ) e. ( LIndS ` T ) )
12 3 8 10 11 syl2an3an 
 |-  ( ( F e. ( S LMIso T ) /\ B e. J ) -> ( F " B ) e. ( LIndS ` T ) )
13 eqid 
 |-  ( LSpan ` S ) = ( LSpan ` S )
14 4 1 13 lbssp 
 |-  ( B e. J -> ( ( LSpan ` S ) ` B ) = ( Base ` S ) )
15 14 adantl 
 |-  ( ( F e. ( S LMIso T ) /\ B e. J ) -> ( ( LSpan ` S ) ` B ) = ( Base ` S ) )
16 15 imaeq2d 
 |-  ( ( F e. ( S LMIso T ) /\ B e. J ) -> ( F " ( ( LSpan ` S ) ` B ) ) = ( F " ( Base ` S ) ) )
17 4 1 lbsss 
 |-  ( B e. J -> B C_ ( Base ` S ) )
18 eqid 
 |-  ( LSpan ` T ) = ( LSpan ` T )
19 4 13 18 lmhmlsp 
 |-  ( ( F e. ( S LMHom T ) /\ B C_ ( Base ` S ) ) -> ( F " ( ( LSpan ` S ) ` B ) ) = ( ( LSpan ` T ) ` ( F " B ) ) )
20 3 17 19 syl2an 
 |-  ( ( F e. ( S LMIso T ) /\ B e. J ) -> ( F " ( ( LSpan ` S ) ` B ) ) = ( ( LSpan ` T ) ` ( F " B ) ) )
21 6 adantr 
 |-  ( ( F e. ( S LMIso T ) /\ B e. J ) -> F : ( Base ` S ) -1-1-onto-> ( Base ` T ) )
22 f1ofo 
 |-  ( F : ( Base ` S ) -1-1-onto-> ( Base ` T ) -> F : ( Base ` S ) -onto-> ( Base ` T ) )
23 foima 
 |-  ( F : ( Base ` S ) -onto-> ( Base ` T ) -> ( F " ( Base ` S ) ) = ( Base ` T ) )
24 21 22 23 3syl 
 |-  ( ( F e. ( S LMIso T ) /\ B e. J ) -> ( F " ( Base ` S ) ) = ( Base ` T ) )
25 16 20 24 3eqtr3d 
 |-  ( ( F e. ( S LMIso T ) /\ B e. J ) -> ( ( LSpan ` T ) ` ( F " B ) ) = ( Base ` T ) )
26 5 2 18 islbs4 
 |-  ( ( F " B ) e. K <-> ( ( F " B ) e. ( LIndS ` T ) /\ ( ( LSpan ` T ) ` ( F " B ) ) = ( Base ` T ) ) )
27 12 25 26 sylanbrc 
 |-  ( ( F e. ( S LMIso T ) /\ B e. J ) -> ( F " B ) e. K )