| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | scmatscm.k | . . . 4
⊢ 𝐾 = (Base‘𝑅) | 
| 2 |  | scmatscm.a | . . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 3 |  | scmatscm.b | . . . 4
⊢ 𝐵 = (Base‘𝐴) | 
| 4 |  | eqid 2737 | . . . 4
⊢
(1r‘𝐴) = (1r‘𝐴) | 
| 5 |  | scmatscm.t | . . . 4
⊢  ∗ = (
·𝑠 ‘𝐴) | 
| 6 |  | scmatscm.c | . . . 4
⊢ 𝑆 = (𝑁 ScMat 𝑅) | 
| 7 | 1, 2, 3, 4, 5, 6 | scmatscmid 22512 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝑆) → ∃𝑐 ∈ 𝐾 𝐶 = (𝑐 ∗
(1r‘𝐴))) | 
| 8 | 7 | 3expa 1119 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → ∃𝑐 ∈ 𝐾 𝐶 = (𝑐 ∗
(1r‘𝐴))) | 
| 9 |  | oveq1 7438 | . . . . . 6
⊢ (𝐶 = (𝑐 ∗
(1r‘𝐴))
→ (𝐶 × 𝑚) = ((𝑐 ∗
(1r‘𝐴))
×
𝑚)) | 
| 10 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) | 
| 11 | 10 | ad4antr 732 | . . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 ∈ Ring) | 
| 12 |  | simpl 482 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) | 
| 13 | 12 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) | 
| 14 | 2 | matring 22449 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) | 
| 15 | 3, 4 | ringidcl 20262 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Ring →
(1r‘𝐴)
∈ 𝐵) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴)
∈ 𝐵) | 
| 17 | 16 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → (1r‘𝐴) ∈ 𝐵) | 
| 18 | 17 | anim1ci 616 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝑐 ∈ 𝐾 ∧ (1r‘𝐴) ∈ 𝐵)) | 
| 19 | 1, 2, 3, 5 | matvscl 22437 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑐 ∈ 𝐾 ∧ (1r‘𝐴) ∈ 𝐵)) → (𝑐 ∗
(1r‘𝐴))
∈ 𝐵) | 
| 20 | 13, 18, 19 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝑐 ∗
(1r‘𝐴))
∈ 𝐵) | 
| 21 | 20 | anim1i 615 | . . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → ((𝑐 ∗
(1r‘𝐴))
∈ 𝐵 ∧ 𝑚 ∈ 𝐵)) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑐 ∗
(1r‘𝐴))
∈ 𝐵 ∧ 𝑚 ∈ 𝐵)) | 
| 23 |  | simpr 484 | . . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) | 
| 24 |  | scmatscm.m | . . . . . . . . . . . 12
⊢  × =
(.r‘𝐴) | 
| 25 | 2, 3, 24 | matmulcell 22451 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ ((𝑐 ∗
(1r‘𝐴))
∈ 𝐵 ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗))))) | 
| 26 | 11, 22, 23, 25 | syl3anc 1373 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗))))) | 
| 27 | 12 | anim1i 615 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑐 ∈ 𝐾)) | 
| 28 |  | df-3an 1089 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑐 ∈ 𝐾)) | 
| 29 | 27, 28 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾)) | 
| 30 | 29 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾)) | 
| 31 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 32 | 2, 1, 5, 31 | matsc 22456 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾) → (𝑐 ∗
(1r‘𝐴)) =
(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, 𝑐, (0g‘𝑅)))) | 
| 33 | 30, 32 | syl 17 | . . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑐 ∗
(1r‘𝐴)) =
(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, 𝑐, (0g‘𝑅)))) | 
| 34 |  | eqeq12 2754 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑘) → (𝑥 = 𝑦 ↔ 𝑖 = 𝑘)) | 
| 35 | 34 | ifbid 4549 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑘) → if(𝑥 = 𝑦, 𝑐, (0g‘𝑅)) = if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))) | 
| 36 | 35 | adantl 481 | . . . . . . . . . . . . . . 15
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) ∧ (𝑥 = 𝑖 ∧ 𝑦 = 𝑘)) → if(𝑥 = 𝑦, 𝑐, (0g‘𝑅)) = if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))) | 
| 37 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) | 
| 38 | 37 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁) | 
| 39 | 38 | adantr 480 | . . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑖 ∈ 𝑁) | 
| 40 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁) | 
| 41 |  | vex 3484 | . . . . . . . . . . . . . . . . 17
⊢ 𝑐 ∈ V | 
| 42 |  | fvex 6919 | . . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑅) ∈ V | 
| 43 | 41, 42 | ifex 4576 | . . . . . . . . . . . . . . . 16
⊢ if(𝑖 = 𝑘, 𝑐, (0g‘𝑅)) ∈ V | 
| 44 | 43 | a1i 11 | . . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → if(𝑖 = 𝑘, 𝑐, (0g‘𝑅)) ∈ V) | 
| 45 | 33, 36, 39, 40, 44 | ovmpod 7585 | . . . . . . . . . . . . . 14
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑖(𝑐 ∗
(1r‘𝐴))𝑘) = if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))) | 
| 46 | 45 | oveq1d 7446 | . . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗)) = (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗))) | 
| 47 | 46 | mpteq2dva 5242 | . . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗))) = (𝑘 ∈ 𝑁 ↦ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗)))) | 
| 48 | 47 | oveq2d 7447 | . . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗))))) | 
| 49 |  | ovif 7531 | . . . . . . . . . . . . . 14
⊢ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗)) = if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), ((0g‘𝑅)(.r‘𝑅)(𝑘𝑚𝑗))) | 
| 50 |  | simp-6r 788 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑅 ∈ Ring) | 
| 51 |  | simplrr 778 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑗 ∈ 𝑁) | 
| 52 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → 𝑚 ∈ 𝐵) | 
| 53 | 52 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑚 ∈ 𝐵) | 
| 54 | 2, 1, 3, 40, 51, 53 | matecld 22432 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑘𝑚𝑗) ∈ 𝐾) | 
| 55 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 56 | 1, 55, 31 | ringlz 20290 | . . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ (𝑘𝑚𝑗) ∈ 𝐾) → ((0g‘𝑅)(.r‘𝑅)(𝑘𝑚𝑗)) = (0g‘𝑅)) | 
| 57 | 50, 54, 56 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → ((0g‘𝑅)(.r‘𝑅)(𝑘𝑚𝑗)) = (0g‘𝑅)) | 
| 58 | 57 | ifeq2d 4546 | . . . . . . . . . . . . . 14
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), ((0g‘𝑅)(.r‘𝑅)(𝑘𝑚𝑗))) = if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) | 
| 59 | 49, 58 | eqtrid 2789 | . . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗)) = if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) | 
| 60 | 59 | mpteq2dva 5242 | . . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑘 ∈ 𝑁 ↦ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗))) = (𝑘 ∈ 𝑁 ↦ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)))) | 
| 61 | 60 | oveq2d 7447 | . . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ (if(𝑖 = 𝑘, 𝑐, (0g‘𝑅))(.r‘𝑅)(𝑘𝑚𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))))) | 
| 62 |  | ringmnd 20240 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | 
| 63 | 62 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Mnd) | 
| 64 | 63 | ad4antr 732 | . . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 ∈ Mnd) | 
| 65 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑁 ∈ Fin) | 
| 66 | 65 | ad4antr 732 | . . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑁 ∈ Fin) | 
| 67 |  | equcom 2017 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 ↔ 𝑘 = 𝑖) | 
| 68 |  | ifbi 4548 | . . . . . . . . . . . . . 14
⊢ ((𝑖 = 𝑘 ↔ 𝑘 = 𝑖) → if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)) = if(𝑘 = 𝑖, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) | 
| 69 | 67, 68 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)) = if(𝑘 = 𝑖, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)) | 
| 70 | 69 | mpteq2i 5247 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑁 ↦ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) = (𝑘 ∈ 𝑁 ↦ if(𝑘 = 𝑖, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅))) | 
| 71 | 1 | eleq2i 2833 | . . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ 𝐾 ↔ 𝑐 ∈ (Base‘𝑅)) | 
| 72 | 71 | biimpi 216 | . . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ 𝐾 → 𝑐 ∈ (Base‘𝑅)) | 
| 73 | 72 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → 𝑐 ∈ (Base‘𝑅)) | 
| 74 | 73 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → 𝑐 ∈ (Base‘𝑅)) | 
| 75 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 76 | 2, 75, 3, 40, 51, 53 | matecld 22432 | . . . . . . . . . . . . . 14
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑘𝑚𝑗) ∈ (Base‘𝑅)) | 
| 77 | 75, 55 | ringcl 20247 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑐 ∈ (Base‘𝑅) ∧ (𝑘𝑚𝑗) ∈ (Base‘𝑅)) → (𝑐(.r‘𝑅)(𝑘𝑚𝑗)) ∈ (Base‘𝑅)) | 
| 78 | 50, 74, 76, 77 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑘 ∈ 𝑁) → (𝑐(.r‘𝑅)(𝑘𝑚𝑗)) ∈ (Base‘𝑅)) | 
| 79 | 78 | ralrimiva 3146 | . . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ∀𝑘 ∈ 𝑁 (𝑐(.r‘𝑅)(𝑘𝑚𝑗)) ∈ (Base‘𝑅)) | 
| 80 | 31, 64, 66, 38, 70, 79 | gsummpt1n0 19983 | . . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ if(𝑖 = 𝑘, (𝑐(.r‘𝑅)(𝑘𝑚𝑗)), (0g‘𝑅)))) = ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗))) | 
| 81 | 48, 61, 80 | 3eqtrd 2781 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖(𝑐 ∗
(1r‘𝐴))𝑘)(.r‘𝑅)(𝑘𝑚𝑗)))) = ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗))) | 
| 82 |  | csbov2g 7479 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)⦋𝑖 / 𝑘⦌(𝑘𝑚𝑗))) | 
| 83 |  | csbov1g 7478 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌(𝑘𝑚𝑗) = (⦋𝑖 / 𝑘⦌𝑘𝑚𝑗)) | 
| 84 |  | csbvarg 4434 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌𝑘 = 𝑖) | 
| 85 | 84 | oveq1d 7446 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ 𝑁 → (⦋𝑖 / 𝑘⦌𝑘𝑚𝑗) = (𝑖𝑚𝑗)) | 
| 86 | 83, 85 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌(𝑘𝑚𝑗) = (𝑖𝑚𝑗)) | 
| 87 | 86 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝑁 → (𝑐(.r‘𝑅)⦋𝑖 / 𝑘⦌(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) | 
| 88 | 82, 87 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ 𝑁 → ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) | 
| 89 | 88 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) | 
| 90 | 89 | adantl 481 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ⦋𝑖 / 𝑘⦌(𝑐(.r‘𝑅)(𝑘𝑚𝑗)) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) | 
| 91 | 26, 81, 90 | 3eqtrd 2781 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) | 
| 92 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → 𝑐 ∈ 𝐾) | 
| 93 | 92 | anim1i 615 | . . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝑐 ∈ 𝐾 ∧ 𝑚 ∈ 𝐵)) | 
| 94 | 93 | adantr 480 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑐 ∈ 𝐾 ∧ 𝑚 ∈ 𝐵)) | 
| 95 | 2, 3, 1, 5, 55 | matvscacell 22442 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑐 ∈ 𝐾 ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑐 ∗ 𝑚)𝑗) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) | 
| 96 | 11, 94, 23, 95 | syl3anc 1373 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑐 ∗ 𝑚)𝑗) = (𝑐(.r‘𝑅)(𝑖𝑚𝑗))) | 
| 97 | 91, 96 | eqtr4d 2780 | . . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑖(𝑐 ∗ 𝑚)𝑗)) | 
| 98 | 97 | ralrimivva 3202 | . . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑖(𝑐 ∗ 𝑚)𝑗)) | 
| 99 | 14 | ad3antrrr 730 | . . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → 𝐴 ∈ Ring) | 
| 100 | 20 | adantr 480 | . . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝑐 ∗
(1r‘𝐴))
∈ 𝐵) | 
| 101 | 3, 24 | ringcl 20247 | . . . . . . . . 9
⊢ ((𝐴 ∈ Ring ∧ (𝑐 ∗
(1r‘𝐴))
∈ 𝐵 ∧ 𝑚 ∈ 𝐵) → ((𝑐 ∗
(1r‘𝐴))
×
𝑚) ∈ 𝐵) | 
| 102 | 99, 100, 52, 101 | syl3anc 1373 | . . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → ((𝑐 ∗
(1r‘𝐴))
×
𝑚) ∈ 𝐵) | 
| 103 | 12 | ad2antrr 726 | . . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) | 
| 104 | 1, 2, 3, 5 | matvscl 22437 | . . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑐 ∈ 𝐾 ∧ 𝑚 ∈ 𝐵)) → (𝑐 ∗ 𝑚) ∈ 𝐵) | 
| 105 | 103, 93, 104 | syl2anc 584 | . . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝑐 ∗ 𝑚) ∈ 𝐵) | 
| 106 | 2, 3 | eqmat 22430 | . . . . . . . 8
⊢ ((((𝑐 ∗
(1r‘𝐴))
×
𝑚) ∈ 𝐵 ∧ (𝑐 ∗ 𝑚) ∈ 𝐵) → (((𝑐 ∗
(1r‘𝐴))
×
𝑚) = (𝑐 ∗ 𝑚) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑖(𝑐 ∗ 𝑚)𝑗))) | 
| 107 | 102, 105,
106 | syl2anc 584 | . . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (((𝑐 ∗
(1r‘𝐴))
×
𝑚) = (𝑐 ∗ 𝑚) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖((𝑐 ∗
(1r‘𝐴))
×
𝑚)𝑗) = (𝑖(𝑐 ∗ 𝑚)𝑗))) | 
| 108 | 98, 107 | mpbird 257 | . . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → ((𝑐 ∗
(1r‘𝐴))
×
𝑚) = (𝑐 ∗ 𝑚)) | 
| 109 | 9, 108 | sylan9eqr 2799 | . . . . 5
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) ∧ 𝐶 = (𝑐 ∗
(1r‘𝐴)))
→ (𝐶 × 𝑚) = (𝑐 ∗ 𝑚)) | 
| 110 | 109 | ex 412 | . . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) ∧ 𝑚 ∈ 𝐵) → (𝐶 = (𝑐 ∗
(1r‘𝐴))
→ (𝐶 × 𝑚) = (𝑐 ∗ 𝑚))) | 
| 111 | 110 | ralrimdva 3154 | . . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) ∧ 𝑐 ∈ 𝐾) → (𝐶 = (𝑐 ∗
(1r‘𝐴))
→ ∀𝑚 ∈
𝐵 (𝐶 × 𝑚) = (𝑐 ∗ 𝑚))) | 
| 112 | 111 | reximdva 3168 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → (∃𝑐 ∈ 𝐾 𝐶 = (𝑐 ∗
(1r‘𝐴))
→ ∃𝑐 ∈
𝐾 ∀𝑚 ∈ 𝐵 (𝐶 × 𝑚) = (𝑐 ∗ 𝑚))) | 
| 113 | 8, 112 | mpd 15 | 1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → ∃𝑐 ∈ 𝐾 ∀𝑚 ∈ 𝐵 (𝐶 × 𝑚) = (𝑐 ∗ 𝑚)) |