Step | Hyp | Ref
| Expression |
1 | | mamucl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
2 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | mamuvs1.t |
. . . . . 6
⊢ · =
(.r‘𝑅) |
5 | | mamucl.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑅 ∈ Ring) |
7 | | mamudi.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ Fin) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑁 ∈ Fin) |
9 | | mamuvs1.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
10 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑋 ∈ 𝐵) |
11 | 5 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
12 | | mamuvs1.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) |
13 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁)) → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
15 | 14 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
16 | | simplrl 796 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑀) |
17 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
18 | 15, 16, 17 | fovrnd 6704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖𝑌𝑗) ∈ 𝐵) |
19 | | mamuvs1.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) |
20 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂)) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
22 | 21 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
23 | | simplrr 797 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑘 ∈ 𝑂) |
24 | 22, 17, 23 | fovrnd 6704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑗𝑍𝑘) ∈ 𝐵) |
25 | 1, 4 | ringcl 18384 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑌𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵) → ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)) ∈ 𝐵) |
26 | 11, 18, 24, 25 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)) ∈ 𝐵) |
27 | | eqid 2610 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))) |
28 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)) ∈ V |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)) ∈ V) |
30 | | fvex 6113 |
. . . . . . . 8
⊢
(0g‘𝑅) ∈ V |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (0g‘𝑅) ∈ V) |
32 | 27, 8, 29, 31 | fsuppmptdm 8169 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))) finSupp (0g‘𝑅)) |
33 | 1, 2, 3, 4, 6, 8, 10, 26, 32 | gsummulc2 18430 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))))) = (𝑋 · (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))))) |
34 | | df-ov 6552 |
. . . . . . . . . 10
⊢ (𝑖(((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝑗) = ((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)‘〈𝑖, 𝑗〉) |
35 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑖 ∈ 𝑀) |
36 | | opelxpi 5072 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
37 | 35, 36 | sylan 487 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
38 | | mamudi.m |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Fin) |
39 | | xpfi 8116 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝑀 × 𝑁) ∈ Fin) |
40 | 38, 7, 39 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 × 𝑁) ∈ Fin) |
41 | 40 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑀 × 𝑁) ∈ Fin) |
42 | 9 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐵) |
43 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝑌:(𝑀 × 𝑁)⟶𝐵 → 𝑌 Fn (𝑀 × 𝑁)) |
44 | 12, 13, 43 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 Fn (𝑀 × 𝑁)) |
45 | 44 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌 Fn (𝑀 × 𝑁)) |
46 | | df-ov 6552 |
. . . . . . . . . . . . . 14
⊢ (𝑖𝑌𝑗) = (𝑌‘〈𝑖, 𝑗〉) |
47 | 46 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢ (𝑌‘〈𝑖, 𝑗〉) = (𝑖𝑌𝑗) |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) ∧ 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) → (𝑌‘〈𝑖, 𝑗〉) = (𝑖𝑌𝑗)) |
49 | 41, 42, 45, 48 | ofc1 6818 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) ∧ 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) → ((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)‘〈𝑖, 𝑗〉) = (𝑋 · (𝑖𝑌𝑗))) |
50 | 37, 49 | mpdan 699 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)‘〈𝑖, 𝑗〉) = (𝑋 · (𝑖𝑌𝑗))) |
51 | 34, 50 | syl5eq 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖(((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝑗) = (𝑋 · (𝑖𝑌𝑗))) |
52 | 51 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝑗) · (𝑗𝑍𝑘)) = ((𝑋 · (𝑖𝑌𝑗)) · (𝑗𝑍𝑘))) |
53 | 1, 4 | ringass 18387 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ (𝑖𝑌𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵)) → ((𝑋 · (𝑖𝑌𝑗)) · (𝑗𝑍𝑘)) = (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))) |
54 | 11, 42, 18, 24, 53 | syl13anc 1320 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑋 · (𝑖𝑌𝑗)) · (𝑗𝑍𝑘)) = (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))) |
55 | 52, 54 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝑗) · (𝑗𝑍𝑘)) = (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))) |
56 | 55 | mpteq2dva 4672 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝑗) · (𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))))) |
57 | 56 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝑗) · (𝑗𝑍𝑘)))) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ (𝑋 · ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))))) |
58 | | mamudi.f |
. . . . . . 7
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑂〉) |
59 | 38 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑀 ∈ Fin) |
60 | | mamudi.o |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ Fin) |
61 | 60 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑂 ∈ Fin) |
62 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑌 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) |
63 | 19 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) |
64 | | simprr 792 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑘 ∈ 𝑂) |
65 | 58, 1, 4, 6, 59, 8,
61, 62, 63, 35, 64 | mamufv 20012 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑌𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘))))) |
66 | 65 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘)) = (𝑋 · (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗) · (𝑗𝑍𝑘)))))) |
67 | 33, 57, 66 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝑗) · (𝑗𝑍𝑘)))) = (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘))) |
68 | | fconst6g 6007 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 → ((𝑀 × 𝑁) × {𝑋}):(𝑀 × 𝑁)⟶𝐵) |
69 | 9, 68 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 × 𝑁) × {𝑋}):(𝑀 × 𝑁)⟶𝐵) |
70 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
71 | 1, 70 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
72 | | elmapg 7757 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ (𝑀 × 𝑁) ∈ Fin) → (((𝑀 × 𝑁) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁)) ↔ ((𝑀 × 𝑁) × {𝑋}):(𝑀 × 𝑁)⟶𝐵)) |
73 | 71, 40, 72 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → (((𝑀 × 𝑁) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁)) ↔ ((𝑀 × 𝑁) × {𝑋}):(𝑀 × 𝑁)⟶𝐵)) |
74 | 69, 73 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 × 𝑁) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) |
75 | 1, 4 | ringvcl 20023 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ ((𝑀 × 𝑁) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁)) ∧ 𝑌 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) → (((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) |
76 | 5, 74, 12, 75 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) |
77 | 76 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) |
78 | 58, 1, 4, 6, 59, 8,
61, 77, 63, 35, 64 | mamufv 20012 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝑗) · (𝑗𝑍𝑘))))) |
79 | | df-ov 6552 |
. . . . 5
⊢ (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))𝑘) = ((((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) |
80 | | opelxpi 5072 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
81 | 80 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
82 | | xpfi 8116 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Fin ∧ 𝑂 ∈ Fin) → (𝑀 × 𝑂) ∈ Fin) |
83 | 38, 60, 82 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 × 𝑂) ∈ Fin) |
84 | 83 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑀 × 𝑂) ∈ Fin) |
85 | 1, 5, 58, 38, 7, 60, 12, 19 | mamucl 20026 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌𝐹𝑍) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
86 | | elmapi 7765 |
. . . . . . . . 9
⊢ ((𝑌𝐹𝑍) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) → (𝑌𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
87 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑌𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
88 | 85, 86, 87 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
89 | 88 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
90 | | df-ov 6552 |
. . . . . . . . 9
⊢ (𝑖(𝑌𝐹𝑍)𝑘) = ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉) |
91 | 90 | eqcomi 2619 |
. . . . . . . 8
⊢ ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉) = (𝑖(𝑌𝐹𝑍)𝑘) |
92 | 91 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) → ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉) = (𝑖(𝑌𝐹𝑍)𝑘)) |
93 | 84, 10, 89, 92 | ofc1 6818 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) → ((((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) = (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘))) |
94 | 81, 93 | mpdan 699 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → ((((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) = (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘))) |
95 | 79, 94 | syl5eq 2656 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))𝑘) = (𝑋 · (𝑖(𝑌𝐹𝑍)𝑘))) |
96 | 67, 78, 95 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍)𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))𝑘)) |
97 | 96 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍)𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))𝑘)) |
98 | 1, 5, 58, 38, 7, 60, 76, 19 | mamucl 20026 |
. . . 4
⊢ (𝜑 → ((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
99 | | elmapi 7765 |
. . . 4
⊢
(((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) → ((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
100 | | ffn 5958 |
. . . 4
⊢
(((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → ((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂)) |
101 | 98, 99, 100 | 3syl 18 |
. . 3
⊢ (𝜑 → ((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂)) |
102 | | fconst6g 6007 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → ((𝑀 × 𝑂) × {𝑋}):(𝑀 × 𝑂)⟶𝐵) |
103 | 9, 102 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑀 × 𝑂) × {𝑋}):(𝑀 × 𝑂)⟶𝐵) |
104 | | elmapg 7757 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ (𝑀 × 𝑂) ∈ Fin) → (((𝑀 × 𝑂) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) ↔ ((𝑀 × 𝑂) × {𝑋}):(𝑀 × 𝑂)⟶𝐵)) |
105 | 71, 83, 104 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → (((𝑀 × 𝑂) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) ↔ ((𝑀 × 𝑂) × {𝑋}):(𝑀 × 𝑂)⟶𝐵)) |
106 | 103, 105 | mpbird 246 |
. . . . 5
⊢ (𝜑 → ((𝑀 × 𝑂) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
107 | 1, 4 | ringvcl 20023 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑀 × 𝑂) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) ∧ (𝑌𝐹𝑍) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) → (((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
108 | 5, 106, 85, 107 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
109 | | elmapi 7765 |
. . . 4
⊢ ((((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) → (((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵) |
110 | | ffn 5958 |
. . . 4
⊢ ((((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵 → (((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) |
111 | 108, 109,
110 | 3syl 18 |
. . 3
⊢ (𝜑 → (((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) |
112 | | eqfnov2 6665 |
. . 3
⊢
((((((𝑀 ×
𝑁) × {𝑋}) ∘𝑓
·
𝑌)𝐹𝑍) Fn (𝑀 × 𝑂) ∧ (((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) → (((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍) = (((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍)𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))𝑘))) |
113 | 101, 111,
112 | syl2anc 691 |
. 2
⊢ (𝜑 → (((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍) = (((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍)𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))𝑘))) |
114 | 97, 113 | mpbird 246 |
1
⊢ (𝜑 → ((((𝑀 × 𝑁) × {𝑋}) ∘𝑓 · 𝑌)𝐹𝑍) = (((𝑀 × 𝑂) × {𝑋}) ∘𝑓 · (𝑌𝐹𝑍))) |