| Step | Hyp | Ref
| Expression |
| 1 | | mamucl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 2 | | mamucl.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 3 | 2 | ringcmnd 20281 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ CMnd) |
| 4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑅 ∈ CMnd) |
| 5 | | mamuass.o |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ Fin) |
| 6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑂 ∈ Fin) |
| 7 | | mamuass.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑁 ∈ Fin) |
| 9 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 10 | 2 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → 𝑅 ∈ Ring) |
| 11 | | mamuass.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 12 | | elmapi 8889 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
| 14 | 13 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
| 15 | | simplrl 777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑖 ∈ 𝑀) |
| 16 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑙 ∈ 𝑁) |
| 17 | 14, 15, 16 | fovcdmd 7605 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → (𝑖𝑋𝑙) ∈ 𝐵) |
| 18 | 17 | adantrl 716 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → (𝑖𝑋𝑙) ∈ 𝐵) |
| 19 | | mamuass.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑂))) |
| 20 | | elmapi 8889 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑂)) → 𝑌:(𝑁 × 𝑂)⟶𝐵) |
| 21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌:(𝑁 × 𝑂)⟶𝐵) |
| 22 | 21 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → 𝑌:(𝑁 × 𝑂)⟶𝐵) |
| 23 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → 𝑙 ∈ 𝑁) |
| 24 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → 𝑗 ∈ 𝑂) |
| 25 | 22, 23, 24 | fovcdmd 7605 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → (𝑙𝑌𝑗) ∈ 𝐵) |
| 26 | | mamuass.z |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑂 × 𝑃))) |
| 27 | | elmapi 8889 |
. . . . . . . . . . . 12
⊢ (𝑍 ∈ (𝐵 ↑m (𝑂 × 𝑃)) → 𝑍:(𝑂 × 𝑃)⟶𝐵) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍:(𝑂 × 𝑃)⟶𝐵) |
| 29 | 28 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑍:(𝑂 × 𝑃)⟶𝐵) |
| 30 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑗 ∈ 𝑂) |
| 31 | | simplrr 778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑘 ∈ 𝑃) |
| 32 | 29, 30, 31 | fovcdmd 7605 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → (𝑗𝑍𝑘) ∈ 𝐵) |
| 33 | 32 | adantrr 717 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → (𝑗𝑍𝑘) ∈ 𝐵) |
| 34 | 1, 9, 10, 25, 33 | ringcld 20257 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → ((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
| 35 | 1, 9, 10, 18, 34 | ringcld 20257 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) ∈ 𝐵) |
| 36 | 1, 4, 6, 8, 35 | gsumcom3fi 19997 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑅 Σg (𝑗 ∈ 𝑂 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))))) = (𝑅 Σg (𝑙 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))))) |
| 37 | | mamuass.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑂〉) |
| 38 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑅 ∈ Ring) |
| 39 | | mamuass.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Fin) |
| 40 | 39 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑀 ∈ Fin) |
| 41 | 7 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑁 ∈ Fin) |
| 42 | 5 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑂 ∈ Fin) |
| 43 | 11 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 44 | 19 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑂))) |
| 45 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → 𝑖 ∈ 𝑀) |
| 46 | 37, 1, 9, 38, 40, 41, 42, 43, 44, 45, 30 | mamufv 22398 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → (𝑖(𝑋𝐹𝑌)𝑗) = (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))))) |
| 47 | 46 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → ((𝑖(𝑋𝐹𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) = ((𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))))(.r‘𝑅)(𝑗𝑍𝑘))) |
| 48 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 49 | 1, 9, 10, 18, 25 | ringcld 20257 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗)) ∈ 𝐵) |
| 50 | 49 | anassrs 467 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) ∧ 𝑙 ∈ 𝑁) → ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗)) ∈ 𝐵) |
| 51 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))) = (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))) |
| 52 | | ovexd 7466 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) ∧ 𝑙 ∈ 𝑁) → ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗)) ∈ V) |
| 53 | | fvexd 6921 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → (0g‘𝑅) ∈ V) |
| 54 | 51, 41, 52, 53 | fsuppmptdm 9416 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))) finSupp (0g‘𝑅)) |
| 55 | 1, 48, 9, 38, 41, 32, 50, 54 | gsummulc1 20313 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ (((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘)))) = ((𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))))(.r‘𝑅)(𝑗𝑍𝑘))) |
| 56 | 1, 9 | ringass 20250 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ ((𝑖𝑋𝑙) ∈ 𝐵 ∧ (𝑙𝑌𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵)) → (((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘)) = ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
| 57 | 10, 18, 25, 33, 56 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ (𝑗 ∈ 𝑂 ∧ 𝑙 ∈ 𝑁)) → (((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘)) = ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
| 58 | 57 | anassrs 467 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) ∧ 𝑙 ∈ 𝑁) → (((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘)) = ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
| 59 | 58 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → (𝑙 ∈ 𝑁 ↦ (((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
| 60 | 59 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ (((𝑖𝑋𝑙)(.r‘𝑅)(𝑙𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘)))) = (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
| 61 | 47, 55, 60 | 3eqtr2d 2783 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑗 ∈ 𝑂) → ((𝑖(𝑋𝐹𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) = (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
| 62 | 61 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑗 ∈ 𝑂 ↦ ((𝑖(𝑋𝐹𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑂 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))))) |
| 63 | 62 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑖(𝑋𝐹𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) = (𝑅 Σg (𝑗 ∈ 𝑂 ↦ (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))))) |
| 64 | | mamuass.i |
. . . . . . . . . 10
⊢ 𝐼 = (𝑅 maMul 〈𝑁, 𝑂, 𝑃〉) |
| 65 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑅 ∈ Ring) |
| 66 | 7 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑁 ∈ Fin) |
| 67 | 5 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑂 ∈ Fin) |
| 68 | | mamuass.p |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ Fin) |
| 69 | 68 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑃 ∈ Fin) |
| 70 | 19 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑂))) |
| 71 | 26 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑍 ∈ (𝐵 ↑m (𝑂 × 𝑃))) |
| 72 | | simplrr 778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → 𝑘 ∈ 𝑃) |
| 73 | 64, 1, 9, 65, 66, 67, 69, 70, 71, 16, 72 | mamufv 22398 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → (𝑙(𝑌𝐼𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
| 74 | 73 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙(𝑌𝐼𝑍)𝑘)) = ((𝑖𝑋𝑙)(.r‘𝑅)(𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
| 75 | 34 | anass1rs 655 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) ∧ 𝑗 ∈ 𝑂) → ((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
| 76 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑂 ↦ ((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑂 ↦ ((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) |
| 77 | | ovexd 7466 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) ∧ 𝑗 ∈ 𝑂) → ((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ V) |
| 78 | | fvexd 6921 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → (0g‘𝑅) ∈ V) |
| 79 | 76, 67, 77, 78 | fsuppmptdm 9416 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → (𝑗 ∈ 𝑂 ↦ ((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) finSupp (0g‘𝑅)) |
| 80 | 1, 48, 9, 65, 67, 17, 75, 79 | gsummulc2 20314 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) = ((𝑖𝑋𝑙)(.r‘𝑅)(𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
| 81 | 74, 80 | eqtr4d 2780 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) ∧ 𝑙 ∈ 𝑁) → ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙(𝑌𝐼𝑍)𝑘)) = (𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
| 82 | 81 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙(𝑌𝐼𝑍)𝑘))) = (𝑙 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))))) |
| 83 | 82 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙(𝑌𝐼𝑍)𝑘)))) = (𝑅 Σg (𝑙 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)((𝑙𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))))) |
| 84 | 36, 63, 83 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑖(𝑋𝐹𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) = (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙(𝑌𝐼𝑍)𝑘))))) |
| 85 | | mamuass.g |
. . . . 5
⊢ 𝐺 = (𝑅 maMul 〈𝑀, 𝑂, 𝑃〉) |
| 86 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑅 ∈ Ring) |
| 87 | 39 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑀 ∈ Fin) |
| 88 | 68 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑃 ∈ Fin) |
| 89 | 1, 2, 37, 39, 7, 5, 11, 19 | mamucl 22405 |
. . . . . 6
⊢ (𝜑 → (𝑋𝐹𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 90 | 89 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑋𝐹𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 91 | 26 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑍 ∈ (𝐵 ↑m (𝑂 × 𝑃))) |
| 92 | | simprl 771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑖 ∈ 𝑀) |
| 93 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑘 ∈ 𝑃) |
| 94 | 85, 1, 9, 86, 87, 6, 88, 90, 91, 92, 93 | mamufv 22398 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑖((𝑋𝐹𝑌)𝐺𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑂 ↦ ((𝑖(𝑋𝐹𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
| 95 | | mamuass.h |
. . . . 5
⊢ 𝐻 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) |
| 96 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 97 | 1, 2, 64, 7, 5, 68, 19, 26 | mamucl 22405 |
. . . . . 6
⊢ (𝜑 → (𝑌𝐼𝑍) ∈ (𝐵 ↑m (𝑁 × 𝑃))) |
| 98 | 97 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑌𝐼𝑍) ∈ (𝐵 ↑m (𝑁 × 𝑃))) |
| 99 | 95, 1, 9, 86, 87, 8, 88, 96, 98, 92, 93 | mamufv 22398 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑖(𝑋𝐻(𝑌𝐼𝑍))𝑘) = (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝑖𝑋𝑙)(.r‘𝑅)(𝑙(𝑌𝐼𝑍)𝑘))))) |
| 100 | 84, 94, 99 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃)) → (𝑖((𝑋𝐹𝑌)𝐺𝑍)𝑘) = (𝑖(𝑋𝐻(𝑌𝐼𝑍))𝑘)) |
| 101 | 100 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑃 (𝑖((𝑋𝐹𝑌)𝐺𝑍)𝑘) = (𝑖(𝑋𝐻(𝑌𝐼𝑍))𝑘)) |
| 102 | 1, 2, 85, 39, 5, 68, 89, 26 | mamucl 22405 |
. . . 4
⊢ (𝜑 → ((𝑋𝐹𝑌)𝐺𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑃))) |
| 103 | | elmapi 8889 |
. . . 4
⊢ (((𝑋𝐹𝑌)𝐺𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑃)) → ((𝑋𝐹𝑌)𝐺𝑍):(𝑀 × 𝑃)⟶𝐵) |
| 104 | | ffn 6736 |
. . . 4
⊢ (((𝑋𝐹𝑌)𝐺𝑍):(𝑀 × 𝑃)⟶𝐵 → ((𝑋𝐹𝑌)𝐺𝑍) Fn (𝑀 × 𝑃)) |
| 105 | 102, 103,
104 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑋𝐹𝑌)𝐺𝑍) Fn (𝑀 × 𝑃)) |
| 106 | 1, 2, 95, 39, 7, 68, 11, 97 | mamucl 22405 |
. . . 4
⊢ (𝜑 → (𝑋𝐻(𝑌𝐼𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑃))) |
| 107 | | elmapi 8889 |
. . . 4
⊢ ((𝑋𝐻(𝑌𝐼𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑃)) → (𝑋𝐻(𝑌𝐼𝑍)):(𝑀 × 𝑃)⟶𝐵) |
| 108 | | ffn 6736 |
. . . 4
⊢ ((𝑋𝐻(𝑌𝐼𝑍)):(𝑀 × 𝑃)⟶𝐵 → (𝑋𝐻(𝑌𝐼𝑍)) Fn (𝑀 × 𝑃)) |
| 109 | 106, 107,
108 | 3syl 18 |
. . 3
⊢ (𝜑 → (𝑋𝐻(𝑌𝐼𝑍)) Fn (𝑀 × 𝑃)) |
| 110 | | eqfnov2 7563 |
. . 3
⊢ ((((𝑋𝐹𝑌)𝐺𝑍) Fn (𝑀 × 𝑃) ∧ (𝑋𝐻(𝑌𝐼𝑍)) Fn (𝑀 × 𝑃)) → (((𝑋𝐹𝑌)𝐺𝑍) = (𝑋𝐻(𝑌𝐼𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑃 (𝑖((𝑋𝐹𝑌)𝐺𝑍)𝑘) = (𝑖(𝑋𝐻(𝑌𝐼𝑍))𝑘))) |
| 111 | 105, 109,
110 | syl2anc 584 |
. 2
⊢ (𝜑 → (((𝑋𝐹𝑌)𝐺𝑍) = (𝑋𝐻(𝑌𝐼𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑃 (𝑖((𝑋𝐹𝑌)𝐺𝑍)𝑘) = (𝑖(𝑋𝐻(𝑌𝐼𝑍))𝑘))) |
| 112 | 101, 111 | mpbird 257 |
1
⊢ (𝜑 → ((𝑋𝐹𝑌)𝐺𝑍) = (𝑋𝐻(𝑌𝐼𝑍))) |