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 ⊢ 𝐽 = ( LBasis ‘ 𝑆 )
lmimlbs.k ⊢ 𝐾 = ( LBasis ‘ 𝑇 )
Assertion lmimlbs ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐵 ∈ 𝐽 ) → ( 𝐹 “ 𝐵 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 lmimlbs.j ⊢ 𝐽 = ( LBasis ‘ 𝑆 )
2 lmimlbs.k ⊢ 𝐾 = ( LBasis ‘ 𝑇 )
3 lmimlmhm ⊢ ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
4 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
6 4 5 lmimf1o ⊢ ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) )
7 f1of1 ⊢ ( 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) –1-1→ ( Base ‘ 𝑇 ) )
8 6 7 syl ⊢ ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) –1-1→ ( Base ‘ 𝑇 ) )
9 1 lbslinds ⊢ 𝐽 ⊆ ( LIndS ‘ 𝑆 )
10 9 sseli ⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ∈ ( LIndS ‘ 𝑆 ) )
11 4 5 lindsmm2 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : ( Base ‘ 𝑆 ) –1-1→ ( Base ‘ 𝑇 ) ∧ 𝐵 ∈ ( LIndS ‘ 𝑆 ) ) → ( 𝐹 “ 𝐵 ) ∈ ( LIndS ‘ 𝑇 ) )
12 3 8 10 11 syl2an3an ⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐵 ∈ 𝐽 ) → ( 𝐹 “ 𝐵 ) ∈ ( LIndS ‘ 𝑇 ) )
13 eqid ⊢ ( LSpan ‘ 𝑆 ) = ( LSpan ‘ 𝑆 )
14 4 1 13 lbssp ⊢ ( 𝐵 ∈ 𝐽 → ( ( LSpan ‘ 𝑆 ) ‘ 𝐵 ) = ( Base ‘ 𝑆 ) )
15 14 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐵 ∈ 𝐽 ) → ( ( LSpan ‘ 𝑆 ) ‘ 𝐵 ) = ( Base ‘ 𝑆 ) )
16 15 imaeq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐵 ∈ 𝐽 ) → ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝐵 ) ) = ( 𝐹 “ ( Base ‘ 𝑆 ) ) )
17 4 1 lbsss ⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
18 eqid ⊢ ( LSpan ‘ 𝑇 ) = ( LSpan ‘ 𝑇 )
19 4 13 18 lmhmlsp ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐵 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝐵 ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝐵 ) ) )
20 3 17 19 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐵 ∈ 𝐽 ) → ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝐵 ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝐵 ) ) )
21 6 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐵 ∈ 𝐽 ) → 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) )
22 f1ofo ⊢ ( 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) –onto→ ( Base ‘ 𝑇 ) )
23 foima ⊢ ( 𝐹 : ( Base ‘ 𝑆 ) –onto→ ( Base ‘ 𝑇 ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) = ( Base ‘ 𝑇 ) )
24 21 22 23 3syl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐵 ∈ 𝐽 ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) = ( Base ‘ 𝑇 ) )
25 16 20 24 3eqtr3d ⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐵 ∈ 𝐽 ) → ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝐵 ) ) = ( Base ‘ 𝑇 ) )
26 5 2 18 islbs4 ⊢ ( ( 𝐹 “ 𝐵 ) ∈ 𝐾 ↔ ( ( 𝐹 “ 𝐵 ) ∈ ( LIndS ‘ 𝑇 ) ∧ ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝐵 ) ) = ( Base ‘ 𝑇 ) ) )
27 12 25 26 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐵 ∈ 𝐽 ) → ( 𝐹 “ 𝐵 ) ∈ 𝐾 )