Step | Hyp | Ref
| Expression |
1 | | crngring 18381 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
2 | | scmatid.a |
. . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | | scmatid.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐴) |
4 | | scmatid.e |
. . . . 5
⊢ 𝐸 = (Base‘𝑅) |
5 | | scmatid.0 |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
6 | | scmatid.s |
. . . . 5
⊢ 𝑆 = (𝑁 ScMat 𝑅) |
7 | 2, 3, 4, 5, 6 | scmatsrng 20145 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubRing‘𝐴)) |
8 | 1, 7 | sylan2 490 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑆 ∈ (SubRing‘𝐴)) |
9 | | scmatcrng.c |
. . . 4
⊢ 𝐶 = (𝐴 ↾s 𝑆) |
10 | 9 | subrgring 18606 |
. . 3
⊢ (𝑆 ∈ (SubRing‘𝐴) → 𝐶 ∈ Ring) |
11 | 8, 10 | syl 17 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ Ring) |
12 | | simp1lr 1118 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑅 ∈ CRing) |
13 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝐴) =
(Base‘𝐴) |
14 | | simp2 1055 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑎 ∈ 𝑁) |
15 | | simp3 1056 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑏 ∈ 𝑁) |
16 | 2, 13, 6 | scmatmat 20134 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑥 ∈ 𝑆 → 𝑥 ∈ (Base‘𝐴))) |
17 | 16 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐴)) |
18 | 17 | adantrr 749 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ (Base‘𝐴)) |
19 | 18 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑥 ∈ (Base‘𝐴)) |
20 | 2, 4, 13, 14, 15, 19 | matecld 20051 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑥𝑏) ∈ 𝐸) |
21 | 2, 13, 6 | scmatmat 20134 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑦 ∈ 𝑆 → 𝑦 ∈ (Base‘𝐴))) |
22 | 21 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ (Base‘𝐴)) |
23 | 22 | adantrl 748 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (Base‘𝐴)) |
24 | 23 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑦 ∈ (Base‘𝐴)) |
25 | 2, 4, 13, 14, 15, 24 | matecld 20051 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑦𝑏) ∈ 𝐸) |
26 | | eqid 2610 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
27 | 4, 26 | crngcom 18385 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑎𝑥𝑏) ∈ 𝐸 ∧ (𝑎𝑦𝑏) ∈ 𝐸) → ((𝑎𝑥𝑏)(.r‘𝑅)(𝑎𝑦𝑏)) = ((𝑎𝑦𝑏)(.r‘𝑅)(𝑎𝑥𝑏))) |
28 | 12, 20, 25, 27 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ((𝑎𝑥𝑏)(.r‘𝑅)(𝑎𝑦𝑏)) = ((𝑎𝑦𝑏)(.r‘𝑅)(𝑎𝑥𝑏))) |
29 | 28 | ifeq1d 4054 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝑏, ((𝑎𝑥𝑏)(.r‘𝑅)(𝑎𝑦𝑏)), 0 ) = if(𝑎 = 𝑏, ((𝑎𝑦𝑏)(.r‘𝑅)(𝑎𝑥𝑏)), 0 )) |
30 | 29 | mpt2eq3dva 6617 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, ((𝑎𝑥𝑏)(.r‘𝑅)(𝑎𝑦𝑏)), 0 )) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, ((𝑎𝑦𝑏)(.r‘𝑅)(𝑎𝑥𝑏)), 0 ))) |
31 | 1 | anim2i 591 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
32 | 31 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
33 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑁 DMat 𝑅) = (𝑁 DMat 𝑅) |
34 | 2, 3, 4, 5, 6, 33 | scmatdmat 20140 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → 𝑥 ∈ (𝑁 DMat 𝑅))) |
35 | 1, 34 | sylan2 490 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑥 ∈ 𝑆 → 𝑥 ∈ (𝑁 DMat 𝑅))) |
36 | 2, 3, 4, 5, 6, 33 | scmatdmat 20140 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝑆 → 𝑦 ∈ (𝑁 DMat 𝑅))) |
37 | 1, 36 | sylan2 490 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑦 ∈ 𝑆 → 𝑦 ∈ (𝑁 DMat 𝑅))) |
38 | 35, 37 | anim12d 584 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 ∈ (𝑁 DMat 𝑅) ∧ 𝑦 ∈ (𝑁 DMat 𝑅)))) |
39 | 38 | imp 444 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 ∈ (𝑁 DMat 𝑅) ∧ 𝑦 ∈ (𝑁 DMat 𝑅))) |
40 | 2, 3, 5, 33 | dmatmul 20122 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ (𝑁 DMat 𝑅) ∧ 𝑦 ∈ (𝑁 DMat 𝑅))) → (𝑥(.r‘𝐴)𝑦) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, ((𝑎𝑥𝑏)(.r‘𝑅)(𝑎𝑦𝑏)), 0 ))) |
41 | 32, 39, 40 | syl2anc 691 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(.r‘𝐴)𝑦) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, ((𝑎𝑥𝑏)(.r‘𝑅)(𝑎𝑦𝑏)), 0 ))) |
42 | 39 | ancomd 466 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑦 ∈ (𝑁 DMat 𝑅) ∧ 𝑥 ∈ (𝑁 DMat 𝑅))) |
43 | 2, 3, 5, 33 | dmatmul 20122 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (𝑁 DMat 𝑅) ∧ 𝑥 ∈ (𝑁 DMat 𝑅))) → (𝑦(.r‘𝐴)𝑥) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, ((𝑎𝑦𝑏)(.r‘𝑅)(𝑎𝑥𝑏)), 0 ))) |
44 | 32, 42, 43 | syl2anc 691 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑦(.r‘𝐴)𝑥) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, ((𝑎𝑦𝑏)(.r‘𝑅)(𝑎𝑥𝑏)), 0 ))) |
45 | 30, 41, 44 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥)) |
46 | 45 | ralrimivva 2954 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥)) |
47 | 9 | subrgbas 18612 |
. . . . . 6
⊢ (𝑆 ∈ (SubRing‘𝐴) → 𝑆 = (Base‘𝐶)) |
48 | 47 | eqcomd 2616 |
. . . . 5
⊢ (𝑆 ∈ (SubRing‘𝐴) → (Base‘𝐶) = 𝑆) |
49 | | eqid 2610 |
. . . . . . . . . 10
⊢
(.r‘𝐴) = (.r‘𝐴) |
50 | 9, 49 | ressmulr 15829 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubRing‘𝐴) →
(.r‘𝐴) =
(.r‘𝐶)) |
51 | 50 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubRing‘𝐴) →
(.r‘𝐶) =
(.r‘𝐴)) |
52 | 51 | oveqd 6566 |
. . . . . . 7
⊢ (𝑆 ∈ (SubRing‘𝐴) → (𝑥(.r‘𝐶)𝑦) = (𝑥(.r‘𝐴)𝑦)) |
53 | 51 | oveqd 6566 |
. . . . . . 7
⊢ (𝑆 ∈ (SubRing‘𝐴) → (𝑦(.r‘𝐶)𝑥) = (𝑦(.r‘𝐴)𝑥)) |
54 | 52, 53 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑆 ∈ (SubRing‘𝐴) → ((𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥) ↔ (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥))) |
55 | 48, 54 | raleqbidv 3129 |
. . . . 5
⊢ (𝑆 ∈ (SubRing‘𝐴) → (∀𝑦 ∈ (Base‘𝐶)(𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥) ↔ ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥))) |
56 | 48, 55 | raleqbidv 3129 |
. . . 4
⊢ (𝑆 ∈ (SubRing‘𝐴) → (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥))) |
57 | 8, 56 | syl 17 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
(∀𝑥 ∈
(Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝐴)𝑦) = (𝑦(.r‘𝐴)𝑥))) |
58 | 46, 57 | mpbird 246 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
∀𝑥 ∈
(Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥)) |
59 | | eqid 2610 |
. . 3
⊢
(Base‘𝐶) =
(Base‘𝐶) |
60 | | eqid 2610 |
. . 3
⊢
(.r‘𝐶) = (.r‘𝐶) |
61 | 59, 60 | iscrng2 18386 |
. 2
⊢ (𝐶 ∈ CRing ↔ (𝐶 ∈ Ring ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥))) |
62 | 11, 58, 61 | sylanbrc 695 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ CRing) |