Step | Hyp | Ref
| Expression |
1 | | mamucl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
2 | | mamudir.p |
. . . . . 6
⊢ + =
(+g‘𝑅) |
3 | | mamucl.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | ringcmn 18404 |
. . . . . . . 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 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
10 | | mamudir.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) |
11 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁)) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
13 | 12 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
14 | | simplrl 796 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑀) |
15 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
16 | 13, 14, 15 | fovrnd 6704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖𝑋𝑗) ∈ 𝐵) |
17 | | mamudir.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) |
18 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂)) → 𝑌:(𝑁 × 𝑂)⟶𝐵) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌:(𝑁 × 𝑂)⟶𝐵) |
20 | 19 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌:(𝑁 × 𝑂)⟶𝐵) |
21 | | simplrr 797 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑘 ∈ 𝑂) |
22 | 20, 15, 21 | fovrnd 6704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑗𝑌𝑘) ∈ 𝐵) |
23 | | eqid 2610 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
24 | 1, 23 | ringcl 18384 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑋𝑗) ∈ 𝐵 ∧ (𝑗𝑌𝑘) ∈ 𝐵) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)) ∈ 𝐵) |
25 | 9, 16, 22, 24 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)) ∈ 𝐵) |
26 | | mamudir.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) |
27 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂)) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
29 | 28 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
30 | 29, 15, 21 | fovrnd 6704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑗𝑍𝑘) ∈ 𝐵) |
31 | 1, 23 | ringcl 18384 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑋𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
32 | 9, 16, 30, 31 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
33 | | eqid 2610 |
. . . . . 6
⊢ (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘))) |
34 | | eqid 2610 |
. . . . . 6
⊢ (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) |
35 | 1, 2, 6, 8, 25, 32, 33, 34 | gsummptfidmadd2 18149 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘))) ∘𝑓 + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) = ((𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)))) + (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
36 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ (𝑌:(𝑁 × 𝑂)⟶𝐵 → 𝑌 Fn (𝑁 × 𝑂)) |
37 | 20, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌 Fn (𝑁 × 𝑂)) |
38 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ (𝑍:(𝑁 × 𝑂)⟶𝐵 → 𝑍 Fn (𝑁 × 𝑂)) |
39 | 29, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑍 Fn (𝑁 × 𝑂)) |
40 | | mamudi.o |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑂 ∈ Fin) |
41 | | xpfi 8116 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑂 ∈ Fin) → (𝑁 × 𝑂) ∈ Fin) |
42 | 7, 40, 41 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 × 𝑂) ∈ Fin) |
43 | 42 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑁 × 𝑂) ∈ Fin) |
44 | | opelxpi 5072 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑂) → 〈𝑗, 𝑘〉 ∈ (𝑁 × 𝑂)) |
45 | 44 | ancoms 468 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ 𝑂 ∧ 𝑗 ∈ 𝑁) → 〈𝑗, 𝑘〉 ∈ (𝑁 × 𝑂)) |
46 | 45 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂) ∧ 𝑗 ∈ 𝑁) → 〈𝑗, 𝑘〉 ∈ (𝑁 × 𝑂)) |
47 | 46 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 〈𝑗, 𝑘〉 ∈ (𝑁 × 𝑂)) |
48 | | fnfvof 6809 |
. . . . . . . . . . . 12
⊢ (((𝑌 Fn (𝑁 × 𝑂) ∧ 𝑍 Fn (𝑁 × 𝑂)) ∧ ((𝑁 × 𝑂) ∈ Fin ∧ 〈𝑗, 𝑘〉 ∈ (𝑁 × 𝑂))) → ((𝑌 ∘𝑓 + 𝑍)‘〈𝑗, 𝑘〉) = ((𝑌‘〈𝑗, 𝑘〉) + (𝑍‘〈𝑗, 𝑘〉))) |
49 | 37, 39, 43, 47, 48 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑌 ∘𝑓 + 𝑍)‘〈𝑗, 𝑘〉) = ((𝑌‘〈𝑗, 𝑘〉) + (𝑍‘〈𝑗, 𝑘〉))) |
50 | | df-ov 6552 |
. . . . . . . . . . 11
⊢ (𝑗(𝑌 ∘𝑓 + 𝑍)𝑘) = ((𝑌 ∘𝑓 + 𝑍)‘〈𝑗, 𝑘〉) |
51 | | df-ov 6552 |
. . . . . . . . . . . 12
⊢ (𝑗𝑌𝑘) = (𝑌‘〈𝑗, 𝑘〉) |
52 | | df-ov 6552 |
. . . . . . . . . . . 12
⊢ (𝑗𝑍𝑘) = (𝑍‘〈𝑗, 𝑘〉) |
53 | 51, 52 | oveq12i 6561 |
. . . . . . . . . . 11
⊢ ((𝑗𝑌𝑘) + (𝑗𝑍𝑘)) = ((𝑌‘〈𝑗, 𝑘〉) + (𝑍‘〈𝑗, 𝑘〉)) |
54 | 49, 50, 53 | 3eqtr4g 2669 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑗(𝑌 ∘𝑓 + 𝑍)𝑘) = ((𝑗𝑌𝑘) + (𝑗𝑍𝑘))) |
55 | 54 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗(𝑌 ∘𝑓 + 𝑍)𝑘)) = ((𝑖𝑋𝑗)(.r‘𝑅)((𝑗𝑌𝑘) + (𝑗𝑍𝑘)))) |
56 | 1, 2, 23 | ringdi 18389 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ ((𝑖𝑋𝑗) ∈ 𝐵 ∧ (𝑗𝑌𝑘) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵)) → ((𝑖𝑋𝑗)(.r‘𝑅)((𝑗𝑌𝑘) + (𝑗𝑍𝑘))) = (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)) + ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
57 | 9, 16, 22, 30, 56 | syl13anc 1320 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑋𝑗)(.r‘𝑅)((𝑗𝑌𝑘) + (𝑗𝑍𝑘))) = (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)) + ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
58 | 55, 57 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗(𝑌 ∘𝑓 + 𝑍)𝑘)) = (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)) + ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
59 | 58 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗(𝑌 ∘𝑓 + 𝑍)𝑘))) = (𝑗 ∈ 𝑁 ↦ (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)) + ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
60 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)))) |
61 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
62 | 8, 25, 32, 60, 61 | offval2 6812 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘))) ∘𝑓 + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) = (𝑗 ∈ 𝑁 ↦ (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)) + ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
63 | 59, 62 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗(𝑌 ∘𝑓 + 𝑍)𝑘))) = ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘))) ∘𝑓 + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
64 | 63 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗(𝑌 ∘𝑓 + 𝑍)𝑘)))) = (𝑅 Σg ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘))) ∘𝑓 + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
65 | | mamudi.f |
. . . . . . 7
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑂〉) |
66 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑅 ∈ Ring) |
67 | | mamudi.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ Fin) |
68 | 67 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑀 ∈ Fin) |
69 | 40 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑂 ∈ Fin) |
70 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑋 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) |
71 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑌 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) |
72 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑖 ∈ 𝑀) |
73 | | simprr 792 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑘 ∈ 𝑂) |
74 | 65, 1, 23, 66, 68, 8, 69, 70, 71, 72, 73 | mamufv 20012 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑋𝐹𝑌)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘))))) |
75 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) |
76 | 65, 1, 23, 66, 68, 8, 69, 70, 75, 72, 73 | mamufv 20012 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑋𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
77 | 74, 76 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → ((𝑖(𝑋𝐹𝑌)𝑘) + (𝑖(𝑋𝐹𝑍)𝑘)) = ((𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝑘)))) + (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
78 | 35, 64, 77 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗(𝑌 ∘𝑓 + 𝑍)𝑘)))) = ((𝑖(𝑋𝐹𝑌)𝑘) + (𝑖(𝑋𝐹𝑍)𝑘))) |
79 | | ringmnd 18379 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
80 | 3, 79 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Mnd) |
81 | 1, 2 | mndvcl 20016 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝑌 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂)) ∧ 𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) → (𝑌 ∘𝑓 + 𝑍) ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) |
82 | 80, 17, 26, 81 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝑌 ∘𝑓 + 𝑍) ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) |
83 | 82 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑌 ∘𝑓 + 𝑍) ∈ (𝐵 ↑𝑚 (𝑁 × 𝑂))) |
84 | 65, 1, 23, 66, 68, 8, 69, 70, 83, 72, 73 | mamufv 20012 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑋𝐹(𝑌 ∘𝑓 + 𝑍))𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗(𝑌 ∘𝑓 + 𝑍)𝑘))))) |
85 | 1, 3, 65, 67, 7, 40, 10, 17 | mamucl 20026 |
. . . . . . . 8
⊢ (𝜑 → (𝑋𝐹𝑌) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
86 | | elmapi 7765 |
. . . . . . . 8
⊢ ((𝑋𝐹𝑌) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) → (𝑋𝐹𝑌):(𝑀 × 𝑂)⟶𝐵) |
87 | | ffn 5958 |
. . . . . . . 8
⊢ ((𝑋𝐹𝑌):(𝑀 × 𝑂)⟶𝐵 → (𝑋𝐹𝑌) Fn (𝑀 × 𝑂)) |
88 | 85, 86, 87 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑋𝐹𝑌) Fn (𝑀 × 𝑂)) |
89 | 88 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑋𝐹𝑌) Fn (𝑀 × 𝑂)) |
90 | 1, 3, 65, 67, 7, 40, 10, 26 | mamucl 20026 |
. . . . . . . 8
⊢ (𝜑 → (𝑋𝐹𝑍) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
91 | | elmapi 7765 |
. . . . . . . 8
⊢ ((𝑋𝐹𝑍) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) → (𝑋𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
92 | | ffn 5958 |
. . . . . . . 8
⊢ ((𝑋𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) |
93 | 90, 91, 92 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) |
94 | 93 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) |
95 | | xpfi 8116 |
. . . . . . . 8
⊢ ((𝑀 ∈ Fin ∧ 𝑂 ∈ Fin) → (𝑀 × 𝑂) ∈ Fin) |
96 | 67, 40, 95 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑀 × 𝑂) ∈ Fin) |
97 | 96 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑀 × 𝑂) ∈ Fin) |
98 | | opelxpi 5072 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
99 | 98 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
100 | | fnfvof 6809 |
. . . . . 6
⊢ ((((𝑋𝐹𝑌) Fn (𝑀 × 𝑂) ∧ (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) ∧ ((𝑀 × 𝑂) ∈ Fin ∧ 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂))) → (((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))‘〈𝑖, 𝑘〉) = (((𝑋𝐹𝑌)‘〈𝑖, 𝑘〉) + ((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉))) |
101 | 89, 94, 97, 99, 100 | syl22anc 1319 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))‘〈𝑖, 𝑘〉) = (((𝑋𝐹𝑌)‘〈𝑖, 𝑘〉) + ((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉))) |
102 | | df-ov 6552 |
. . . . 5
⊢ (𝑖((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))𝑘) = (((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))‘〈𝑖, 𝑘〉) |
103 | | df-ov 6552 |
. . . . . 6
⊢ (𝑖(𝑋𝐹𝑌)𝑘) = ((𝑋𝐹𝑌)‘〈𝑖, 𝑘〉) |
104 | | df-ov 6552 |
. . . . . 6
⊢ (𝑖(𝑋𝐹𝑍)𝑘) = ((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉) |
105 | 103, 104 | oveq12i 6561 |
. . . . 5
⊢ ((𝑖(𝑋𝐹𝑌)𝑘) + (𝑖(𝑋𝐹𝑍)𝑘)) = (((𝑋𝐹𝑌)‘〈𝑖, 𝑘〉) + ((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉)) |
106 | 101, 102,
105 | 3eqtr4g 2669 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))𝑘) = ((𝑖(𝑋𝐹𝑌)𝑘) + (𝑖(𝑋𝐹𝑍)𝑘))) |
107 | 78, 84, 106 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑋𝐹(𝑌 ∘𝑓 + 𝑍))𝑘) = (𝑖((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))𝑘)) |
108 | 107 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖(𝑋𝐹(𝑌 ∘𝑓 + 𝑍))𝑘) = (𝑖((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))𝑘)) |
109 | 1, 3, 65, 67, 7, 40, 10, 82 | mamucl 20026 |
. . . 4
⊢ (𝜑 → (𝑋𝐹(𝑌 ∘𝑓 + 𝑍)) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
110 | | elmapi 7765 |
. . . 4
⊢ ((𝑋𝐹(𝑌 ∘𝑓 + 𝑍)) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) → (𝑋𝐹(𝑌 ∘𝑓 + 𝑍)):(𝑀 × 𝑂)⟶𝐵) |
111 | | ffn 5958 |
. . . 4
⊢ ((𝑋𝐹(𝑌 ∘𝑓 + 𝑍)):(𝑀 × 𝑂)⟶𝐵 → (𝑋𝐹(𝑌 ∘𝑓 + 𝑍)) Fn (𝑀 × 𝑂)) |
112 | 109, 110,
111 | 3syl 18 |
. . 3
⊢ (𝜑 → (𝑋𝐹(𝑌 ∘𝑓 + 𝑍)) Fn (𝑀 × 𝑂)) |
113 | 1, 2 | mndvcl 20016 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ (𝑋𝐹𝑌) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) ∧ (𝑋𝐹𝑍) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) → ((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
114 | 80, 85, 90, 113 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → ((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂))) |
115 | | elmapi 7765 |
. . . 4
⊢ (((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)) ∈ (𝐵 ↑𝑚 (𝑀 × 𝑂)) → ((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵) |
116 | | ffn 5958 |
. . . 4
⊢ (((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵 → ((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)) Fn (𝑀 × 𝑂)) |
117 | 114, 115,
116 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)) Fn (𝑀 × 𝑂)) |
118 | | eqfnov2 6665 |
. . 3
⊢ (((𝑋𝐹(𝑌 ∘𝑓 + 𝑍)) Fn (𝑀 × 𝑂) ∧ ((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)) Fn (𝑀 × 𝑂)) → ((𝑋𝐹(𝑌 ∘𝑓 + 𝑍)) = ((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖(𝑋𝐹(𝑌 ∘𝑓 + 𝑍))𝑘) = (𝑖((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))𝑘))) |
119 | 112, 117,
118 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝑋𝐹(𝑌 ∘𝑓 + 𝑍)) = ((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖(𝑋𝐹(𝑌 ∘𝑓 + 𝑍))𝑘) = (𝑖((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))𝑘))) |
120 | 108, 119 | mpbird 246 |
1
⊢ (𝜑 → (𝑋𝐹(𝑌 ∘𝑓 + 𝑍)) = ((𝑋𝐹𝑌) ∘𝑓 + (𝑋𝐹𝑍))) |