| Step | Hyp | Ref
| Expression |
| 1 | | psrring.s |
. . . . . . . . 9
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
| 2 | | psrass23l.n |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝑆) |
| 3 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 4 | | psrass.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑆) |
| 5 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 6 | | psrass.d |
. . . . . . . . 9
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 7 | | psrass23l.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝐾) |
| 8 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐴 ∈ 𝐾) |
| 9 | | psrass23l.k |
. . . . . . . . . . 11
⊢ 𝐾 = (Base‘𝑅) |
| 10 | 8, 9 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐴 ∈ (Base‘𝑅)) |
| 11 | 10 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝐴 ∈ (Base‘𝑅)) |
| 12 | | psrass.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋 ∈ 𝐵) |
| 14 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ⊆ 𝐷 |
| 15 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
| 16 | 14, 15 | sselid 3981 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
| 17 | 1, 2, 3, 4, 5, 6, 11, 13, 16 | psrvscaval 21970 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝐴 · 𝑋)‘𝑥) = (𝐴(.r‘𝑅)(𝑋‘𝑥))) |
| 18 | 17 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) = ((𝐴(.r‘𝑅)(𝑋‘𝑥))(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) |
| 19 | | psrring.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 20 | 19 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑅 ∈ Ring) |
| 21 | 1, 3, 6, 4, 13 | psrelbas 21954 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
| 22 | 21, 16 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
| 23 | | psrass.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 24 | 23 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌 ∈ 𝐵) |
| 25 | 1, 3, 6, 4, 24 | psrelbas 21954 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
| 26 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} |
| 27 | 6, 26 | psrbagconcl 21947 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
| 28 | 27 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
| 29 | 14, 28 | sselid 3981 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ 𝐷) |
| 30 | 25, 29 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) |
| 31 | 3, 5 | ringass 20250 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (Base‘𝑅) ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅))) → ((𝐴(.r‘𝑅)(𝑋‘𝑥))(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) = (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) |
| 32 | 20, 11, 22, 30, 31 | syl13anc 1374 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝐴(.r‘𝑅)(𝑋‘𝑥))(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) = (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) |
| 33 | 18, 32 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) = (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) |
| 34 | 33 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) |
| 35 | 34 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
| 36 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 37 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) |
| 38 | 6 | psrbaglefi 21946 |
. . . . . 6
⊢ (𝑘 ∈ 𝐷 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
| 39 | 38 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
| 40 | 3, 5, 20, 22, 30 | ringcld 20257 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
| 41 | | ovex 7464 |
. . . . . . . . . 10
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 42 | 6, 41 | rabex2 5341 |
. . . . . . . . 9
⊢ 𝐷 ∈ V |
| 43 | 42 | mptrabex 7245 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V |
| 44 | | funmpt 6604 |
. . . . . . . 8
⊢ Fun
(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) |
| 45 | | fvex 6919 |
. . . . . . . 8
⊢
(0g‘𝑅) ∈ V |
| 46 | 43, 44, 45 | 3pm3.2i 1340 |
. . . . . . 7
⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∧
(0g‘𝑅)
∈ V) |
| 47 | 46 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∧
(0g‘𝑅)
∈ V)) |
| 48 | | suppssdm 8202 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp
(0g‘𝑅))
⊆ dom (𝑥 ∈
{𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) |
| 49 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) |
| 50 | 49 | dmmptss 6261 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} |
| 51 | 48, 50 | sstri 3993 |
. . . . . . 7
⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp
(0g‘𝑅))
⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} |
| 52 | 51 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp
(0g‘𝑅))
⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
| 53 | | suppssfifsupp 9420 |
. . . . . 6
⊢ ((((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∧
(0g‘𝑅)
∈ V) ∧ ({𝑦 ∈
𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp
(0g‘𝑅))
⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp
(0g‘𝑅)) |
| 54 | 47, 39, 52, 53 | syl12anc 837 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp
(0g‘𝑅)) |
| 55 | 3, 36, 5, 37, 39, 10, 40, 54 | gsummulc2 20314 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) = (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
| 56 | 35, 55 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) = (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
| 57 | 56 | mpteq2dva 5242 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))) |
| 58 | | psrass.t |
. . 3
⊢ × =
(.r‘𝑆) |
| 59 | 1, 2, 9, 4, 19, 7,
12 | psrvscacl 21971 |
. . 3
⊢ (𝜑 → (𝐴 · 𝑋) ∈ 𝐵) |
| 60 | 1, 4, 5, 58, 6, 59, 23 | psrmulfval 21963 |
. 2
⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (((𝐴 · 𝑋)‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
| 61 | 1, 4, 58, 19, 12, 23 | psrmulcl 21966 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑌) ∈ 𝐵) |
| 62 | 1, 2, 9, 4, 5, 6, 7, 61 | psrvsca 21969 |
. . 3
⊢ (𝜑 → (𝐴 · (𝑋 × 𝑌)) = ((𝐷 × {𝐴}) ∘f
(.r‘𝑅)(𝑋 × 𝑌))) |
| 63 | 42 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
| 64 | | ovexd 7466 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ V) |
| 65 | | fconstmpt 5747 |
. . . . 5
⊢ (𝐷 × {𝐴}) = (𝑘 ∈ 𝐷 ↦ 𝐴) |
| 66 | 65 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐷 × {𝐴}) = (𝑘 ∈ 𝐷 ↦ 𝐴)) |
| 67 | 1, 4, 5, 58, 6, 12, 23 | psrmulfval 21963 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑌) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
| 68 | 63, 8, 64, 66, 67 | offval2 7717 |
. . 3
⊢ (𝜑 → ((𝐷 × {𝐴}) ∘f
(.r‘𝑅)(𝑋 × 𝑌)) = (𝑘 ∈ 𝐷 ↦ (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))) |
| 69 | 62, 68 | eqtrd 2777 |
. 2
⊢ (𝜑 → (𝐴 · (𝑋 × 𝑌)) = (𝑘 ∈ 𝐷 ↦ (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))) |
| 70 | 57, 60, 69 | 3eqtr4d 2787 |
1
⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) |