Step | Hyp | Ref
| Expression |
1 | | scmatscm.k |
. . . 4
⊢ 𝐾 = (Base‘𝑅) |
2 | | scmatscm.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | | scmatscm.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
4 | | eqid 2610 |
. . . 4
⊢
(1r‘𝐴) = (1r‘𝐴) |
5 | | scmatscm.t |
. . . 4
⊢ ∗ = (
·𝑠 ‘𝐴) |
6 | | scmatscm.c |
. . . 4
⊢ 𝑆 = (𝑁 ScMat 𝑅) |
7 | 1, 2, 3, 4, 5, 6 | scmatscmid 20131 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝑆) → ∃𝑐 ∈ 𝐾 𝐶 = (𝑐 ∗
(1r‘𝐴))) |
8 | 7 | 3expa 1257 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → ∃𝑐 ∈ 𝐾 𝐶 = (𝑐 ∗
(1r‘𝐴))) |
9 | | oveq1 6556 |
. . . . . 6
⊢ (𝐶 = (𝑐 ∗
(1r‘𝐴))
→ (𝐶 × 𝑚) = ((𝑐 ∗
(1r‘𝐴))
×
𝑚)) |
10 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) |
11 | 10 | ad4antr 764 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 ∈ Ring) |
12 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
13 | 12 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
14 | 2 | matring 20068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
15 | 3, 4 | ringidcl 18391 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ Ring →
(1r‘𝐴)
∈ 𝐵) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴)
∈ 𝐵) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → (1r‘𝐴) ∈ 𝐵) |
18 | 17 | anim1i 590 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → ((1r‘𝐴) ∈ 𝐵 ∧ 𝑐 ∈ 𝐾)) |
19 | 18 | ancomd 466 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝑐 ∈ 𝐾 ∧ (1r‘𝐴) ∈ 𝐵)) |
20 | 1, 2, 3, 5 | matvscl 20056 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑐 ∈ 𝐾 ∧ (1r‘𝐴) ∈ 𝐵)) → (𝑐 ∗
(1r‘𝐴))
∈ 𝐵) |
21 | 13, 19, 20 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝑐 ∗
(1r‘𝐴))
∈ 𝐵) |
22 | 21 | anim1i 590 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → ((𝑐 ∗
(1r‘𝐴))
∈ 𝐵 ∧ 𝑚 ∈ 𝐵)) |
23 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑐 ∗
(1r‘𝐴))
∈ 𝐵 ∧ 𝑚 ∈ 𝐵)) |
24 | | simpr 476 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) |
25 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) |
26 | | scmatscm.m |
. . . . . . . . . . . 12
⊢ × =
(.r‘𝐴) |
27 | 2, 3, 25, 26 | matmulcell 20070 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ ((𝑐 ∗
(1r‘𝐴))
∈ 𝐵 ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗))))) |
28 | 11, 23, 24, 27 | syl3anc 1318 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗))))) |
29 | 12 | anim1i 590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑐 ∈ 𝐾)) |
30 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑐 ∈ 𝐾)) |
31 | 29, 30 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾)) |
32 | 31 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾)) |
33 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑅) = (0g‘𝑅) |
34 | 2, 1, 5, 33 | matsc 20075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾) → (𝑐 ∗
(1r‘𝐴)) =
(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, 𝑐, (0g‘𝑅)))) |
35 | 32, 34 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑐 ∗
(1r‘𝐴)) =
(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, 𝑐, (0g‘𝑅)))) |
36 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑘) → (𝑥 = 𝑦 ↔ 𝑖 = 𝑘)) |
37 | 36 | ifbid 4058 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑘) → if(𝑥 = 𝑦, 𝑐, (0g‘𝑅)) = if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) ∧ (𝑥 = 𝑖 ∧ 𝑦 = 𝑘)) → if(𝑥 = 𝑦, 𝑐, (0g‘𝑅)) = if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))) |
39 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
42 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
43 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑐 ∈ V |
44 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑅) ∈ V |
45 | 43, 44 | ifex 4106 |
. . . . . . . . . . . . . . . 16
⊢ if(𝑖 = 𝑘, 𝑐, (0g‘𝑅)) ∈ V |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → if(𝑖 = 𝑘, 𝑐, (0g‘𝑅)) ∈ V) |
47 | 35, 38, 41, 42, 46 | ovmpt2d 6686 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑖(𝑐 ∗
(1r‘𝐴))𝑘) = if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))) |
48 | 47 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗)) = (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗))) |
49 | 48 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗))) = (𝑘 ∈ 𝑁 ↦ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗)))) |
50 | 49 | oveq2d 6565 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗))))) |
51 | | ovif 6635 |
. . . . . . . . . . . . . 14
⊢ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗)) = if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), ((0g‘𝑅)(.r‘𝑅)(𝑘𝑚𝑗))) |
52 | | simp-6r 807 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑅 ∈ Ring) |
53 | | simplrr 797 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
54 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → 𝑚 ∈ 𝐵) |
55 | 54 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑚 ∈ 𝐵) |
56 | 2, 1, 3, 42, 53, 55 | matecld 20051 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑘𝑚𝑗) ∈ 𝐾) |
57 | 1, 25, 33 | ringlz 18410 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ (𝑘𝑚𝑗) ∈ 𝐾) → ((0g‘𝑅)(.r‘𝑅)(𝑘𝑚𝑗)) = (0g‘𝑅)) |
58 | 52, 56, 57 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → ((0g‘𝑅)(.r‘𝑅)(𝑘𝑚𝑗)) = (0g‘𝑅)) |
59 | 58 | ifeq2d 4055 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), ((0g‘𝑅)(.r‘𝑅)(𝑘𝑚𝑗))) = if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) |
60 | 51, 59 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗)) = if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) |
61 | 60 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑘 ∈ 𝑁 ↦ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗))) = (𝑘 ∈ 𝑁 ↦ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)))) |
62 | 61 | oveq2d 6565 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))))) |
63 | | ringmnd 18379 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Mnd) |
65 | 64 | ad4antr 764 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 ∈ Mnd) |
66 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑁 ∈ Fin) |
67 | 66 | ad4antr 764 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑁 ∈ Fin) |
68 | | equcom 1932 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 ↔ 𝑘 = 𝑖) |
69 | | ifbi 4057 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = 𝑘 ↔ 𝑘 = 𝑖) → if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)) = if(𝑘 = 𝑖, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)) = if(𝑘 = 𝑖, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)) |
71 | 70 | mpteq2i 4669 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑁 ↦ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) = (𝑘 ∈ 𝑁 ↦ if(𝑘 = 𝑖, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) |
72 | 1 | eleq2i 2680 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ 𝐾 ↔ 𝑐 ∈ (Base‘𝑅)) |
73 | 72 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ 𝐾 → 𝑐 ∈ (Base‘𝑅)) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → 𝑐 ∈ (Base‘𝑅)) |
75 | 74 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑐 ∈ (Base‘𝑅)) |
76 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅) =
(Base‘𝑅) |
77 | 2, 76, 3, 42, 53, 55 | matecld 20051 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑘𝑚𝑗) ∈ (Base‘𝑅)) |
78 | 76, 25 | ringcl 18384 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅) ∧ (𝑘𝑚𝑗) ∈ (Base‘𝑅)) → (𝑐(.r‘𝑅)(𝑘𝑚𝑗)) ∈ (Base‘𝑅)) |
79 | 52, 75, 77, 78 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑐(.r‘𝑅)(𝑘𝑚𝑗)) ∈ (Base‘𝑅)) |
80 | 79 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ∀𝑘 ∈ 𝑁 (𝑐(.r‘𝑅)(𝑘𝑚𝑗)) ∈ (Base‘𝑅)) |
81 | 33, 65, 67, 40, 71, 80 | gsummpt1n0 18187 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)))) = ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗))) |
82 | 50, 62, 81 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗)))) = ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗))) |
83 | | csbov2g 6589 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)⦋𝑖 / 𝑘⦌(𝑘𝑚𝑗))) |
84 | | csbov1g 6588 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌(𝑘𝑚𝑗) = (⦋𝑖 / 𝑘⦌𝑘𝑚𝑗)) |
85 | | csbvarg 3955 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌𝑘 = 𝑖) |
86 | 85 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ 𝑁 → (⦋𝑖 / 𝑘⦌𝑘𝑚𝑗) = (𝑖𝑚𝑗)) |
87 | 84, 86 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌(𝑘𝑚𝑗) = (𝑖𝑚𝑗)) |
88 | 87 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝑁 → (𝑐(.r‘𝑅)⦋𝑖 / 𝑘⦌(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) |
89 | 83, 88 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) |
90 | 89 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) |
91 | 90 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) |
92 | 28, 82, 91 | 3eqtrd 2648 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) |
93 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → 𝑐 ∈ 𝐾) |
94 | 93 | anim1i 590 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝑐 ∈ 𝐾 ∧ 𝑚 ∈ 𝐵)) |
95 | 94 | adantr 480 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑐 ∈ 𝐾 ∧ 𝑚 ∈ 𝐵)) |
96 | 2, 3, 1, 5, 25 | matvscacell 20061 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑐 ∈ 𝐾 ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑐 ∗ 𝑚)𝑗) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) |
97 | 11, 95, 24, 96 | syl3anc 1318 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑐 ∗ 𝑚)𝑗) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) |
98 | 92, 97 | eqtr4d 2647 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑖(𝑐 ∗ 𝑚)𝑗)) |
99 | 98 | ralrimivva 2954 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑖(𝑐 ∗ 𝑚)𝑗)) |
100 | 14 | ad3antrrr 762 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → 𝐴 ∈ Ring) |
101 | 21 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝑐 ∗
(1r‘𝐴))
∈ 𝐵) |
102 | 3, 26 | ringcl 18384 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Ring ∧ (𝑐 ∗
(1r‘𝐴))
∈ 𝐵 ∧ 𝑚 ∈ 𝐵) → ((𝑐 ∗
(1r‘𝐴))
×
𝑚) ∈ 𝐵) |
103 | 100, 101,
54, 102 | syl3anc 1318 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → ((𝑐 ∗
(1r‘𝐴))
×
𝑚) ∈ 𝐵) |
104 | 12 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
105 | 1, 2, 3, 5 | matvscl 20056 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑐 ∈ 𝐾 ∧ 𝑚 ∈ 𝐵)) → (𝑐 ∗ 𝑚) ∈ 𝐵) |
106 | 104, 94, 105 | syl2anc 691 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝑐 ∗ 𝑚) ∈ 𝐵) |
107 | 2, 3 | eqmat 20049 |
. . . . . . . 8
⊢ ((((𝑐 ∗
(1r‘𝐴))
×
𝑚) ∈ 𝐵 ∧ (𝑐 ∗ 𝑚) ∈ 𝐵) → (((𝑐 ∗
(1r‘𝐴))
×
𝑚) = (𝑐 ∗ 𝑚) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑖(𝑐 ∗ 𝑚)𝑗))) |
108 | 103, 106,
107 | syl2anc 691 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (((𝑐 ∗
(1r‘𝐴))
×
𝑚) = (𝑐 ∗ 𝑚) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑖(𝑐 ∗ 𝑚)𝑗))) |
109 | 99, 108 | mpbird 246 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → ((𝑐 ∗
(1r‘𝐴))
×
𝑚) = (𝑐 ∗ 𝑚)) |
110 | 9, 109 | sylan9eqr 2666 |
. . . . 5
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ 𝐶 = (𝑐 ∗
(1r‘𝐴)))
→ (𝐶 × 𝑚) = (𝑐 ∗ 𝑚)) |
111 | 110 | ex 449 |
. . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝐶 = (𝑐 ∗
(1r‘𝐴))
→ (𝐶 × 𝑚) = (𝑐 ∗ 𝑚))) |
112 | 111 | ralrimdva 2952 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝐶 = (𝑐 ∗
(1r‘𝐴))
→ ∀𝑚 ∈
𝐵 (𝐶 × 𝑚) = (𝑐 ∗ 𝑚))) |
113 | 112 | reximdva 3000 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → (∃𝑐 ∈ 𝐾 𝐶 = (𝑐 ∗
(1r‘𝐴))
→ ∃𝑐 ∈
𝐾 ∀𝑚 ∈ 𝐵 (𝐶 × 𝑚) = (𝑐 ∗ 𝑚))) |
114 | 8, 113 | mpd 15 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → ∃𝑐 ∈ 𝐾 ∀𝑚 ∈ 𝐵 (𝐶 × 𝑚) = (𝑐 ∗ 𝑚)) |