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 
|- A = ( I Mat R )
matdim.n 
|- N = ( # ` I )
Assertion matdim 
|- ( ( I e. Fin /\ R e. DivRing ) -> ( dim ` A ) = ( N x. N ) )

Proof

Step Hyp Ref Expression
1 matdim.a 
 |-  A = ( I Mat R )
2 matdim.n 
 |-  N = ( # ` I )
3 simpr 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> R e. DivRing )
4 simpl 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> I e. Fin )
5 xpfi 
 |-  ( ( I e. Fin /\ I e. Fin ) -> ( I X. I ) e. Fin )
6 4 4 5 syl2anc 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( I X. I ) e. Fin )
7 eqid 
 |-  ( R freeLMod ( I X. I ) ) = ( R freeLMod ( I X. I ) )
8 7 frlmdim 
 |-  ( ( R e. DivRing /\ ( I X. I ) e. Fin ) -> ( dim ` ( R freeLMod ( I X. I ) ) ) = ( # ` ( I X. I ) ) )
9 3 6 8 syl2anc 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( dim ` ( R freeLMod ( I X. I ) ) ) = ( # ` ( I X. I ) ) )
10 1 7 matbas 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( Base ` ( R freeLMod ( I X. I ) ) ) = ( Base ` A ) )
11 10 eqcomd 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( Base ` A ) = ( Base ` ( R freeLMod ( I X. I ) ) ) )
12 eqidd 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( Base ` A ) = ( Base ` A ) )
13 ssidd 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( Base ` A ) C_ ( Base ` A ) )
14 1 7 matplusg 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( +g ` ( R freeLMod ( I X. I ) ) ) = ( +g ` A ) )
15 14 oveqdr 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( x ( +g ` ( R freeLMod ( I X. I ) ) ) y ) = ( x ( +g ` A ) y ) )
16 7 frlmlvec 
 |-  ( ( R e. DivRing /\ ( I X. I ) e. Fin ) -> ( R freeLMod ( I X. I ) ) e. LVec )
17 3 6 16 syl2anc 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( R freeLMod ( I X. I ) ) e. LVec )
18 lveclmod 
 |-  ( ( R freeLMod ( I X. I ) ) e. LVec -> ( R freeLMod ( I X. I ) ) e. LMod )
19 17 18 syl 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( R freeLMod ( I X. I ) ) e. LMod )
20 19 adantr 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( R freeLMod ( I X. I ) ) e. LMod )
21 simprl 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> x e. ( Base ` ( Scalar ` A ) ) )
22 1 7 matsca 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( Scalar ` ( R freeLMod ( I X. I ) ) ) = ( Scalar ` A ) )
23 22 fveq2d 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( Base ` ( Scalar ` ( R freeLMod ( I X. I ) ) ) ) = ( Base ` ( Scalar ` A ) ) )
24 23 eqcomd 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` ( R freeLMod ( I X. I ) ) ) ) )
25 24 adantr 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` ( R freeLMod ( I X. I ) ) ) ) )
26 21 25 eleqtrd 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> x e. ( Base ` ( Scalar ` ( R freeLMod ( I X. I ) ) ) ) )
27 simprr 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> y e. ( Base ` A ) )
28 11 adantr 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( Base ` A ) = ( Base ` ( R freeLMod ( I X. I ) ) ) )
29 27 28 eleqtrd 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> y e. ( Base ` ( R freeLMod ( I X. I ) ) ) )
30 eqid 
 |-  ( Base ` ( R freeLMod ( I X. I ) ) ) = ( Base ` ( R freeLMod ( I X. I ) ) )
31 eqid 
 |-  ( Scalar ` ( R freeLMod ( I X. I ) ) ) = ( Scalar ` ( R freeLMod ( I X. I ) ) )
32 eqid 
 |-  ( .s ` ( R freeLMod ( I X. I ) ) ) = ( .s ` ( R freeLMod ( I X. I ) ) )
33 eqid 
 |-  ( Base ` ( Scalar ` ( R freeLMod ( I X. I ) ) ) ) = ( Base ` ( Scalar ` ( R freeLMod ( I X. I ) ) ) )
34 30 31 32 33 lmodvscl 
 |-  ( ( ( R freeLMod ( I X. I ) ) e. LMod /\ x e. ( Base ` ( Scalar ` ( R freeLMod ( I X. I ) ) ) ) /\ y e. ( Base ` ( R freeLMod ( I X. I ) ) ) ) -> ( x ( .s ` ( R freeLMod ( I X. I ) ) ) y ) e. ( Base ` ( R freeLMod ( I X. I ) ) ) )
35 20 26 29 34 syl3anc 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( x ( .s ` ( R freeLMod ( I X. I ) ) ) y ) e. ( Base ` ( R freeLMod ( I X. I ) ) ) )
36 35 28 eleqtrrd 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( x ( .s ` ( R freeLMod ( I X. I ) ) ) y ) e. ( Base ` A ) )
37 1 7 matvsca 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( .s ` ( R freeLMod ( I X. I ) ) ) = ( .s ` A ) )
38 37 oveqdr 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` A ) ) ) -> ( x ( .s ` ( R freeLMod ( I X. I ) ) ) y ) = ( x ( .s ` A ) y ) )
39 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
40 eqidd 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) ) )
41 22 fveq2d 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( +g ` ( Scalar ` ( R freeLMod ( I X. I ) ) ) ) = ( +g ` ( Scalar ` A ) ) )
42 41 oveqdr 
 |-  ( ( ( I e. Fin /\ R e. DivRing ) /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. ( Base ` ( Scalar ` A ) ) ) ) -> ( x ( +g ` ( Scalar ` ( R freeLMod ( I X. I ) ) ) ) y ) = ( x ( +g ` ( Scalar ` A ) ) y ) )
43 drngring 
 |-  ( R e. DivRing -> R e. Ring )
44 1 matlmod 
 |-  ( ( I e. Fin /\ R e. Ring ) -> A e. LMod )
45 43 44 sylan2 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> A e. LMod )
46 1 matsca2 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> R = ( Scalar ` A ) )
47 46 3 eqeltrrd 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( Scalar ` A ) e. DivRing )
48 39 islvec 
 |-  ( A e. LVec <-> ( A e. LMod /\ ( Scalar ` A ) e. DivRing ) )
49 45 47 48 sylanbrc 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> A e. LVec )
50 11 12 13 15 36 38 31 39 24 40 42 17 49 dimpropd 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( dim ` ( R freeLMod ( I X. I ) ) ) = ( dim ` A ) )
51 hashxp 
 |-  ( ( I e. Fin /\ I e. Fin ) -> ( # ` ( I X. I ) ) = ( ( # ` I ) x. ( # ` I ) ) )
52 4 4 51 syl2anc 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( # ` ( I X. I ) ) = ( ( # ` I ) x. ( # ` I ) ) )
53 9 50 52 3eqtr3d 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( dim ` A ) = ( ( # ` I ) x. ( # ` I ) ) )
54 2 2 oveq12i 
 |-  ( N x. N ) = ( ( # ` I ) x. ( # ` I ) )
55 53 54 eqtr4di 
 |-  ( ( I e. Fin /\ R e. DivRing ) -> ( dim ` A ) = ( N x. N ) )