Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . . . . . . . . . . . 13
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | psrass.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑆) |
3 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | psrdi.a |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝑆) |
5 | | psrass.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
6 | | psrass.y |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
7 | 1, 2, 3, 4, 5, 6 | psradd 19203 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 + 𝑌) = (𝑋 ∘𝑓
(+g‘𝑅)𝑌)) |
8 | 7 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 + 𝑌)‘𝑥) = ((𝑋 ∘𝑓
(+g‘𝑅)𝑌)‘𝑥)) |
9 | 8 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋 + 𝑌)‘𝑥) = ((𝑋 ∘𝑓
(+g‘𝑅)𝑌)‘𝑥)) |
10 | | ssrab2 3650 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ⊆ 𝐷 |
11 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
12 | 10, 11 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
13 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅) =
(Base‘𝑅) |
14 | | psrass.d |
. . . . . . . . . . . . . . 15
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
15 | 1, 13, 14, 2, 5 | psrelbas 19200 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
16 | 15 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
17 | 16 | ffnd 5959 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑋 Fn 𝐷) |
18 | 1, 13, 14, 2, 6 | psrelbas 19200 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
19 | 18 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
20 | 19 | ffnd 5959 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑌 Fn 𝐷) |
21 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
22 | 14, 21 | rabex2 4742 |
. . . . . . . . . . . . 13
⊢ 𝐷 ∈ V |
23 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝐷 ∈ V) |
24 | | inidm 3784 |
. . . . . . . . . . . 12
⊢ (𝐷 ∩ 𝐷) = 𝐷 |
25 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑥 ∈ 𝐷) → (𝑋‘𝑥) = (𝑋‘𝑥)) |
26 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑥 ∈ 𝐷) → (𝑌‘𝑥) = (𝑌‘𝑥)) |
27 | 17, 20, 23, 23, 24, 25, 26 | ofval 6804 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) ∧ 𝑥 ∈ 𝐷) → ((𝑋 ∘𝑓
(+g‘𝑅)𝑌)‘𝑥) = ((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))) |
28 | 12, 27 | mpdan 699 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋 ∘𝑓
(+g‘𝑅)𝑌)‘𝑥) = ((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))) |
29 | 9, 28 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋 + 𝑌)‘𝑥) = ((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))) |
30 | 29 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))) = (((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) |
31 | | psrring.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
32 | 31 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑅 ∈ Ring) |
33 | 16, 12 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
34 | 19, 12 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑌‘𝑥) ∈ (Base‘𝑅)) |
35 | | psrass.z |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
36 | 1, 13, 14, 2, 35 | psrelbas 19200 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍:𝐷⟶(Base‘𝑅)) |
37 | 36 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑍:𝐷⟶(Base‘𝑅)) |
38 | | psrring.i |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
39 | 38 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝐼 ∈ 𝑉) |
40 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
41 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} |
42 | 14, 41 | psrbagconcl 19194 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑘 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
43 | 39, 40, 11, 42 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
44 | 10, 43 | sseldi 3566 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ 𝐷) |
45 | 37, 44 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑍‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅)) |
46 | | eqid 2610 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
47 | 13, 3, 46 | ringdir 18390 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ ((𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘𝑥) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅))) → (((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))) = (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) |
48 | 32, 33, 34, 45, 47 | syl13anc 1320 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))) = (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) |
49 | 30, 48 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))) = (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) |
50 | 49 | mpteq2dva 4672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))) |
51 | 14 | psrbaglefi 19193 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) |
52 | 38, 51 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) |
53 | 13, 46 | ringcl 18384 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅)) → ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))) ∈ (Base‘𝑅)) |
54 | 32, 33, 45, 53 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))) ∈ (Base‘𝑅)) |
55 | 13, 46 | ringcl 18384 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑥) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅)) → ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))) ∈ (Base‘𝑅)) |
56 | 32, 34, 45, 55 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))) ∈ (Base‘𝑅)) |
57 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) |
58 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) |
59 | 52, 54, 56, 57, 58 | offval2 6812 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) ∘𝑓
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))) |
60 | 50, 59 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) ∘𝑓
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))) |
61 | 60 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) = (𝑅 Σg ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) ∘𝑓
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))))) |
62 | 31 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) |
63 | | ringcmn 18404 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
64 | 62, 63 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ CMnd) |
65 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) |
66 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) |
67 | 13, 3, 64, 52, 54, 56, 65, 66 | gsummptfidmadd2 18149 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))) ∘𝑓
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))) = ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))))) |
68 | 61, 67 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) = ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))))) |
69 | 68 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))))) |
70 | | psrass.t |
. . 3
⊢ × =
(.r‘𝑆) |
71 | | ringgrp 18375 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
72 | 31, 71 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Grp) |
73 | 1, 2, 4, 72, 5, 6 | psraddcl 19204 |
. . 3
⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) |
74 | 1, 2, 46, 70, 14, 73, 35 | psrmulfval 19206 |
. 2
⊢ (𝜑 → ((𝑋 + 𝑌) × 𝑍) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))))) |
75 | 1, 2, 70, 31, 5, 35 | psrmulcl 19209 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑍) ∈ 𝐵) |
76 | 1, 2, 70, 31, 6, 35 | psrmulcl 19209 |
. . . 4
⊢ (𝜑 → (𝑌 × 𝑍) ∈ 𝐵) |
77 | 1, 2, 3, 4, 75, 76 | psradd 19203 |
. . 3
⊢ (𝜑 → ((𝑋 × 𝑍) + (𝑌 × 𝑍)) = ((𝑋 × 𝑍) ∘𝑓
(+g‘𝑅)(𝑌 × 𝑍))) |
78 | 22 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
79 | | ovex 6577 |
. . . . 5
⊢ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) ∈ V |
80 | 79 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) ∈ V) |
81 | | ovex 6577 |
. . . . 5
⊢ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) ∈ V |
82 | 81 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))) ∈ V) |
83 | 1, 2, 46, 70, 14, 5, 35 | psrmulfval 19206 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑍) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))))) |
84 | 1, 2, 46, 70, 14, 6, 35 | psrmulfval 19206 |
. . . 4
⊢ (𝜑 → (𝑌 × 𝑍) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥))))))) |
85 | 78, 80, 82, 83, 84 | offval2 6812 |
. . 3
⊢ (𝜑 → ((𝑋 × 𝑍) ∘𝑓
(+g‘𝑅)(𝑌 × 𝑍)) = (𝑘 ∈ 𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))))) |
86 | 77, 85 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((𝑋 × 𝑍) + (𝑌 × 𝑍)) = (𝑘 ∈ 𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘𝑓 − 𝑥)))))))) |
87 | 69, 74, 86 | 3eqtr4d 2654 |
1
⊢ (𝜑 → ((𝑋 + 𝑌) × 𝑍) = ((𝑋 × 𝑍) + (𝑌 × 𝑍))) |