Step | Hyp | Ref
| Expression |
1 | | mamucl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
2 | | mamudi.p |
. . . . . 6
⊢ + =
(+g‘𝑅) |
3 | | mamucl.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | ringcmn 19818 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ CMnd) |
6 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑅 ∈ CMnd) |
7 | | mamudi.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ Fin) |
8 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑁 ∈ Fin) |
9 | 3 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
10 | | mamudi.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
11 | | elmapi 8635 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
13 | 12 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
14 | | simplrl 774 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑀) |
15 | | simpr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
16 | 13, 14, 15 | fovrnd 7444 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖𝑋𝑗) ∈ 𝐵) |
17 | | mamudi.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂))) |
18 | | elmapi 8635 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
20 | 19 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑍:(𝑁 × 𝑂)⟶𝐵) |
21 | | simplrr 775 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑘 ∈ 𝑂) |
22 | 20, 15, 21 | fovrnd 7444 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑗𝑍𝑘) ∈ 𝐵) |
23 | | eqid 2738 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
24 | 1, 23 | ringcl 19798 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑋𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
25 | 9, 16, 22, 24 | syl3anc 1370 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
26 | | mamudi.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
27 | | elmapi 8635 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁)) → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
29 | 28 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌:(𝑀 × 𝑁)⟶𝐵) |
30 | 29, 14, 15 | fovrnd 7444 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖𝑌𝑗) ∈ 𝐵) |
31 | 1, 23 | ringcl 19798 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑌𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵) → ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
32 | 9, 30, 22, 31 | syl3anc 1370 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) ∈ 𝐵) |
33 | | eqid 2738 |
. . . . . 6
⊢ (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) |
34 | | eqid 2738 |
. . . . . 6
⊢ (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) |
35 | 1, 2, 6, 8, 25, 32, 33, 34 | gsummptfidmadd2 19525 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) ∘f + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) = ((𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) + (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
36 | 10 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
37 | | ffn 6602 |
. . . . . . . . . . . . 13
⊢ (𝑋:(𝑀 × 𝑁)⟶𝐵 → 𝑋 Fn (𝑀 × 𝑁)) |
38 | 36, 11, 37 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑋 Fn (𝑀 × 𝑁)) |
39 | 26 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
40 | | ffn 6602 |
. . . . . . . . . . . . 13
⊢ (𝑌:(𝑀 × 𝑁)⟶𝐵 → 𝑌 Fn (𝑀 × 𝑁)) |
41 | 39, 27, 40 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 𝑌 Fn (𝑀 × 𝑁)) |
42 | | mamudi.m |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Fin) |
43 | | xpfi 9083 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝑀 × 𝑁) ∈ Fin) |
44 | 42, 7, 43 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 × 𝑁) ∈ Fin) |
45 | 44 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑀 × 𝑁) ∈ Fin) |
46 | | opelxpi 5628 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
47 | 46 | adantlr 712 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂) ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
48 | 47 | adantll 711 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁)) |
49 | | fnfvof 7550 |
. . . . . . . . . . . 12
⊢ (((𝑋 Fn (𝑀 × 𝑁) ∧ 𝑌 Fn (𝑀 × 𝑁)) ∧ ((𝑀 × 𝑁) ∈ Fin ∧ 〈𝑖, 𝑗〉 ∈ (𝑀 × 𝑁))) → ((𝑋 ∘f + 𝑌)‘〈𝑖, 𝑗〉) = ((𝑋‘〈𝑖, 𝑗〉) + (𝑌‘〈𝑖, 𝑗〉))) |
50 | 38, 41, 45, 48, 49 | syl22anc 836 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑋 ∘f + 𝑌)‘〈𝑖, 𝑗〉) = ((𝑋‘〈𝑖, 𝑗〉) + (𝑌‘〈𝑖, 𝑗〉))) |
51 | | df-ov 7280 |
. . . . . . . . . . 11
⊢ (𝑖(𝑋 ∘f + 𝑌)𝑗) = ((𝑋 ∘f + 𝑌)‘〈𝑖, 𝑗〉) |
52 | | df-ov 7280 |
. . . . . . . . . . . 12
⊢ (𝑖𝑋𝑗) = (𝑋‘〈𝑖, 𝑗〉) |
53 | | df-ov 7280 |
. . . . . . . . . . . 12
⊢ (𝑖𝑌𝑗) = (𝑌‘〈𝑖, 𝑗〉) |
54 | 52, 53 | oveq12i 7289 |
. . . . . . . . . . 11
⊢ ((𝑖𝑋𝑗) + (𝑖𝑌𝑗)) = ((𝑋‘〈𝑖, 𝑗〉) + (𝑌‘〈𝑖, 𝑗〉)) |
55 | 50, 51, 54 | 3eqtr4g 2803 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑋 ∘f + 𝑌)𝑗) = ((𝑖𝑋𝑗) + (𝑖𝑌𝑗))) |
56 | 55 | oveq1d 7292 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) = (((𝑖𝑋𝑗) + (𝑖𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘))) |
57 | 1, 2, 23 | ringdir 19804 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ ((𝑖𝑋𝑗) ∈ 𝐵 ∧ (𝑖𝑌𝑗) ∈ 𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵)) → (((𝑖𝑋𝑗) + (𝑖𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘)) = (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
58 | 9, 16, 30, 22, 57 | syl13anc 1371 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → (((𝑖𝑋𝑗) + (𝑖𝑌𝑗))(.r‘𝑅)(𝑗𝑍𝑘)) = (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
59 | 56, 58 | eqtrd 2778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) = (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
60 | 59 | mpteq2dva 5176 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
61 | | eqidd 2739 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
62 | | eqidd 2739 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) |
63 | 8, 25, 32, 61, 62 | offval2 7553 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) ∘f + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) = (𝑗 ∈ 𝑁 ↦ (((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)) + ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
64 | 60, 63 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) = ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) ∘f + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
65 | 64 | oveq2d 7293 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) = (𝑅 Σg ((𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))) ∘f + (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
66 | | mamudi.f |
. . . . . . 7
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑂〉) |
67 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑅 ∈ Ring) |
68 | 42 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑀 ∈ Fin) |
69 | | mamudi.o |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ Fin) |
70 | 69 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑂 ∈ Fin) |
71 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
72 | 17 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂))) |
73 | | simprl 768 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑖 ∈ 𝑀) |
74 | | simprr 770 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑘 ∈ 𝑂) |
75 | 66, 1, 23, 67, 68, 8, 70, 71, 72, 73, 74 | mamufv 21534 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑋𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
76 | 26 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
77 | 66, 1, 23, 67, 68, 8, 70, 76, 72, 73, 74 | mamufv 21534 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖(𝑌𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
78 | 75, 77 | oveq12d 7295 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → ((𝑖(𝑋𝐹𝑍)𝑘) + (𝑖(𝑌𝐹𝑍)𝑘)) = ((𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) + (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑌𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))))) |
79 | 35, 65, 78 | 3eqtr4d 2788 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘)))) = ((𝑖(𝑋𝐹𝑍)𝑘) + (𝑖(𝑌𝐹𝑍)𝑘))) |
80 | | ringmnd 19791 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
81 | 3, 80 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Mnd) |
82 | 1, 2 | mndvcl 21538 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)) ∧ 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁))) → (𝑋 ∘f + 𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
83 | 81, 10, 26, 82 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∘f + 𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
84 | 83 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑋 ∘f + 𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
85 | 66, 1, 23, 67, 68, 8, 70, 84, 72, 73, 74 | mamufv 21534 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 ∘f + 𝑌)𝑗)(.r‘𝑅)(𝑗𝑍𝑘))))) |
86 | 1, 3, 66, 42, 7, 69, 10, 17 | mamucl 21546 |
. . . . . . . 8
⊢ (𝜑 → (𝑋𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
87 | | elmapi 8635 |
. . . . . . . 8
⊢ ((𝑋𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → (𝑋𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
88 | | ffn 6602 |
. . . . . . . 8
⊢ ((𝑋𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) |
89 | 86, 87, 88 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) |
90 | 89 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂)) |
91 | 1, 3, 66, 42, 7, 69, 26, 17 | mamucl 21546 |
. . . . . . . 8
⊢ (𝜑 → (𝑌𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
92 | | elmapi 8635 |
. . . . . . . 8
⊢ ((𝑌𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → (𝑌𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
93 | | ffn 6602 |
. . . . . . . 8
⊢ ((𝑌𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
94 | 91, 92, 93 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
95 | 94 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) |
96 | | xpfi 9083 |
. . . . . . . 8
⊢ ((𝑀 ∈ Fin ∧ 𝑂 ∈ Fin) → (𝑀 × 𝑂) ∈ Fin) |
97 | 42, 69, 96 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑀 × 𝑂) ∈ Fin) |
98 | 97 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑀 × 𝑂) ∈ Fin) |
99 | | opelxpi 5628 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
100 | 99 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂)) |
101 | | fnfvof 7550 |
. . . . . 6
⊢ ((((𝑋𝐹𝑍) Fn (𝑀 × 𝑂) ∧ (𝑌𝐹𝑍) Fn (𝑀 × 𝑂)) ∧ ((𝑀 × 𝑂) ∈ Fin ∧ 〈𝑖, 𝑘〉 ∈ (𝑀 × 𝑂))) → (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) = (((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉) + ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉))) |
102 | 90, 95, 98, 100, 101 | syl22anc 836 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) = (((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉) + ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉))) |
103 | | df-ov 7280 |
. . . . 5
⊢ (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘) = (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))‘〈𝑖, 𝑘〉) |
104 | | df-ov 7280 |
. . . . . 6
⊢ (𝑖(𝑋𝐹𝑍)𝑘) = ((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉) |
105 | | df-ov 7280 |
. . . . . 6
⊢ (𝑖(𝑌𝐹𝑍)𝑘) = ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉) |
106 | 104, 105 | oveq12i 7289 |
. . . . 5
⊢ ((𝑖(𝑋𝐹𝑍)𝑘) + (𝑖(𝑌𝐹𝑍)𝑘)) = (((𝑋𝐹𝑍)‘〈𝑖, 𝑘〉) + ((𝑌𝐹𝑍)‘〈𝑖, 𝑘〉)) |
107 | 102, 103,
106 | 3eqtr4g 2803 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘) = ((𝑖(𝑋𝐹𝑍)𝑘) + (𝑖(𝑌𝐹𝑍)𝑘))) |
108 | 79, 85, 107 | 3eqtr4d 2788 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂)) → (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘)) |
109 | 108 | ralrimivva 3111 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘)) |
110 | 1, 3, 66, 42, 7, 69, 83, 17 | mamucl 21546 |
. . . 4
⊢ (𝜑 → ((𝑋 ∘f + 𝑌)𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
111 | | elmapi 8635 |
. . . 4
⊢ (((𝑋 ∘f + 𝑌)𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → ((𝑋 ∘f + 𝑌)𝐹𝑍):(𝑀 × 𝑂)⟶𝐵) |
112 | | ffn 6602 |
. . . 4
⊢ (((𝑋 ∘f + 𝑌)𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → ((𝑋 ∘f + 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂)) |
113 | 110, 111,
112 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑋 ∘f + 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂)) |
114 | 1, 2 | mndvcl 21538 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ (𝑋𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂)) ∧ (𝑌𝐹𝑍) ∈ (𝐵 ↑m (𝑀 × 𝑂))) → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
115 | 81, 86, 91, 114 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑂))) |
116 | | elmapi 8635 |
. . . 4
⊢ (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ∈ (𝐵 ↑m (𝑀 × 𝑂)) → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵) |
117 | | ffn 6602 |
. . . 4
⊢ (((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵 → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) |
118 | 115, 116,
117 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) |
119 | | eqfnov2 7404 |
. . 3
⊢ ((((𝑋 ∘f + 𝑌)𝐹𝑍) Fn (𝑀 × 𝑂) ∧ ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) Fn (𝑀 × 𝑂)) → (((𝑋 ∘f + 𝑌)𝐹𝑍) = ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘))) |
120 | 113, 118,
119 | syl2anc 584 |
. 2
⊢ (𝜑 → (((𝑋 ∘f + 𝑌)𝐹𝑍) = ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)) ↔ ∀𝑖 ∈ 𝑀 ∀𝑘 ∈ 𝑂 (𝑖((𝑋 ∘f + 𝑌)𝐹𝑍)𝑘) = (𝑖((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))𝑘))) |
121 | 109, 120 | mpbird 256 |
1
⊢ (𝜑 → ((𝑋 ∘f + 𝑌)𝐹𝑍) = ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍))) |