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

Metamath Proof Explorer

Theorem matdim

Description: Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypotheses matdim.a ⊢ 𝐴 = ( 𝐼 Mat 𝑅 )
matdim.n ⊢ 𝑁 = ( ♯ ‘ 𝐼 )
Assertion matdim ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( dim ‘ 𝐴 ) = ( 𝑁 · 𝑁 ) )

Proof

Step Hyp Ref Expression
1 matdim.a ⊢ 𝐴 = ( 𝐼 Mat 𝑅 )
2 matdim.n ⊢ 𝑁 = ( ♯ ‘ 𝐼 )
3 simpr ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → 𝑅 ∈ DivRing )
4 simpl ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → 𝐼 ∈ Fin )
5 xpfi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( 𝐼 × 𝐼 ) ∈ Fin )
6 4 4 5 syl2anc ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( 𝐼 × 𝐼 ) ∈ Fin )
7 eqid ⊢ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) = ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) )
8 7 frlmdim ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐼 × 𝐼 ) ∈ Fin ) → ( dim ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( ♯ ‘ ( 𝐼 × 𝐼 ) ) )
9 3 6 8 syl2anc ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( dim ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( ♯ ‘ ( 𝐼 × 𝐼 ) ) )
10 1 7 matbas ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( Base ‘ 𝐴 ) )
11 10 eqcomd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) )
12 eqidd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 ) )
13 ssidd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( Base ‘ 𝐴 ) ⊆ ( Base ‘ 𝐴 ) )
14 1 7 matplusg ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( +g ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( +g ‘ 𝐴 ) )
15 14 oveqdr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 ( +g ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
16 7 frlmlvec ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐼 × 𝐼 ) ∈ Fin ) → ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ∈ LVec )
17 3 6 16 syl2anc ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ∈ LVec )
18 lveclmod ⊢ ( ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ∈ LVec → ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ∈ LMod )
19 17 18 syl ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ∈ LMod )
20 19 adantr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ∈ LMod )
21 simprl ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
22 1 7 matsca ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( Scalar ‘ 𝐴 ) )
23 22 fveq2d ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
24 23 eqcomd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) ) )
25 24 adantr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) ) )
26 21 25 eleqtrd ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) ) )
27 simprr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
28 11 adantr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) )
29 27 28 eleqtrd ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) )
30 eqid ⊢ ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) )
31 eqid ⊢ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) )
32 eqid ⊢ ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) )
33 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) )
34 30 31 32 33 lmodvscl ⊢ ( ( ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) 𝑦 ) ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) )
35 20 26 29 34 syl3anc ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) 𝑦 ) ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) )
36 35 28 eleqtrrd ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) 𝑦 ) ∈ ( Base ‘ 𝐴 ) )
37 1 7 matvsca ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( ·𝑠 ‘ 𝐴 ) )
38 37 oveqdr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) )
39 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
40 eqidd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
41 22 fveq2d ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( +g ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) ) = ( +g ‘ ( Scalar ‘ 𝐴 ) ) )
42 41 oveqdr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ) → ( 𝑥 ( +g ‘ ( Scalar ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( Scalar ‘ 𝐴 ) ) 𝑦 ) )
43 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
44 1 matlmod ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
45 43 44 sylan2 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → 𝐴 ∈ LMod )
46 1 matsca2 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
47 46 3 eqeltrrd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( Scalar ‘ 𝐴 ) ∈ DivRing )
48 39 islvec ⊢ ( 𝐴 ∈ LVec ↔ ( 𝐴 ∈ LMod ∧ ( Scalar ‘ 𝐴 ) ∈ DivRing ) )
49 45 47 48 sylanbrc ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → 𝐴 ∈ LVec )
50 11 12 13 15 36 38 31 39 24 40 42 17 49 dimpropd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( dim ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( dim ‘ 𝐴 ) )
51 hashxp ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( ♯ ‘ ( 𝐼 × 𝐼 ) ) = ( ( ♯ ‘ 𝐼 ) · ( ♯ ‘ 𝐼 ) ) )
52 4 4 51 syl2anc ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( ♯ ‘ ( 𝐼 × 𝐼 ) ) = ( ( ♯ ‘ 𝐼 ) · ( ♯ ‘ 𝐼 ) ) )
53 9 50 52 3eqtr3d ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( dim ‘ 𝐴 ) = ( ( ♯ ‘ 𝐼 ) · ( ♯ ‘ 𝐼 ) ) )
54 2 2 oveq12i ⊢ ( 𝑁 · 𝑁 ) = ( ( ♯ ‘ 𝐼 ) · ( ♯ ‘ 𝐼 ) )
55 53 54 eqtr4di ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing ) → ( dim ‘ 𝐴 ) = ( 𝑁 · 𝑁 ) )