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