Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . . . . . . . . . . . 13
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | psrass.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑆) |
3 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | psrdi.a |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝑆) |
5 | | psrass.y |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
6 | | psrass.z |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
7 | 1, 2, 3, 4, 5, 6 | psradd 20754 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 + 𝑍) = (𝑌 ∘f
(+g‘𝑅)𝑍)) |
8 | 7 | fveq1d 6670 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥)) = ((𝑌 ∘f
(+g‘𝑅)𝑍)‘(𝑘 ∘f − 𝑥))) |
9 | 8 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥)) = ((𝑌 ∘f
(+g‘𝑅)𝑍)‘(𝑘 ∘f − 𝑥))) |
10 | | ssrab2 3967 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ⊆ 𝐷 |
11 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
12 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
13 | | psrass.d |
. . . . . . . . . . . . . 14
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
14 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} |
15 | 13, 14 | psrbagconcl 20740 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
16 | 11, 12, 15 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
17 | 10, 16 | sseldi 3873 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ 𝐷) |
18 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅) =
(Base‘𝑅) |
19 | 1, 18, 13, 2, 5 | psrelbas 20751 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
20 | 19 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
21 | 20 | ffnd 6499 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌 Fn 𝐷) |
22 | 1, 18, 13, 2, 6 | psrelbas 20751 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍:𝐷⟶(Base‘𝑅)) |
23 | 22 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑍:𝐷⟶(Base‘𝑅)) |
24 | 23 | ffnd 6499 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑍 Fn 𝐷) |
25 | | ovex 7197 |
. . . . . . . . . . . . . 14
⊢
(ℕ0 ↑m 𝐼) ∈ V |
26 | 13, 25 | rabex2 5199 |
. . . . . . . . . . . . 13
⊢ 𝐷 ∈ V |
27 | 26 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝐷 ∈ V) |
28 | | inidm 4107 |
. . . . . . . . . . . 12
⊢ (𝐷 ∩ 𝐷) = 𝐷 |
29 | | eqidd 2739 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ (𝑘 ∘f − 𝑥) ∈ 𝐷) → (𝑌‘(𝑘 ∘f − 𝑥)) = (𝑌‘(𝑘 ∘f − 𝑥))) |
30 | | eqidd 2739 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ (𝑘 ∘f − 𝑥) ∈ 𝐷) → (𝑍‘(𝑘 ∘f − 𝑥)) = (𝑍‘(𝑘 ∘f − 𝑥))) |
31 | 21, 24, 27, 27, 28, 29, 30 | ofval 7429 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ (𝑘 ∘f − 𝑥) ∈ 𝐷) → ((𝑌 ∘f
(+g‘𝑅)𝑍)‘(𝑘 ∘f − 𝑥)) = ((𝑌‘(𝑘 ∘f − 𝑥))(+g‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) |
32 | 17, 31 | mpdan 687 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑌 ∘f
(+g‘𝑅)𝑍)‘(𝑘 ∘f − 𝑥)) = ((𝑌‘(𝑘 ∘f − 𝑥))(+g‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) |
33 | 9, 32 | eqtrd 2773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥)) = ((𝑌‘(𝑘 ∘f − 𝑥))(+g‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) |
34 | 33 | oveq2d 7180 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥))) = ((𝑋‘𝑥)(.r‘𝑅)((𝑌‘(𝑘 ∘f − 𝑥))(+g‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
35 | | psrring.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
36 | 35 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑅 ∈ Ring) |
37 | | psrass.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
38 | 1, 18, 13, 2, 37 | psrelbas 20751 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
39 | 38 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
40 | 10, 12 | sseldi 3873 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
41 | 39, 40 | ffvelrnd 6856 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
42 | 20, 17 | ffvelrnd 6856 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) |
43 | 23, 17 | ffvelrnd 6856 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑍‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) |
44 | | eqid 2738 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
45 | 18, 3, 44 | ringdi 19431 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ ((𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅))) → ((𝑋‘𝑥)(.r‘𝑅)((𝑌‘(𝑘 ∘f − 𝑥))(+g‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = (((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
46 | 36, 41, 42, 43, 45 | syl13anc 1373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)((𝑌‘(𝑘 ∘f − 𝑥))(+g‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = (((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
47 | 34, 46 | eqtrd 2773 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥))) = (((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
48 | 47 | mpteq2dva 5122 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))) |
49 | 13 | psrbaglefi 20738 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐷 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
50 | 49 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
51 | 18, 44 | ringcl 19426 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
52 | 36, 41, 42, 51 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
53 | 18, 44 | ringcl 19426 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) → ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
54 | 36, 41, 43, 53 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
55 | | eqidd 2739 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) |
56 | | eqidd 2739 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
57 | 50, 52, 54, 55, 56 | offval2 7438 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∘f
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))) |
58 | 48, 57 | eqtr4d 2776 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥)))) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∘f
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))) |
59 | 58 | oveq2d 7180 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥))))) = (𝑅 Σg ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∘f
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
60 | 35 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) |
61 | | ringcmn 19446 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
62 | 60, 61 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ CMnd) |
63 | | eqid 2738 |
. . . . 5
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) |
64 | | eqid 2738 |
. . . . 5
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) |
65 | 18, 3, 62, 50, 52, 54, 63, 64 | gsummptfidmadd2 19158 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∘f
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))) = ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
66 | 59, 65 | eqtrd 2773 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥))))) = ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
67 | 66 | mpteq2dva 5122 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))))) |
68 | | psrass.t |
. . 3
⊢ × =
(.r‘𝑆) |
69 | | ringgrp 19414 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
70 | 35, 69 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Grp) |
71 | 1, 2, 4, 70, 5, 6 | psraddcl 20755 |
. . 3
⊢ (𝜑 → (𝑌 + 𝑍) ∈ 𝐵) |
72 | 1, 2, 44, 68, 13, 37, 71 | psrmulfval 20757 |
. 2
⊢ (𝜑 → (𝑋 × (𝑌 + 𝑍)) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝑌 + 𝑍)‘(𝑘 ∘f − 𝑥))))))) |
73 | 1, 2, 68, 35, 37, 5 | psrmulcl 20760 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑌) ∈ 𝐵) |
74 | 1, 2, 68, 35, 37, 6 | psrmulcl 20760 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑍) ∈ 𝐵) |
75 | 1, 2, 3, 4, 73, 74 | psradd 20754 |
. . 3
⊢ (𝜑 → ((𝑋 × 𝑌) + (𝑋 × 𝑍)) = ((𝑋 × 𝑌) ∘f
(+g‘𝑅)(𝑋 × 𝑍))) |
76 | 26 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
77 | | ovexd 7199 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ V) |
78 | | ovexd 7199 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) ∈ V) |
79 | 1, 2, 44, 68, 13, 37, 5 | psrmulfval 20757 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑌) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
80 | 1, 2, 44, 68, 13, 37, 6 | psrmulfval 20757 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑍) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
81 | 76, 77, 78, 79, 80 | offval2 7438 |
. . 3
⊢ (𝜑 → ((𝑋 × 𝑌) ∘f
(+g‘𝑅)(𝑋 × 𝑍)) = (𝑘 ∈ 𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))))) |
82 | 75, 81 | eqtrd 2773 |
. 2
⊢ (𝜑 → ((𝑋 × 𝑌) + (𝑋 × 𝑍)) = (𝑘 ∈ 𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))))) |
83 | 67, 72, 82 | 3eqtr4d 2783 |
1
⊢ (𝜑 → (𝑋 × (𝑌 + 𝑍)) = ((𝑋 × 𝑌) + (𝑋 × 𝑍))) |