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

Metamath Proof Explorer

Theorem frlmdim

Description: Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypothesis frlmdim.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
Assertion frlmdim ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( dim ‘ 𝐹 ) = ( ♯ ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 frlmdim.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 1 frlmlvec ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → 𝐹 ∈ LVec )
3 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
4 eqid ⊢ ( 𝑅 unitVec 𝐼 ) = ( 𝑅 unitVec 𝐼 )
5 eqid ⊢ ( LBasis ‘ 𝐹 ) = ( LBasis ‘ 𝐹 )
6 1 4 5 frlmlbs ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ 𝐹 ) )
7 3 6 sylan ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ 𝐹 ) )
8 5 dimval ⊢ ( ( 𝐹 ∈ LVec ∧ ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ 𝐹 ) ) → ( dim ‘ 𝐹 ) = ( ♯ ‘ ran ( 𝑅 unitVec 𝐼 ) ) )
9 2 7 8 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( dim ‘ 𝐹 ) = ( ♯ ‘ ran ( 𝑅 unitVec 𝐼 ) ) )
10 simpr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑉 )
11 drngnzr ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
12 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
13 4 1 12 uvcf1 ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑉 ) → ( 𝑅 unitVec 𝐼 ) : 𝐼 –1-1→ ( Base ‘ 𝐹 ) )
14 11 13 sylan ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( 𝑅 unitVec 𝐼 ) : 𝐼 –1-1→ ( Base ‘ 𝐹 ) )
15 hashf1rn ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑅 unitVec 𝐼 ) : 𝐼 –1-1→ ( Base ‘ 𝐹 ) ) → ( ♯ ‘ ( 𝑅 unitVec 𝐼 ) ) = ( ♯ ‘ ran ( 𝑅 unitVec 𝐼 ) ) )
16 10 14 15 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑅 unitVec 𝐼 ) ) = ( ♯ ‘ ran ( 𝑅 unitVec 𝐼 ) ) )
17 mptexg ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ V )
18 17 ad2antlr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ V )
19 18 ralrimiva ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ∀ 𝑗 ∈ 𝐼 ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ V )
20 eqid ⊢ ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
21 20 fnmpt ⊢ ( ∀ 𝑗 ∈ 𝐼 ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ V → ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) Fn 𝐼 )
22 19 21 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) Fn 𝐼 )
23 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
24 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
25 4 23 24 uvcfval ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( 𝑅 unitVec 𝐼 ) = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
26 25 fneq1d ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( ( 𝑅 unitVec 𝐼 ) Fn 𝐼 ↔ ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) Fn 𝐼 ) )
27 22 26 mpbird ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( 𝑅 unitVec 𝐼 ) Fn 𝐼 )
28 hashfn ⊢ ( ( 𝑅 unitVec 𝐼 ) Fn 𝐼 → ( ♯ ‘ ( 𝑅 unitVec 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )
29 27 28 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑅 unitVec 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )
30 9 16 29 3eqtr2d ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( dim ‘ 𝐹 ) = ( ♯ ‘ 𝐼 ) )