Step | Hyp | Ref
| Expression |
1 | | matassa.a |
. . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | eqid 2738 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | 1, 2 | matbas2 21570 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
((Base‘𝑅)
↑m (𝑁
× 𝑁)) =
(Base‘𝐴)) |
4 | 1 | matsca2 21569 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝐴)) |
5 | | eqidd 2739 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(Base‘𝑅) =
(Base‘𝑅)) |
6 | | eqidd 2739 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴)) |
7 | | eqid 2738 |
. . 3
⊢ (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) |
8 | 1, 7 | matmulr 21587 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
9 | | crngring 19795 |
. . 3
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
10 | 1 | matlmod 21578 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
11 | 9, 10 | sylan2 593 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ LMod) |
12 | 1 | matring 21592 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
13 | 9, 12 | sylan2 593 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
14 | | simpr 485 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ CRing) |
15 | 9 | ad2antlr 724 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → 𝑅 ∈ Ring) |
16 | | simpll 764 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → 𝑁 ∈ Fin) |
17 | | eqid 2738 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
18 | | simpr1 1193 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → 𝑥 ∈ (Base‘𝑅)) |
19 | | simpr2 1194 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
20 | | simpr3 1195 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
21 | 2, 15, 7, 16, 16, 16, 17, 18, 19, 20 | mamuvs1 21552 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → ((((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)𝑦)(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧) = (((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)(𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧))) |
22 | 3 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = (Base‘𝐴)) |
23 | 19, 22 | eleqtrd 2841 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → 𝑦 ∈ (Base‘𝐴)) |
24 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝐴) =
(Base‘𝐴) |
25 | | eqid 2738 |
. . . . . 6
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
26 | | eqid 2738 |
. . . . . 6
⊢ (𝑁 × 𝑁) = (𝑁 × 𝑁) |
27 | 1, 24, 2, 25, 17, 26 | matvsca2 21577 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝐴)) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)𝑦)) |
28 | 18, 23, 27 | syl2anc 584 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)𝑦)) |
29 | 28 | oveq1d 7290 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧) = ((((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)𝑦)(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧)) |
30 | 2, 15, 7, 16, 16, 16, 19, 20 | mamucl 21548 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → (𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧) ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
31 | 30, 22 | eleqtrd 2841 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → (𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧) ∈ (Base‘𝐴)) |
32 | 1, 24, 2, 25, 17, 26 | matvsca2 21577 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑅) ∧ (𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧) ∈ (Base‘𝐴)) → (𝑥( ·𝑠
‘𝐴)(𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧)) = (((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)(𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧))) |
33 | 18, 31, 32 | syl2anc 584 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → (𝑥( ·𝑠
‘𝐴)(𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧)) = (((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)(𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧))) |
34 | 21, 29, 33 | 3eqtr4d 2788 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧) = (𝑥( ·𝑠
‘𝐴)(𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧))) |
35 | | simplr 766 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → 𝑅 ∈ CRing) |
36 | 35, 2, 17, 7, 16, 16, 16, 19, 18, 20 | mamuvs2 21553 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → (𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)𝑧)) = (((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)(𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧))) |
37 | 20, 22 | eleqtrd 2841 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → 𝑧 ∈ (Base‘𝐴)) |
38 | 1, 24, 2, 25, 17, 26 | matvsca2 21577 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)𝑧)) |
39 | 18, 37, 38 | syl2anc 584 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)𝑧)) |
40 | 39 | oveq2d 7291 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → (𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(((𝑁 × 𝑁) × {𝑥}) ∘f
(.r‘𝑅)𝑧))) |
41 | 36, 40, 33 | 3eqtr4d 2788 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ 𝑧 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))) → (𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑥( ·𝑠
‘𝐴)(𝑦(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝑧))) |
42 | 3, 4, 5, 6, 8, 11,
13, 14, 34, 41 | isassad 21071 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ AssAlg) |