| Step | Hyp | Ref
| Expression |
| 1 | | mamucl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 3 | | mamuvs1.t |
. . . . . 6
⊢ · =
(.r‘𝑅) |
| 4 | | mamucl.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑅 ∈ Ring) |
| 6 | | mamudi.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑁 ∈ Fin) |
| 8 | | mamuvs1.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑋 ∈ 𝐵) |
| 10 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
| 11 | | mamuvs1.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 12 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁)) → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
| 14 | 13 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
| 15 | | simplrl 777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑀) |
| 16 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
| 17 | 14, 15, 16 | fovcdmd 7605 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖𝑌𝑗) ∈ 𝐵) |
| 18 | | mamuvs1.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂))) |
| 19 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
| 20 | 18, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
| 21 | 20 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
| 22 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑘 ∈ 𝑂) |
| 23 | 21, 16, 22 | fovcdmd 7605 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑗𝑍𝑘) ∈ 𝐵) |
| 24 | 1, 3, 10, 17, 23 | ringcld 20257 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)) ∈ 𝐵) |
| 25 | | eqid 2737 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))) |
| 26 | | ovexd 7466 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)) ∈ V) |
| 27 | | fvexd 6921 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (0g‘𝑅) ∈ V) |
| 28 | 25, 7, 26, 27 | fsuppmptdm 9416 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))) finSupp (0g‘𝑅)) |
| 29 | 1, 2, 3, 5, 7, 9, 24, 28 | gsummulc2 20314 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))))) = (𝑋 · (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))))) |
| 30 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑖(((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝑗) = ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)‘〈𝑖, 𝑗〉) |
| 31 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑖 ∈ 𝑀) |
| 32 | | opelxpi 5722 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
| 33 | 31, 32 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
| 34 | | mamudi.m |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Fin) |
| 35 | | xpfi 9358 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝑀 × 𝑁) ∈ Fin) |
| 36 | 34, 6, 35 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 × 𝑁) ∈ Fin) |
| 37 | 36 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑀 × 𝑁) ∈ Fin) |
| 38 | 8 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐵) |
| 39 | | ffn 6736 |
. . . . . . . . . . . . . 14
⊢ (𝑌:(𝑀 × 𝑁)⟶𝐵 → 𝑌 Fn (𝑀 × 𝑁)) |
| 40 | 11, 12, 39 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 Fn (𝑀 × 𝑁)) |
| 41 | 40 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌 Fn (𝑀 × 𝑁)) |
| 42 | | df-ov 7434 |
. . . . . . . . . . . . . 14
⊢ (𝑖𝑌𝑗) = (𝑌‘〈𝑖, 𝑗〉) |
| 43 | 42 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ (𝑌‘〈𝑖, 𝑗〉) = (𝑖𝑌𝑗) |
| 44 | 43 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) ∧ 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) → (𝑌‘〈𝑖, 𝑗〉) = (𝑖𝑌𝑗)) |
| 45 | 37, 38, 41, 44 | ofc1 7725 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) ∧ 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) → ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)‘〈𝑖, 𝑗〉) = (𝑋 · (𝑖𝑌𝑗))) |
| 46 | 33, 45 | mpdan 687 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)‘〈𝑖, 𝑗〉) = (𝑋 · (𝑖𝑌𝑗))) |
| 47 | 30, 46 | eqtrid 2789 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖(((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝑗) = (𝑋 · (𝑖𝑌𝑗))) |
| 48 | 47 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝑗) · (𝑗𝑍𝑘)) = ((𝑋 · (𝑖𝑌𝑗)) · (𝑗𝑍𝑘))) |
| 49 | 1, 3 | ringass 20250 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ (𝑖𝑌𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵)) → ((𝑋 · (𝑖𝑌𝑗)) · (𝑗𝑍𝑘)) = (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))) |
| 50 | 10, 38, 17, 23, 49 | syl13anc 1374 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑋 · (𝑖𝑌𝑗)) · (𝑗𝑍𝑘)) = (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))) |
| 51 | 48, 50 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝑗) · (𝑗𝑍𝑘)) = (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))) |
| 52 | 51 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝑗) · (𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))))) |
| 53 | 52 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝑗) · (𝑗𝑍𝑘)))) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))))) |
| 54 | | mamudi.f |
. . . . . . 7
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑂〉) |
| 55 | 34 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑀 ∈ Fin) |
| 56 | | mamudi.o |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ Fin) |
| 57 | 56 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑂 ∈ Fin) |
| 58 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 59 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂))) |
| 60 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑘 ∈ 𝑂) |
| 61 | 54, 1, 3, 5, 55, 7,
57, 58, 59, 31, 60 | mamufv 22398 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑌𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))))) |
| 62 | 61 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘)) = (𝑋 · (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))))) |
| 63 | 29, 53, 62 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝑗) · (𝑗𝑍𝑘)))) = (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘))) |
| 64 | | fconst6g 6797 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 → ((𝑀 × 𝑁) × {𝑋}):(𝑀 × 𝑁)⟶𝐵) |
| 65 | 8, 64 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 × 𝑁) × {𝑋}):(𝑀 × 𝑁)⟶𝐵) |
| 66 | 1 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
| 67 | | elmapg 8879 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ (𝑀 × 𝑁) ∈ Fin) → (((𝑀 × 𝑁) × {𝑋}) ∈ (𝐵 ↑m (𝑀 × 𝑁)) ↔ ((𝑀 × 𝑁) × {𝑋}):(𝑀 × 𝑁)⟶𝐵)) |
| 68 | 66, 36, 67 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → (((𝑀 × 𝑁) × {𝑋}) ∈ (𝐵 ↑m (𝑀 × 𝑁)) ↔ ((𝑀 × 𝑁) × {𝑋}):(𝑀 × 𝑁)⟶𝐵)) |
| 69 | 65, 68 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 × 𝑁) × {𝑋}) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 70 | 1, 3 | ringvcl 22404 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ ((𝑀 × 𝑁) × {𝑋}) ∈ (𝐵 ↑m (𝑀 × 𝑁)) ∧ 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) → (((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 71 | 4, 69, 11, 70 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 72 | 71 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
| 73 | 54, 1, 3, 5, 55, 7,
57, 72, 59, 31, 60 | mamufv 22398 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝑗) · (𝑗𝑍𝑘))))) |
| 74 | | df-ov 7434 |
. . . . 5
⊢ (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))𝑘) = ((((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) |
| 75 | | opelxpi 5722 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
| 76 | 75 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
| 77 | | xpfi 9358 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Fin ∧ 𝑂 ∈ Fin) → (𝑀 × 𝑂) ∈ Fin) |
| 78 | 34, 56, 77 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 × 𝑂) ∈ Fin) |
| 79 | 78 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑀 × 𝑂) ∈ Fin) |
| 80 | 1, 4, 54, 34, 6, 56, 11, 18 | mamucl 22405 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 81 | | elmapi 8889 |
. . . . . . . . 9
⊢ ((𝑌𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → (𝑌𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
| 82 | | ffn 6736 |
. . . . . . . . 9
⊢ ((𝑌𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 83 | 80, 81, 82 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 84 | 83 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 85 | | df-ov 7434 |
. . . . . . . . 9
⊢ (𝑖(𝑌𝐹𝑍)𝑘) = ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉) |
| 86 | 85 | eqcomi 2746 |
. . . . . . . 8
⊢ ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉) = (𝑖(𝑌𝐹𝑍)𝑘) |
| 87 | 86 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) → ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉) = (𝑖(𝑌𝐹𝑍)𝑘)) |
| 88 | 79, 9, 84, 87 | ofc1 7725 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) → ((((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) = (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘))) |
| 89 | 76, 88 | mpdan 687 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → ((((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) = (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘))) |
| 90 | 74, 89 | eqtrid 2789 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))𝑘) = (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘))) |
| 91 | 63, 73, 90 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍)𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))𝑘)) |
| 92 | 91 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍)𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))𝑘)) |
| 93 | 1, 4, 54, 34, 6, 56, 71, 18 | mamucl 22405 |
. . . 4
⊢ (𝜑 → ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 94 | | elmapi 8889 |
. . . 4
⊢
(((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
| 95 | | ffn 6736 |
. . . 4
⊢
(((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 96 | 93, 94, 95 | 3syl 18 |
. . 3
⊢ (𝜑 → ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂)) |
| 97 | | fconst6g 6797 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → ((𝑀 × 𝑂) × {𝑋}):(𝑀 × 𝑂)⟶𝐵) |
| 98 | 8, 97 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑀 × 𝑂) × {𝑋}):(𝑀 × 𝑂)⟶𝐵) |
| 99 | | elmapg 8879 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ (𝑀 × 𝑂) ∈ Fin) → (((𝑀 × 𝑂) × {𝑋}) ∈ (𝐵 ↑m (𝑀 × 𝑂)) ↔ ((𝑀 × 𝑂) × {𝑋}):(𝑀 × 𝑂)⟶𝐵)) |
| 100 | 66, 78, 99 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (((𝑀 × 𝑂) × {𝑋}) ∈ (𝐵 ↑m (𝑀 × 𝑂)) ↔ ((𝑀 × 𝑂) × {𝑋}):(𝑀 × 𝑂)⟶𝐵)) |
| 101 | 98, 100 | mpbird 257 |
. . . . 5
⊢ (𝜑 → ((𝑀 × 𝑂) × {𝑋}) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 102 | 1, 3 | ringvcl 22404 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑀 × 𝑂) × {𝑋}) ∈ (𝐵 ↑m (𝑀 × 𝑂)) ∧ (𝑌𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) → (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 103 | 4, 101, 80, 102 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
| 104 | | elmapi 8889 |
. . . 4
⊢ ((((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵) |
| 105 | | ffn 6736 |
. . . 4
⊢ ((((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵 → (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) |
| 106 | 103, 104,
105 | 3syl 18 |
. . 3
⊢ (𝜑 → (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) |
| 107 | | eqfnov2 7563 |
. . 3
⊢
((((((𝑀 ×
𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂) ∧ (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) → (((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) = (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍)𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))𝑘))) |
| 108 | 96, 106, 107 | syl2anc 584 |
. 2
⊢ (𝜑 → (((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) = (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍)𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))𝑘))) |
| 109 | 92, 108 | mpbird 257 |
1
⊢ (𝜑 → ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) = (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍))) |