| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mamurid.f | . . . . 5
⊢ 𝐹 = (𝑅 maMul 〈𝑁, 𝑀, 𝑀〉) | 
| 2 |  | mamumat1cl.b | . . . . 5
⊢ 𝐵 = (Base‘𝑅) | 
| 3 |  | eqid 2737 | . . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 4 |  | mamumat1cl.r | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 5 | 4 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑅 ∈ Ring) | 
| 6 |  | mamulid.n | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ Fin) | 
| 7 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑁 ∈ Fin) | 
| 8 |  | mamumat1cl.m | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ Fin) | 
| 9 | 8 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑀 ∈ Fin) | 
| 10 |  | mamurid.x | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑁 × 𝑀))) | 
| 11 | 10 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑋 ∈ (𝐵 ↑m (𝑁 × 𝑀))) | 
| 12 |  | mamumat1cl.o | . . . . . . 7
⊢  1 =
(1r‘𝑅) | 
| 13 |  | mamumat1cl.z | . . . . . . 7
⊢  0 =
(0g‘𝑅) | 
| 14 |  | mamumat1cl.i | . . . . . . 7
⊢ 𝐼 = (𝑖 ∈ 𝑀, 𝑗 ∈ 𝑀 ↦ if(𝑖 = 𝑗, 1 , 0 )) | 
| 15 | 2, 4, 12, 13, 14, 8 | mamumat1cl 22445 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ (𝐵 ↑m (𝑀 × 𝑀))) | 
| 16 | 15 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝐼 ∈ (𝐵 ↑m (𝑀 × 𝑀))) | 
| 17 |  | simprl 771 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑙 ∈ 𝑁) | 
| 18 |  | simprr 773 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑚 ∈ 𝑀) | 
| 19 | 1, 2, 3, 5, 7, 9, 9, 11, 16, 17, 18 | mamufv 22398 | . . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑙(𝑋𝐹𝐼)𝑚) = (𝑅 Σg (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))))) | 
| 20 |  | ringmnd 20240 | . . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | 
| 21 | 5, 20 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑅 ∈ Mnd) | 
| 22 | 4 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑅 ∈ Ring) | 
| 23 |  | elmapi 8889 | . . . . . . . . . 10
⊢ (𝑋 ∈ (𝐵 ↑m (𝑁 × 𝑀)) → 𝑋:(𝑁 × 𝑀)⟶𝐵) | 
| 24 | 10, 23 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑋:(𝑁 × 𝑀)⟶𝐵) | 
| 25 | 24 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑋:(𝑁 × 𝑀)⟶𝐵) | 
| 26 |  | simplrl 777 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑙 ∈ 𝑁) | 
| 27 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑘 ∈ 𝑀) | 
| 28 | 25, 26, 27 | fovcdmd 7605 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → (𝑙𝑋𝑘) ∈ 𝐵) | 
| 29 |  | elmapi 8889 | . . . . . . . . . 10
⊢ (𝐼 ∈ (𝐵 ↑m (𝑀 × 𝑀)) → 𝐼:(𝑀 × 𝑀)⟶𝐵) | 
| 30 | 15, 29 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐼:(𝑀 × 𝑀)⟶𝐵) | 
| 31 | 30 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝐼:(𝑀 × 𝑀)⟶𝐵) | 
| 32 |  | simplrr 778 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑚 ∈ 𝑀) | 
| 33 | 31, 27, 32 | fovcdmd 7605 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → (𝑘𝐼𝑚) ∈ 𝐵) | 
| 34 | 2, 3 | ringcl 20247 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑙𝑋𝑘) ∈ 𝐵 ∧ (𝑘𝐼𝑚) ∈ 𝐵) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) ∈ 𝐵) | 
| 35 | 22, 28, 33, 34 | syl3anc 1373 | . . . . . 6
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) ∈ 𝐵) | 
| 36 | 35 | fmpttd 7135 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))):𝑀⟶𝐵) | 
| 37 |  | simp2 1138 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → 𝑘 ∈ 𝑀) | 
| 38 | 32 | 3adant3 1133 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → 𝑚 ∈ 𝑀) | 
| 39 | 2, 4, 12, 13, 14, 8 | mat1comp 22446 | . . . . . . . . . 10
⊢ ((𝑘 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀) → (𝑘𝐼𝑚) = if(𝑘 = 𝑚, 1 , 0 )) | 
| 40 | 37, 38, 39 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → (𝑘𝐼𝑚) = if(𝑘 = 𝑚, 1 , 0 )) | 
| 41 |  | ifnefalse 4537 | . . . . . . . . . 10
⊢ (𝑘 ≠ 𝑚 → if(𝑘 = 𝑚, 1 , 0 ) = 0 ) | 
| 42 | 41 | 3ad2ant3 1136 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → if(𝑘 = 𝑚, 1 , 0 ) = 0 ) | 
| 43 | 40, 42 | eqtrd 2777 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → (𝑘𝐼𝑚) = 0 ) | 
| 44 | 43 | oveq2d 7447 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) = ((𝑙𝑋𝑘)(.r‘𝑅) 0 )) | 
| 45 | 2, 3, 13 | ringrz 20291 | . . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑙𝑋𝑘) ∈ 𝐵) → ((𝑙𝑋𝑘)(.r‘𝑅) 0 ) = 0 ) | 
| 46 | 22, 28, 45 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → ((𝑙𝑋𝑘)(.r‘𝑅) 0 ) = 0 ) | 
| 47 | 46 | 3adant3 1133 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → ((𝑙𝑋𝑘)(.r‘𝑅) 0 ) = 0 ) | 
| 48 | 44, 47 | eqtrd 2777 | . . . . . 6
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) = 0 ) | 
| 49 | 48, 9 | suppsssn 8226 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))) supp 0 ) ⊆ {𝑚}) | 
| 50 | 2, 13, 21, 9, 18, 36, 49 | gsumpt 19980 | . . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑅 Σg (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))) = ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚)) | 
| 51 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝑙𝑋𝑘) = (𝑙𝑋𝑚)) | 
| 52 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝑘𝐼𝑚) = (𝑚𝐼𝑚)) | 
| 53 | 51, 52 | oveq12d 7449 | . . . . . . 7
⊢ (𝑘 = 𝑚 → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) = ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚))) | 
| 54 |  | eqid 2737 | . . . . . . 7
⊢ (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))) = (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))) | 
| 55 |  | ovex 7464 | . . . . . . 7
⊢ ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚)) ∈ V | 
| 56 | 53, 54, 55 | fvmpt 7016 | . . . . . 6
⊢ (𝑚 ∈ 𝑀 → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚) = ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚))) | 
| 57 | 56 | ad2antll 729 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚) = ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚))) | 
| 58 |  | equequ1 2024 | . . . . . . . . . 10
⊢ (𝑖 = 𝑚 → (𝑖 = 𝑗 ↔ 𝑚 = 𝑗)) | 
| 59 | 58 | ifbid 4549 | . . . . . . . . 9
⊢ (𝑖 = 𝑚 → if(𝑖 = 𝑗, 1 , 0 ) = if(𝑚 = 𝑗, 1 , 0 )) | 
| 60 |  | equequ2 2025 | . . . . . . . . . . 11
⊢ (𝑗 = 𝑚 → (𝑚 = 𝑗 ↔ 𝑚 = 𝑚)) | 
| 61 | 60 | ifbid 4549 | . . . . . . . . . 10
⊢ (𝑗 = 𝑚 → if(𝑚 = 𝑗, 1 , 0 ) = if(𝑚 = 𝑚, 1 , 0 )) | 
| 62 |  | eqid 2737 | . . . . . . . . . . 11
⊢ 𝑚 = 𝑚 | 
| 63 | 62 | iftruei 4532 | . . . . . . . . . 10
⊢ if(𝑚 = 𝑚, 1 , 0 ) = 1 | 
| 64 | 61, 63 | eqtrdi 2793 | . . . . . . . . 9
⊢ (𝑗 = 𝑚 → if(𝑚 = 𝑗, 1 , 0 ) = 1 ) | 
| 65 | 12 | fvexi 6920 | . . . . . . . . 9
⊢  1 ∈
V | 
| 66 | 59, 64, 14, 65 | ovmpo 7593 | . . . . . . . 8
⊢ ((𝑚 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀) → (𝑚𝐼𝑚) = 1 ) | 
| 67 | 66 | anidms 566 | . . . . . . 7
⊢ (𝑚 ∈ 𝑀 → (𝑚𝐼𝑚) = 1 ) | 
| 68 | 67 | oveq2d 7447 | . . . . . 6
⊢ (𝑚 ∈ 𝑀 → ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚)) = ((𝑙𝑋𝑚)(.r‘𝑅) 1 )) | 
| 69 | 68 | ad2antll 729 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚)) = ((𝑙𝑋𝑚)(.r‘𝑅) 1 )) | 
| 70 | 24 | fovcdmda 7604 | . . . . . 6
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑙𝑋𝑚) ∈ 𝐵) | 
| 71 | 2, 3, 12 | ringridm 20267 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑙𝑋𝑚) ∈ 𝐵) → ((𝑙𝑋𝑚)(.r‘𝑅) 1 ) = (𝑙𝑋𝑚)) | 
| 72 | 5, 70, 71 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑙𝑋𝑚)(.r‘𝑅) 1 ) = (𝑙𝑋𝑚)) | 
| 73 | 57, 69, 72 | 3eqtrd 2781 | . . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚) = (𝑙𝑋𝑚)) | 
| 74 | 19, 50, 73 | 3eqtrd 2781 | . . 3
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚)) | 
| 75 | 74 | ralrimivva 3202 | . 2
⊢ (𝜑 → ∀𝑙 ∈ 𝑁 ∀𝑚 ∈ 𝑀 (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚)) | 
| 76 | 2, 4, 1, 6, 8, 8, 10, 15 | mamucl 22405 | . . . . 5
⊢ (𝜑 → (𝑋𝐹𝐼) ∈ (𝐵 ↑m (𝑁 × 𝑀))) | 
| 77 |  | elmapi 8889 | . . . . 5
⊢ ((𝑋𝐹𝐼) ∈ (𝐵 ↑m (𝑁 × 𝑀)) → (𝑋𝐹𝐼):(𝑁 × 𝑀)⟶𝐵) | 
| 78 | 76, 77 | syl 17 | . . . 4
⊢ (𝜑 → (𝑋𝐹𝐼):(𝑁 × 𝑀)⟶𝐵) | 
| 79 | 78 | ffnd 6737 | . . 3
⊢ (𝜑 → (𝑋𝐹𝐼) Fn (𝑁 × 𝑀)) | 
| 80 | 24 | ffnd 6737 | . . 3
⊢ (𝜑 → 𝑋 Fn (𝑁 × 𝑀)) | 
| 81 |  | eqfnov2 7563 | . . 3
⊢ (((𝑋𝐹𝐼) Fn (𝑁 × 𝑀) ∧ 𝑋 Fn (𝑁 × 𝑀)) → ((𝑋𝐹𝐼) = 𝑋 ↔ ∀𝑙 ∈ 𝑁 ∀𝑚 ∈ 𝑀 (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚))) | 
| 82 | 79, 80, 81 | syl2anc 584 | . 2
⊢ (𝜑 → ((𝑋𝐹𝐼) = 𝑋 ↔ ∀𝑙 ∈ 𝑁 ∀𝑚 ∈ 𝑀 (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚))) | 
| 83 | 75, 82 | mpbird 257 | 1
⊢ (𝜑 → (𝑋𝐹𝐼) = 𝑋) |