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 ‘ 𝐹 ) = ( ♯ ‘ 𝐼 ) )