| 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 ‘ 𝐴 ) = ( 𝑁 · 𝑁 ) ) |