This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem indlcim

Description: An independent, spanning family extends to an isomorphism from a free module. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses indlcim.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
indlcim.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
indlcim.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
indlcim.v ⊢ · = ( ·𝑠 ‘ 𝑇 )
indlcim.n ⊢ 𝑁 = ( LSpan ‘ 𝑇 )
indlcim.e ⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) )
indlcim.t ⊢ ( 𝜑 → 𝑇 ∈ LMod )
indlcim.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
indlcim.r ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) )
indlcim.a ⊢ ( 𝜑 → 𝐴 : 𝐼 –onto→ 𝐽 )
indlcim.l ⊢ ( 𝜑 → 𝐴 LIndF 𝑇 )
indlcim.s ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐽 ) = 𝐶 )
Assertion indlcim ( 𝜑 → 𝐸 ∈ ( 𝐹 LMIso 𝑇 ) )

Proof

Step Hyp Ref Expression
1 indlcim.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 indlcim.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 indlcim.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
4 indlcim.v ⊢ · = ( ·𝑠 ‘ 𝑇 )
5 indlcim.n ⊢ 𝑁 = ( LSpan ‘ 𝑇 )
6 indlcim.e ⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) )
7 indlcim.t ⊢ ( 𝜑 → 𝑇 ∈ LMod )
8 indlcim.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
9 indlcim.r ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) )
10 indlcim.a ⊢ ( 𝜑 → 𝐴 : 𝐼 –onto→ 𝐽 )
11 indlcim.l ⊢ ( 𝜑 → 𝐴 LIndF 𝑇 )
12 indlcim.s ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐽 ) = 𝐶 )
13 fofn ⊢ ( 𝐴 : 𝐼 –onto→ 𝐽 → 𝐴 Fn 𝐼 )
14 10 13 syl ⊢ ( 𝜑 → 𝐴 Fn 𝐼 )
15 3 lindff ⊢ ( ( 𝐴 LIndF 𝑇 ∧ 𝑇 ∈ LMod ) → 𝐴 : dom 𝐴 ⟶ 𝐶 )
16 11 7 15 syl2anc ⊢ ( 𝜑 → 𝐴 : dom 𝐴 ⟶ 𝐶 )
17 16 frnd ⊢ ( 𝜑 → ran 𝐴 ⊆ 𝐶 )
18 df-f ⊢ ( 𝐴 : 𝐼 ⟶ 𝐶 ↔ ( 𝐴 Fn 𝐼 ∧ ran 𝐴 ⊆ 𝐶 ) )
19 14 17 18 sylanbrc ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐶 )
20 1 2 3 4 6 7 8 9 19 frlmup1 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) )
21 1 2 3 4 6 7 8 9 19 islindf5 ⊢ ( 𝜑 → ( 𝐴 LIndF 𝑇 ↔ 𝐸 : 𝐵 –1-1→ 𝐶 ) )
22 11 21 mpbid ⊢ ( 𝜑 → 𝐸 : 𝐵 –1-1→ 𝐶 )
23 1 2 3 4 6 7 8 9 19 5 frlmup3 ⊢ ( 𝜑 → ran 𝐸 = ( 𝑁 ‘ ran 𝐴 ) )
24 forn ⊢ ( 𝐴 : 𝐼 –onto→ 𝐽 → ran 𝐴 = 𝐽 )
25 10 24 syl ⊢ ( 𝜑 → ran 𝐴 = 𝐽 )
26 25 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ran 𝐴 ) = ( 𝑁 ‘ 𝐽 ) )
27 23 26 12 3eqtrd ⊢ ( 𝜑 → ran 𝐸 = 𝐶 )
28 dff1o5 ⊢ ( 𝐸 : 𝐵 –1-1-onto→ 𝐶 ↔ ( 𝐸 : 𝐵 –1-1→ 𝐶 ∧ ran 𝐸 = 𝐶 ) )
29 22 27 28 sylanbrc ⊢ ( 𝜑 → 𝐸 : 𝐵 –1-1-onto→ 𝐶 )
30 2 3 islmim ⊢ ( 𝐸 ∈ ( 𝐹 LMIso 𝑇 ) ↔ ( 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) ∧ 𝐸 : 𝐵 –1-1-onto→ 𝐶 ) )
31 20 29 30 sylanbrc ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 LMIso 𝑇 ) )