Metamath Proof Explorer

Theorem lbslcic

Description: A module with a basis is isomorphic to a free module with the same cardinality. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses lbslcic.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lbslcic.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
Assertion lbslcic ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) → 𝑊 ≃𝑚 ( 𝐹 freeLMod 𝐼 ) )

Proof

Step Hyp Ref Expression
1 lbslcic.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 lbslcic.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
3 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) → 𝐼 ≈ 𝐵 )
4 bren ⊢ ( 𝐼 ≈ 𝐵 ↔ ∃ 𝑒 𝑒 : 𝐼 –1-1-onto→ 𝐵 )
5 3 4 sylib ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) → ∃ 𝑒 𝑒 : 𝐼 –1-1-onto→ 𝐵 )
6 eqid ⊢ ( 𝐹 freeLMod 𝐼 ) = ( 𝐹 freeLMod 𝐼 )
7 eqid ⊢ ( Base ‘ ( 𝐹 freeLMod 𝐼 ) ) = ( Base ‘ ( 𝐹 freeLMod 𝐼 ) )
8 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
9 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
10 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
11 eqid ⊢ ( 𝑥 ∈ ( Base ‘ ( 𝐹 freeLMod 𝐼 ) ) ↦ ( 𝑊 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) ) = ( 𝑥 ∈ ( Base ‘ ( 𝐹 freeLMod 𝐼 ) ) ↦ ( 𝑊 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) )
12 simpl1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → 𝑊 ∈ LMod )
13 relen ⊢ Rel ≈
14 13 brrelex1i ⊢ ( 𝐼 ≈ 𝐵 → 𝐼 ∈ V )
15 14 3ad2ant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) → 𝐼 ∈ V )
16 15 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → 𝐼 ∈ V )
17 1 a1i ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → 𝐹 = ( Scalar ‘ 𝑊 ) )
18 f1ofo ⊢ ( 𝑒 : 𝐼 –1-1-onto→ 𝐵 → 𝑒 : 𝐼 –onto→ 𝐵 )
19 18 adantl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → 𝑒 : 𝐼 –onto→ 𝐵 )
20 2 lbslinds ⊢ 𝐽 ⊆ ( LIndS ‘ 𝑊 )
21 20 sseli ⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ∈ ( LIndS ‘ 𝑊 ) )
22 21 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) → 𝐵 ∈ ( LIndS ‘ 𝑊 ) )
23 22 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → 𝐵 ∈ ( LIndS ‘ 𝑊 ) )
24 f1of1 ⊢ ( 𝑒 : 𝐼 –1-1-onto→ 𝐵 → 𝑒 : 𝐼 –1-1→ 𝐵 )
25 24 adantl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → 𝑒 : 𝐼 –1-1→ 𝐵 )
26 f1linds ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑒 : 𝐼 –1-1→ 𝐵 ) → 𝑒 LIndF 𝑊 )
27 12 23 25 26 syl3anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → 𝑒 LIndF 𝑊 )
28 8 2 10 lbssp ⊢ ( 𝐵 ∈ 𝐽 → ( ( LSpan ‘ 𝑊 ) ‘ 𝐵 ) = ( Base ‘ 𝑊 ) )
29 28 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝐵 ) = ( Base ‘ 𝑊 ) )
30 29 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝐵 ) = ( Base ‘ 𝑊 ) )
31 6 7 8 9 10 11 12 16 17 19 27 30 indlcim ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → ( 𝑥 ∈ ( Base ‘ ( 𝐹 freeLMod 𝐼 ) ) ↦ ( 𝑊 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) ) ∈ ( ( 𝐹 freeLMod 𝐼 ) LMIso 𝑊 ) )
32 lmimcnv ⊢ ( ( 𝑥 ∈ ( Base ‘ ( 𝐹 freeLMod 𝐼 ) ) ↦ ( 𝑊 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) ) ∈ ( ( 𝐹 freeLMod 𝐼 ) LMIso 𝑊 ) → ◡ ( 𝑥 ∈ ( Base ‘ ( 𝐹 freeLMod 𝐼 ) ) ↦ ( 𝑊 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) ) ∈ ( 𝑊 LMIso ( 𝐹 freeLMod 𝐼 ) ) )
33 brlmici ⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ ( 𝐹 freeLMod 𝐼 ) ) ↦ ( 𝑊 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) ) ∈ ( 𝑊 LMIso ( 𝐹 freeLMod 𝐼 ) ) → 𝑊 ≃𝑚 ( 𝐹 freeLMod 𝐼 ) )
34 31 32 33 3syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) ∧ 𝑒 : 𝐼 –1-1-onto→ 𝐵 ) → 𝑊 ≃𝑚 ( 𝐹 freeLMod 𝐼 ) )
35 5 34 exlimddv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵 ) → 𝑊 ≃𝑚 ( 𝐹 freeLMod 𝐼 ) )