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=LBasisS
lmimlbs.k K=LBasisT
Assertion lmimlbs FSLMIsoTBJFBK

Proof

Step Hyp Ref Expression
1 lmimlbs.j J=LBasisS
2 lmimlbs.k K=LBasisT
3 lmimlmhm FSLMIsoTFSLMHomT
4 eqid BaseS=BaseS
5 eqid BaseT=BaseT
6 4 5 lmimf1o FSLMIsoTF:BaseS1-1 ontoBaseT
7 f1of1 F:BaseS1-1 ontoBaseTF:BaseS1-1BaseT
8 6 7 syl FSLMIsoTF:BaseS1-1BaseT
9 1 lbslinds JLIndSS
10 9 sseli BJBLIndSS
11 4 5 lindsmm2 FSLMHomTF:BaseS1-1BaseTBLIndSSFBLIndST
12 3 8 10 11 syl2an3an FSLMIsoTBJFBLIndST
13 eqid LSpanS=LSpanS
14 4 1 13 lbssp BJLSpanSB=BaseS
15 14 adantl FSLMIsoTBJLSpanSB=BaseS
16 15 imaeq2d FSLMIsoTBJFLSpanSB=FBaseS
17 4 1 lbsss BJBBaseS
18 eqid LSpanT=LSpanT
19 4 13 18 lmhmlsp FSLMHomTBBaseSFLSpanSB=LSpanTFB
20 3 17 19 syl2an FSLMIsoTBJFLSpanSB=LSpanTFB
21 6 adantr FSLMIsoTBJF:BaseS1-1 ontoBaseT
22 f1ofo F:BaseS1-1 ontoBaseTF:BaseSontoBaseT
23 foima F:BaseSontoBaseTFBaseS=BaseT
24 21 22 23 3syl FSLMIsoTBJFBaseS=BaseT
25 16 20 24 3eqtr3d FSLMIsoTBJLSpanTFB=BaseT
26 5 2 18 islbs4 FBKFBLIndSTLSpanTFB=BaseT
27 12 25 26 sylanbrc FSLMIsoTBJFBK