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 ⊢ F = R freeLMod I
indlcim.b ⊢ B = Base F
indlcim.c ⊢ C = Base T
indlcim.v ⊢ · ˙ = ⋅ T
indlcim.n ⊢ N = LSpan ⁡ T
indlcim.e ⊢ E = x ∈ B ⟼ ∑ T x · ˙ f A
indlcim.t ⊢ φ → T ∈ LMod
indlcim.i ⊢ φ → I ∈ X
indlcim.r ⊢ φ → R = Scalar ⁡ T
indlcim.a ⊢ φ → A : I ⟶ onto J
indlcim.l ⊢ φ → A LIndF T
indlcim.s ⊢ φ → N ⁡ J = C
Assertion indlcim ⊢ φ → E ∈ F LMIso T

Proof

Step Hyp Ref Expression
1 indlcim.f ⊢ F = R freeLMod I
2 indlcim.b ⊢ B = Base F
3 indlcim.c ⊢ C = Base T
4 indlcim.v ⊢ · ˙ = ⋅ T
5 indlcim.n ⊢ N = LSpan ⁡ T
6 indlcim.e ⊢ E = x ∈ B ⟼ ∑ T x · ˙ f A
7 indlcim.t ⊢ φ → T ∈ LMod
8 indlcim.i ⊢ φ → I ∈ X
9 indlcim.r ⊢ φ → R = Scalar ⁡ T
10 indlcim.a ⊢ φ → A : I ⟶ onto J
11 indlcim.l ⊢ φ → A LIndF T
12 indlcim.s ⊢ φ → N ⁡ J = C
13 fofn ⊢ A : I ⟶ onto J → A Fn I
14 10 13 syl ⊢ φ → A Fn I
15 3 lindff ⊢ A LIndF T ∧ T ∈ LMod → A : dom ⁡ A ⟶ C
16 11 7 15 syl2anc ⊢ φ → A : dom ⁡ A ⟶ C
17 16 frnd ⊢ φ → ran ⁡ A ⊆ C
18 df-f ⊢ A : I ⟶ C ↔ A Fn I ∧ ran ⁡ A ⊆ C
19 14 17 18 sylanbrc ⊢ φ → A : I ⟶ C
20 1 2 3 4 6 7 8 9 19 frlmup1 ⊢ φ → E ∈ F LMHom T
21 1 2 3 4 6 7 8 9 19 islindf5 ⊢ φ → A LIndF T ↔ E : B ⟶ 1-1 C
22 11 21 mpbid ⊢ φ → E : B ⟶ 1-1 C
23 1 2 3 4 6 7 8 9 19 5 frlmup3 ⊢ φ → ran ⁡ E = N ⁡ ran ⁡ A
24 forn ⊢ A : I ⟶ onto J → ran ⁡ A = J
25 10 24 syl ⊢ φ → ran ⁡ A = J
26 25 fveq2d ⊢ φ → N ⁡ ran ⁡ A = N ⁡ J
27 23 26 12 3eqtrd ⊢ φ → ran ⁡ E = C
28 dff1o5 ⊢ E : B ⟶ 1-1 onto C ↔ E : B ⟶ 1-1 C ∧ ran ⁡ E = C
29 22 27 28 sylanbrc ⊢ φ → E : B ⟶ 1-1 onto C
30 2 3 islmim ⊢ E ∈ F LMIso T ↔ E ∈ F LMHom T ∧ E : B ⟶ 1-1 onto C
31 20 29 30 sylanbrc ⊢ φ → E ∈ F LMIso T