| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → 𝑅 ∈
DivRing) |
| 2 | | simpl 482 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → 𝐼 ∈ Fin) |
| 3 | | xpfi 9358 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) → (𝐼 × 𝐼) ∈ Fin) |
| 4 | 2, 2, 3 | syl2anc 584 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (𝐼 × 𝐼) ∈ Fin) |
| 5 | | eqid 2737 |
. . . . 5
⊢ (𝑅 freeLMod (𝐼 × 𝐼)) = (𝑅 freeLMod (𝐼 × 𝐼)) |
| 6 | 5 | frlmdim 33662 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ (𝐼 × 𝐼) ∈ Fin) → (dim‘(𝑅 freeLMod (𝐼 × 𝐼))) = (♯‘(𝐼 × 𝐼))) |
| 7 | 1, 4, 6 | syl2anc 584 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(dim‘(𝑅 freeLMod
(𝐼 × 𝐼))) = (♯‘(𝐼 × 𝐼))) |
| 8 | | matdim.a |
. . . . . 6
⊢ 𝐴 = (𝐼 Mat 𝑅) |
| 9 | 8, 5 | matbas 22417 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(Base‘(𝑅 freeLMod
(𝐼 × 𝐼))) = (Base‘𝐴)) |
| 10 | 9 | eqcomd 2743 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(Base‘𝐴) =
(Base‘(𝑅 freeLMod
(𝐼 × 𝐼)))) |
| 11 | | eqidd 2738 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(Base‘𝐴) =
(Base‘𝐴)) |
| 12 | | ssidd 4007 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(Base‘𝐴) ⊆
(Base‘𝐴)) |
| 13 | 8, 5 | matplusg 22418 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(+g‘(𝑅
freeLMod (𝐼 × 𝐼))) = (+g‘𝐴)) |
| 14 | 13 | oveqdr 7459 |
. . . 4
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑥(+g‘(𝑅 freeLMod (𝐼 × 𝐼)))𝑦) = (𝑥(+g‘𝐴)𝑦)) |
| 15 | 5 | frlmlvec 21781 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ (𝐼 × 𝐼) ∈ Fin) → (𝑅 freeLMod (𝐼 × 𝐼)) ∈ LVec) |
| 16 | 1, 4, 15 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (𝑅 freeLMod (𝐼 × 𝐼)) ∈ LVec) |
| 17 | | lveclmod 21105 |
. . . . . . . 8
⊢ ((𝑅 freeLMod (𝐼 × 𝐼)) ∈ LVec → (𝑅 freeLMod (𝐼 × 𝐼)) ∈ LMod) |
| 18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (𝑅 freeLMod (𝐼 × 𝐼)) ∈ LMod) |
| 19 | 18 | adantr 480 |
. . . . . 6
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑅 freeLMod (𝐼 × 𝐼)) ∈ LMod) |
| 20 | | simprl 771 |
. . . . . . 7
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑥 ∈ (Base‘(Scalar‘𝐴))) |
| 21 | 8, 5 | matsca 22419 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(Scalar‘(𝑅 freeLMod
(𝐼 × 𝐼))) = (Scalar‘𝐴)) |
| 22 | 21 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(Base‘(Scalar‘(𝑅 freeLMod (𝐼 × 𝐼)))) = (Base‘(Scalar‘𝐴))) |
| 23 | 22 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘(𝑅 freeLMod (𝐼 × 𝐼))))) |
| 24 | 23 | adantr 480 |
. . . . . . 7
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (Base‘(Scalar‘𝐴)) =
(Base‘(Scalar‘(𝑅 freeLMod (𝐼 × 𝐼))))) |
| 25 | 20, 24 | eleqtrd 2843 |
. . . . . 6
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑥 ∈ (Base‘(Scalar‘(𝑅 freeLMod (𝐼 × 𝐼))))) |
| 26 | | simprr 773 |
. . . . . . 7
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑦 ∈ (Base‘𝐴)) |
| 27 | 10 | adantr 480 |
. . . . . . 7
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (Base‘𝐴) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼)))) |
| 28 | 26, 27 | eleqtrd 2843 |
. . . . . 6
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → 𝑦 ∈ (Base‘(𝑅 freeLMod (𝐼 × 𝐼)))) |
| 29 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝑅
freeLMod (𝐼 × 𝐼))) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) |
| 30 | | eqid 2737 |
. . . . . . 7
⊢
(Scalar‘(𝑅
freeLMod (𝐼 × 𝐼))) = (Scalar‘(𝑅 freeLMod (𝐼 × 𝐼))) |
| 31 | | eqid 2737 |
. . . . . . 7
⊢ (
·𝑠 ‘(𝑅 freeLMod (𝐼 × 𝐼))) = ( ·𝑠
‘(𝑅 freeLMod (𝐼 × 𝐼))) |
| 32 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(Scalar‘(𝑅 freeLMod (𝐼 × 𝐼)))) = (Base‘(Scalar‘(𝑅 freeLMod (𝐼 × 𝐼)))) |
| 33 | 29, 30, 31, 32 | lmodvscl 20876 |
. . . . . 6
⊢ (((𝑅 freeLMod (𝐼 × 𝐼)) ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘(𝑅 freeLMod (𝐼 × 𝐼)))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod (𝐼 × 𝐼)))) → (𝑥( ·𝑠
‘(𝑅 freeLMod (𝐼 × 𝐼)))𝑦) ∈ (Base‘(𝑅 freeLMod (𝐼 × 𝐼)))) |
| 34 | 19, 25, 28, 33 | syl3anc 1373 |
. . . . 5
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑥( ·𝑠
‘(𝑅 freeLMod (𝐼 × 𝐼)))𝑦) ∈ (Base‘(𝑅 freeLMod (𝐼 × 𝐼)))) |
| 35 | 34, 27 | eleqtrrd 2844 |
. . . 4
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑥( ·𝑠
‘(𝑅 freeLMod (𝐼 × 𝐼)))𝑦) ∈ (Base‘𝐴)) |
| 36 | 8, 5 | matvsca 22421 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (
·𝑠 ‘(𝑅 freeLMod (𝐼 × 𝐼))) = ( ·𝑠
‘𝐴)) |
| 37 | 36 | oveqdr 7459 |
. . . 4
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴))) → (𝑥( ·𝑠
‘(𝑅 freeLMod (𝐼 × 𝐼)))𝑦) = (𝑥( ·𝑠
‘𝐴)𝑦)) |
| 38 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
| 39 | | eqidd 2738 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴))) |
| 40 | 21 | fveq2d 6910 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(+g‘(Scalar‘(𝑅 freeLMod (𝐼 × 𝐼)))) =
(+g‘(Scalar‘𝐴))) |
| 41 | 40 | oveqdr 7459 |
. . . 4
⊢ (((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) ∧ (𝑥 ∈
(Base‘(Scalar‘𝐴)) ∧ 𝑦 ∈ (Base‘(Scalar‘𝐴)))) → (𝑥(+g‘(Scalar‘(𝑅 freeLMod (𝐼 × 𝐼))))𝑦) = (𝑥(+g‘(Scalar‘𝐴))𝑦)) |
| 42 | | drngring 20736 |
. . . . . 6
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
| 43 | 8 | matlmod 22435 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
| 44 | 42, 43 | sylan2 593 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → 𝐴 ∈ LMod) |
| 45 | 8 | matsca2 22426 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → 𝑅 = (Scalar‘𝐴)) |
| 46 | 45, 1 | eqeltrrd 2842 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(Scalar‘𝐴) ∈
DivRing) |
| 47 | 38 | islvec 21103 |
. . . . 5
⊢ (𝐴 ∈ LVec ↔ (𝐴 ∈ LMod ∧
(Scalar‘𝐴) ∈
DivRing)) |
| 48 | 44, 46, 47 | sylanbrc 583 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → 𝐴 ∈ LVec) |
| 49 | 10, 11, 12, 14, 35, 37, 30, 38, 23, 39, 41, 16, 48 | dimpropd 33659 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(dim‘(𝑅 freeLMod
(𝐼 × 𝐼))) = (dim‘𝐴)) |
| 50 | | hashxp 14473 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) →
(♯‘(𝐼 ×
𝐼)) = ((♯‘𝐼) · (♯‘𝐼))) |
| 51 | 2, 2, 50 | syl2anc 584 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(♯‘(𝐼 ×
𝐼)) = ((♯‘𝐼) · (♯‘𝐼))) |
| 52 | 7, 49, 51 | 3eqtr3d 2785 |
. 2
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(dim‘𝐴) =
((♯‘𝐼) ·
(♯‘𝐼))) |
| 53 | | matdim.n |
. . 3
⊢ 𝑁 = (♯‘𝐼) |
| 54 | 53, 53 | oveq12i 7443 |
. 2
⊢ (𝑁 · 𝑁) = ((♯‘𝐼) · (♯‘𝐼)) |
| 55 | 52, 54 | eqtr4di 2795 |
1
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) →
(dim‘𝐴) = (𝑁 · 𝑁)) |