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 𝑇 ) )