| Step | Hyp | Ref
| Expression |
| 1 | | psrring.s |
. . . . . . . . . . . . 13
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
| 2 | | psrass.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑆) |
| 3 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 4 | | psrdi.a |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝑆) |
| 5 | | psrass.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 6 | | psrass.y |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 7 | 1, 2, 3, 4, 5, 6 | psradd 21957 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 + 𝑌) = (𝑋 ∘f
(+g‘𝑅)𝑌)) |
| 8 | 7 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 + 𝑌)‘𝑥) = ((𝑋 ∘f
(+g‘𝑅)𝑌)‘𝑥)) |
| 9 | 8 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋 + 𝑌)‘𝑥) = ((𝑋 ∘f
(+g‘𝑅)𝑌)‘𝑥)) |
| 10 | | ssrab2 4080 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ⊆ 𝐷 |
| 11 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
| 12 | 10, 11 | sselid 3981 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
| 13 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 14 | | psrass.d |
. . . . . . . . . . . . . . 15
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 15 | 1, 13, 14, 2, 5 | psrelbas 21954 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
| 16 | 15 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
| 17 | 16 | ffnd 6737 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋 Fn 𝐷) |
| 18 | 1, 13, 14, 2, 6 | psrelbas 21954 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
| 19 | 18 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
| 20 | 19 | ffnd 6737 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌 Fn 𝐷) |
| 21 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 22 | 14, 21 | rabex2 5341 |
. . . . . . . . . . . . 13
⊢ 𝐷 ∈ V |
| 23 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝐷 ∈ V) |
| 24 | | inidm 4227 |
. . . . . . . . . . . 12
⊢ (𝐷 ∩ 𝐷) = 𝐷 |
| 25 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ 𝑥 ∈ 𝐷) → (𝑋‘𝑥) = (𝑋‘𝑥)) |
| 26 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ 𝑥 ∈ 𝐷) → (𝑌‘𝑥) = (𝑌‘𝑥)) |
| 27 | 17, 20, 23, 23, 24, 25, 26 | ofval 7708 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ 𝑥 ∈ 𝐷) → ((𝑋 ∘f
(+g‘𝑅)𝑌)‘𝑥) = ((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))) |
| 28 | 12, 27 | mpdan 687 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋 ∘f
(+g‘𝑅)𝑌)‘𝑥) = ((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))) |
| 29 | 9, 28 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋 + 𝑌)‘𝑥) = ((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))) |
| 30 | 29 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) = (((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) |
| 31 | | psrring.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 32 | 31 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑅 ∈ Ring) |
| 33 | 16, 12 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
| 34 | 19, 12 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑌‘𝑥) ∈ (Base‘𝑅)) |
| 35 | | psrass.z |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
| 36 | 1, 13, 14, 2, 35 | psrelbas 21954 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍:𝐷⟶(Base‘𝑅)) |
| 37 | 36 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑍:𝐷⟶(Base‘𝑅)) |
| 38 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
| 39 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} |
| 40 | 14, 39 | psrbagconcl 21947 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
| 41 | 38, 11, 40 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
| 42 | 10, 41 | sselid 3981 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ 𝐷) |
| 43 | 37, 42 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑍‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) |
| 44 | | eqid 2737 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 45 | 13, 3, 44 | ringdir 20259 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ ((𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘𝑥) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅))) → (((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) = (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
| 46 | 32, 33, 34, 43, 45 | syl13anc 1374 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (((𝑋‘𝑥)(+g‘𝑅)(𝑌‘𝑥))(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) = (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
| 47 | 30, 46 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) = (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
| 48 | 47 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))) |
| 49 | 14 | psrbaglefi 21946 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐷 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
| 50 | 49 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
| 51 | 13, 44 | ringcl 20247 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) → ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
| 52 | 32, 33, 43, 51 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
| 53 | 13, 44 | ringcl 20247 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑥) ∈ (Base‘𝑅) ∧ (𝑍‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) → ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
| 54 | 32, 34, 43, 53 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
| 55 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
| 56 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) |
| 57 | 50, 52, 54, 55, 56 | offval2 7717 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) ∘f
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))(+g‘𝑅)((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))) |
| 58 | 48, 57 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) ∘f
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))) |
| 59 | 58 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) = (𝑅 Σg ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) ∘f
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
| 60 | 31 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) |
| 61 | | ringcmn 20279 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
| 62 | 60, 61 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ CMnd) |
| 63 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) |
| 64 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) |
| 65 | 13, 3, 62, 50, 52, 54, 63, 64 | gsummptfidmadd2 19944 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))) ∘f
(+g‘𝑅)(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))) = ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
| 66 | 59, 65 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) = ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
| 67 | 66 | mpteq2dva 5242 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))))) |
| 68 | | psrass.t |
. . 3
⊢ × =
(.r‘𝑆) |
| 69 | 31 | ringgrpd 20239 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 70 | 69 | grpmgmd 18979 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Mgm) |
| 71 | 1, 2, 4, 70, 5, 6 | psraddcl 21958 |
. . 3
⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) |
| 72 | 1, 2, 44, 68, 14, 71, 35 | psrmulfval 21963 |
. 2
⊢ (𝜑 → ((𝑋 + 𝑌) × 𝑍) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝑋 + 𝑌)‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
| 73 | 1, 2, 68, 31, 5, 35 | psrmulcl 21966 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑍) ∈ 𝐵) |
| 74 | 1, 2, 68, 31, 6, 35 | psrmulcl 21966 |
. . . 4
⊢ (𝜑 → (𝑌 × 𝑍) ∈ 𝐵) |
| 75 | 1, 2, 3, 4, 73, 74 | psradd 21957 |
. . 3
⊢ (𝜑 → ((𝑋 × 𝑍) + (𝑌 × 𝑍)) = ((𝑋 × 𝑍) ∘f
(+g‘𝑅)(𝑌 × 𝑍))) |
| 76 | 22 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
| 77 | | ovexd 7466 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) ∈ V) |
| 78 | | ovexd 7466 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))) ∈ V) |
| 79 | 1, 2, 44, 68, 14, 5, 35 | psrmulfval 21963 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑍) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
| 80 | 1, 2, 44, 68, 14, 6, 35 | psrmulfval 21963 |
. . . 4
⊢ (𝜑 → (𝑌 × 𝑍) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥))))))) |
| 81 | 76, 77, 78, 79, 80 | offval2 7717 |
. . 3
⊢ (𝜑 → ((𝑋 × 𝑍) ∘f
(+g‘𝑅)(𝑌 × 𝑍)) = (𝑘 ∈ 𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))))) |
| 82 | 75, 81 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((𝑋 × 𝑍) + (𝑌 × 𝑍)) = (𝑘 ∈ 𝐷 ↦ ((𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑌‘𝑥)(.r‘𝑅)(𝑍‘(𝑘 ∘f − 𝑥)))))))) |
| 83 | 67, 72, 82 | 3eqtr4d 2787 |
1
⊢ (𝜑 → ((𝑋 + 𝑌) × 𝑍) = ((𝑋 × 𝑍) + (𝑌 × 𝑍))) |