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 ∈ S LMIso T ∧ B ∈ J → F B ∈ K

Proof

Step Hyp Ref Expression
1 lmimlbs.j ⊢ J = LBasis ⁡ S
2 lmimlbs.k ⊢ K = LBasis ⁡ T
3 lmimlmhm ⊢ F ∈ S LMIso T → F ∈ S LMHom T
4 eqid ⊢ Base S = Base S
5 eqid ⊢ Base T = Base T
6 4 5 lmimf1o ⊢ F ∈ 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 ∈ S LMIso T → F : Base S ⟶ 1-1 Base T
9 1 lbslinds ⊢ J ⊆ LIndS ⁡ S
10 9 sseli ⊢ B ∈ J → B ∈ LIndS ⁡ S
11 4 5 lindsmm2 ⊢ F ∈ S LMHom T ∧ F : Base S ⟶ 1-1 Base T ∧ B ∈ LIndS ⁡ S → F B ∈ LIndS ⁡ T
12 3 8 10 11 syl2an3an ⊢ F ∈ S LMIso T ∧ B ∈ J → F B ∈ LIndS ⁡ T
13 eqid ⊢ LSpan ⁡ S = LSpan ⁡ S
14 4 1 13 lbssp ⊢ B ∈ J → LSpan ⁡ S ⁡ B = Base S
15 14 adantl ⊢ F ∈ S LMIso T ∧ B ∈ J → LSpan ⁡ S ⁡ B = Base S
16 15 imaeq2d ⊢ F ∈ S LMIso T ∧ B ∈ J → F LSpan ⁡ S ⁡ B = F Base S
17 4 1 lbsss ⊢ B ∈ J → B ⊆ Base S
18 eqid ⊢ LSpan ⁡ T = LSpan ⁡ T
19 4 13 18 lmhmlsp ⊢ F ∈ S LMHom T ∧ B ⊆ Base S → F LSpan ⁡ S ⁡ B = LSpan ⁡ T ⁡ F B
20 3 17 19 syl2an ⊢ F ∈ S LMIso T ∧ B ∈ J → F LSpan ⁡ S ⁡ B = LSpan ⁡ T ⁡ F B
21 6 adantr ⊢ F ∈ S LMIso T ∧ B ∈ 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 ∈ S LMIso T ∧ B ∈ J → F Base S = Base T
25 16 20 24 3eqtr3d ⊢ F ∈ S LMIso T ∧ B ∈ J → LSpan ⁡ T ⁡ F B = Base T
26 5 2 18 islbs4 ⊢ F B ∈ K ↔ F B ∈ LIndS ⁡ T ∧ LSpan ⁡ T ⁡ F B = Base T
27 12 25 26 sylanbrc ⊢ F ∈ S LMIso T ∧ B ∈ J → F B ∈ K