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