| Step | Hyp | Ref
| Expression |
| 1 | | mamucl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 2 | | mamudi.p |
. . . . . 6
⊢ + =
(+g‘𝑅) |
| 3 | | mamucl.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 4 | | ringcmn 20279 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
| 5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ CMnd) |
| 6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑅 ∈ CMnd) |
| 7 | | mamudi.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑁 ∈ Fin) |
| 9 | 3 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
| 10 | | mamudi.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 11 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
| 14 | | simplrl 777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑀) |
| 15 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
| 16 | 13, 14, 15 | fovcdmd 7605 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖𝑋𝑗) ∈ 𝐵) |
| 17 | | mamudi.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂))) |
| 18 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
| 19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
| 20 | 19 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
| 21 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑘 ∈ 𝑂) |
| 22 | 20, 15, 21 | fovcdmd 7605 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑗𝑍𝑘) ∈ 𝐵) |
| 23 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 24 | 1, 23 | ringcl 20247 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑋𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
| 25 | 9, 16, 22, 24 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
| 26 | | mamudi.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 27 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁)) → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
| 29 | 28 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
| 30 | 29, 14, 15 | fovcdmd 7605 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖𝑌𝑗) ∈ 𝐵) |
| 31 | 1, 23 | ringcl 20247 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑌𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵) → ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
| 32 | 9, 30, 22, 31 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
| 33 | | eqid 2737 |
. . . . . 6
⊢ (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) |
| 34 | | eqid 2737 |
. . . . . 6
⊢ (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) |
| 35 | 1, 2, 6, 8, 25, 32, 33, 34 | gsummptfidmadd2 19944 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) ∘f + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) = ((𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) + (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
| 36 | 10 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 37 | | ffn 6736 |
. . . . . . . . . . . . 13
⊢ (𝑋:(𝑀 × 𝑁)⟶𝐵 → 𝑋 Fn (𝑀 × 𝑁)) |
| 38 | 36, 11, 37 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑋 Fn (𝑀 × 𝑁)) |
| 39 | 26 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 40 | | ffn 6736 |
. . . . . . . . . . . . 13
⊢ (𝑌:(𝑀 × 𝑁)⟶𝐵 → 𝑌 Fn (𝑀 × 𝑁)) |
| 41 | 39, 27, 40 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌 Fn (𝑀 × 𝑁)) |
| 42 | | mamudi.m |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Fin) |
| 43 | | xpfi 9358 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝑀 × 𝑁) ∈ Fin) |
| 44 | 42, 7, 43 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 × 𝑁) ∈ Fin) |
| 45 | 44 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑀 × 𝑁) ∈ Fin) |
| 46 | | opelxpi 5722 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
| 47 | 46 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂) ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
| 48 | 47 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
| 49 | | fnfvof 7714 |
. . . . . . . . . . . 12
⊢ (((𝑋 Fn (𝑀 × 𝑁) ∧ 𝑌 Fn (𝑀 × 𝑁)) ∧ ((𝑀 × 𝑁) ∈ Fin ∧ 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁))) → ((𝑋 ∘f + 𝑌)‘〈𝑖, 𝑗〉) = ((𝑋‘〈𝑖, 𝑗〉) + (𝑌‘〈𝑖, 𝑗〉))) |
| 50 | 38, 41, 45, 48, 49 | syl22anc 839 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑋 ∘f + 𝑌)‘〈𝑖, 𝑗〉) = ((𝑋‘〈𝑖, 𝑗〉) + (𝑌‘〈𝑖, 𝑗〉))) |
| 51 | | df-ov 7434 |
. . . . . . . . . . 11
⊢ (𝑖(𝑋 ∘f + 𝑌)𝑗) = ((𝑋 ∘f + 𝑌)‘〈𝑖, 𝑗〉) |
| 52 | | df-ov 7434 |
. . . . . . . . . . . 12
⊢ (𝑖𝑋𝑗) = (𝑋‘〈𝑖, 𝑗〉) |
| 53 | | df-ov 7434 |
. . . . . . . . . . . 12
⊢ (𝑖𝑌𝑗) = (𝑌‘〈𝑖, 𝑗〉) |
| 54 | 52, 53 | oveq12i 7443 |
. . . . . . . . . . 11
⊢ ((𝑖𝑋𝑗) + (𝑖𝑌𝑗)) = ((𝑋‘〈𝑖, 𝑗〉) + (𝑌‘〈𝑖, 𝑗〉)) |
| 55 | 50, 51, 54 | 3eqtr4g 2802 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑋 ∘f + 𝑌)𝑗) = ((𝑖𝑋𝑗) + (𝑖𝑌𝑗))) |
| 56 | 55 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) = (((𝑖𝑋𝑗) + (𝑖𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘))) |
| 57 | 1, 2, 23 | ringdir 20259 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ ((𝑖𝑋𝑗) ∈ 𝐵 ∧ (𝑖𝑌𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵)) → (((𝑖𝑋𝑗) + (𝑖𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘)) = (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
| 58 | 9, 16, 30, 22, 57 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (((𝑖𝑋𝑗) + (𝑖𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘)) = (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
| 59 | 56, 58 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) = (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
| 60 | 59 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
| 61 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
| 62 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
| 63 | 8, 25, 32, 61, 62 | offval2 7717 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) ∘f + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) = (𝑗 ∈ 𝑁 ↦ (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
| 64 | 60, 63 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) ∘f + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
| 65 | 64 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) = (𝑅 Σg ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) ∘f + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
| 66 | | mamudi.f |
. . . . . . 7
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑂〉) |
| 67 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑅 ∈ Ring) |
| 68 | 42 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑀 ∈ Fin) |
| 69 | | mamudi.o |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ Fin) |
| 70 | 69 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑂 ∈ Fin) |
| 71 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 72 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂))) |
| 73 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑖 ∈ 𝑀) |
| 74 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑘 ∈ 𝑂) |
| 75 | 66, 1, 23, 67, 68, 8, 70, 71, 72, 73, 74 | mamufv 22398 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑋𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
| 76 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 77 | 66, 1, 23, 67, 68, 8, 70, 76, 72, 73, 74 | mamufv 22398 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑌𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
| 78 | 75, 77 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → ((𝑖(𝑋𝐹𝑍)𝑘) + (𝑖(𝑌𝐹𝑍)𝑘)) = ((𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) + (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
| 79 | 35, 65, 78 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) = ((𝑖(𝑋𝐹𝑍)𝑘) + (𝑖(𝑌𝐹𝑍)𝑘))) |
| 80 | | ringmnd 20240 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
| 81 | 3, 80 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Mnd) |
| 82 | 1, 2 | mndvcl 18810 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)) ∧ 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) → (𝑋 ∘f + 𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 83 | 81, 10, 26, 82 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∘f + 𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 84 | 83 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑋 ∘f + 𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 85 | 66, 1, 23, 67, 68, 8, 70, 84, 72, 73, 74 | mamufv 22398 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
| 86 | 1, 3, 66, 42, 7, 69, 10, 17 | mamucl 22405 |
. . . . . . . 8
⊢ (𝜑 → (𝑋𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 87 | | elmapi 8889 |
. . . . . . . 8
⊢ ((𝑋𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → (𝑋𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
| 88 | | ffn 6736 |
. . . . . . . 8
⊢ ((𝑋𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 89 | 86, 87, 88 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 90 | 89 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 91 | 1, 3, 66, 42, 7, 69, 26, 17 | mamucl 22405 |
. . . . . . . 8
⊢ (𝜑 → (𝑌𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 92 | | elmapi 8889 |
. . . . . . . 8
⊢ ((𝑌𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → (𝑌𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
| 93 | | ffn 6736 |
. . . . . . . 8
⊢ ((𝑌𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 94 | 91, 92, 93 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 95 | 94 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 96 | | xpfi 9358 |
. . . . . . . 8
⊢ ((𝑀 ∈ Fin ∧ 𝑂 ∈ Fin) → (𝑀 × 𝑂) ∈ Fin) |
| 97 | 42, 69, 96 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑀 × 𝑂) ∈ Fin) |
| 98 | 97 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑀 × 𝑂) ∈ Fin) |
| 99 | | opelxpi 5722 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
| 100 | 99 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
| 101 | | fnfvof 7714 |
. . . . . 6
⊢ ((((𝑋𝐹𝑍) Fn (𝑀 × 𝑂) ∧ (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) ∧ ((𝑀 × 𝑂) ∈ Fin ∧ 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂))) → (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) = (((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉) + ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉))) |
| 102 | 90, 95, 98, 100, 101 | syl22anc 839 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) = (((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉) + ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉))) |
| 103 | | df-ov 7434 |
. . . . 5
⊢ (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘) = (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) |
| 104 | | df-ov 7434 |
. . . . . 6
⊢ (𝑖(𝑋𝐹𝑍)𝑘) = ((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉) |
| 105 | | df-ov 7434 |
. . . . . 6
⊢ (𝑖(𝑌𝐹𝑍)𝑘) = ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉) |
| 106 | 104, 105 | oveq12i 7443 |
. . . . 5
⊢ ((𝑖(𝑋𝐹𝑍)𝑘) + (𝑖(𝑌𝐹𝑍)𝑘)) = (((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉) + ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉)) |
| 107 | 102, 103,
106 | 3eqtr4g 2802 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘) = ((𝑖(𝑋𝐹𝑍)𝑘) + (𝑖(𝑌𝐹𝑍)𝑘))) |
| 108 | 79, 85, 107 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘)) |
| 109 | 108 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘)) |
| 110 | 1, 3, 66, 42, 7, 69, 83, 17 | mamucl 22405 |
. . . 4
⊢ (𝜑 → ((𝑋 ∘f + 𝑌)𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 111 | | elmapi 8889 |
. . . 4
⊢ (((𝑋 ∘f + 𝑌)𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → ((𝑋 ∘f + 𝑌)𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
| 112 | | ffn 6736 |
. . . 4
⊢ (((𝑋 ∘f + 𝑌)𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → ((𝑋 ∘f + 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 113 | 110, 111,
112 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑋 ∘f + 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 114 | 1, 2 | mndvcl 18810 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ (𝑋𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) ∧ (𝑌𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 115 | 81, 86, 91, 114 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 116 | | elmapi 8889 |
. . . 4
⊢ (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵) |
| 117 | | ffn 6736 |
. . . 4
⊢ (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵 → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) |
| 118 | 115, 116,
117 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) |
| 119 | | eqfnov2 7563 |
. . 3
⊢ ((((𝑋 ∘f + 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂) ∧ ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) → (((𝑋 ∘f + 𝑌)𝐹𝑍) = ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘))) |
| 120 | 113, 118,
119 | syl2anc 584 |
. 2
⊢ (𝜑 → (((𝑋 ∘f + 𝑌)𝐹𝑍) = ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘))) |
| 121 | 109, 120 | mpbird 257 |
1
⊢ (𝜑 → ((𝑋 ∘f + 𝑌)𝐹𝑍) = ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))) |