Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . 3
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | psrring.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
3 | | psrring.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | psrass.d |
. . 3
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
5 | | psrass.t |
. . 3
⊢ × =
(.r‘𝑆) |
6 | | psrass.b |
. . 3
⊢ 𝐵 = (Base‘𝑆) |
7 | | psrass.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
8 | | psrass.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
9 | | psrass.k |
. . 3
⊢ 𝐾 = (Base‘𝑅) |
10 | | psrass.n |
. . 3
⊢ · = (
·𝑠 ‘𝑆) |
11 | | psrass.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝐾) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | psrass23l 21158 |
. 2
⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) |
13 | | eqid 2739 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
14 | | eqid 2739 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
15 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐴 ∈ 𝐾) |
16 | 15, 9 | eleqtrdi 2850 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐴 ∈ (Base‘𝑅)) |
17 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝐴 ∈ (Base‘𝑅)) |
18 | 8 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌 ∈ 𝐵) |
19 | | ssrab2 4017 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ⊆ 𝐷 |
20 | | simplr 765 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
21 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
22 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} |
23 | 4, 22 | psrbagconcl 21118 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
24 | 20, 21, 23 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
25 | 19, 24 | sselid 3923 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ 𝐷) |
26 | 1, 10, 13, 6, 14, 4, 17, 18, 25 | psrvscaval 21142 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝐴 · 𝑌)‘(𝑘 ∘f − 𝑥)) = (𝐴(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) |
27 | 26 | oveq2d 7284 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)((𝐴 · 𝑌)‘(𝑘 ∘f − 𝑥))) = ((𝑋‘𝑥)(.r‘𝑅)(𝐴(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) |
28 | 7 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋 ∈ 𝐵) |
29 | 1, 13, 4, 6, 28 | psrelbas 21129 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
30 | 19, 21 | sselid 3923 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
31 | 29, 30 | ffvelrnd 6956 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
32 | 1, 13, 4, 6, 18 | psrelbas 21129 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
33 | 32, 25 | ffvelrnd 6956 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) |
34 | | psrcom.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ CRing) |
35 | 34 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑅 ∈ CRing) |
36 | 13, 14 | crngcom 19782 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ (Base‘𝑅)) → (𝑢(.r‘𝑅)𝑣) = (𝑣(.r‘𝑅)𝑢)) |
37 | 36 | 3expb 1118 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ (Base‘𝑅))) → (𝑢(.r‘𝑅)𝑣) = (𝑣(.r‘𝑅)𝑢)) |
38 | 35, 37 | sylan 579 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ (Base‘𝑅))) → (𝑢(.r‘𝑅)𝑣) = (𝑣(.r‘𝑅)𝑢)) |
39 | 3 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑅 ∈ Ring) |
40 | 13, 14 | ringass 19784 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ (Base‘𝑅) ∧ 𝑤 ∈ (Base‘𝑅))) → ((𝑢(.r‘𝑅)𝑣)(.r‘𝑅)𝑤) = (𝑢(.r‘𝑅)(𝑣(.r‘𝑅)𝑤))) |
41 | 39, 40 | sylan 579 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ (Base‘𝑅) ∧ 𝑤 ∈ (Base‘𝑅))) → ((𝑢(.r‘𝑅)𝑣)(.r‘𝑅)𝑤) = (𝑢(.r‘𝑅)(𝑣(.r‘𝑅)𝑤))) |
42 | 31, 17, 33, 38, 41 | caov12d 7484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝐴(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) = (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) |
43 | 27, 42 | eqtrd 2779 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)((𝐴 · 𝑌)‘(𝑘 ∘f − 𝑥))) = (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) |
44 | 43 | mpteq2dva 5178 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝐴 · 𝑌)‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) |
45 | 44 | oveq2d 7284 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝐴 · 𝑌)‘(𝑘 ∘f − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
46 | | eqid 2739 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
47 | | eqid 2739 |
. . . . . 6
⊢
(+g‘𝑅) = (+g‘𝑅) |
48 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) |
49 | 4 | psrbaglefi 21116 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐷 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
50 | 49 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
51 | 13, 14 | ringcl 19781 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
52 | 39, 31, 33, 51 | syl3anc 1369 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
53 | | ovex 7301 |
. . . . . . . . . . 11
⊢
(ℕ0 ↑m 𝐼) ∈ V |
54 | 4, 53 | rabex2 5261 |
. . . . . . . . . 10
⊢ 𝐷 ∈ V |
55 | 54 | mptrabex 7095 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V |
56 | | funmpt 6468 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) |
57 | | fvex 6781 |
. . . . . . . . 9
⊢
(0g‘𝑅) ∈ V |
58 | 55, 56, 57 | 3pm3.2i 1337 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∧
(0g‘𝑅)
∈ V) |
59 | 58 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∧
(0g‘𝑅)
∈ V)) |
60 | | suppssdm 7977 |
. . . . . . . . 9
⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp
(0g‘𝑅))
⊆ dom (𝑥 ∈
{𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) |
61 | | eqid 2739 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) |
62 | 61 | dmmptss 6141 |
. . . . . . . . 9
⊢ dom
(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} |
63 | 60, 62 | sstri 3934 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp
(0g‘𝑅))
⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} |
64 | 63 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp
(0g‘𝑅))
⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
65 | | suppssfifsupp 9104 |
. . . . . . 7
⊢ ((((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) ∧
(0g‘𝑅)
∈ V) ∧ ({𝑦 ∈
𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin ∧ ((𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) supp
(0g‘𝑅))
⊆ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp
(0g‘𝑅)) |
66 | 59, 50, 64, 65 | syl12anc 833 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp
(0g‘𝑅)) |
67 | 13, 46, 47, 14, 48, 50, 16, 52, 66 | gsummulc2 19827 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ (𝐴(.r‘𝑅)((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) = (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
68 | 45, 67 | eqtrd 2779 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝐴 · 𝑌)‘(𝑘 ∘f − 𝑥))))) = (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
69 | 68 | mpteq2dva 5178 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝐴 · 𝑌)‘(𝑘 ∘f − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))) |
70 | 1, 10, 9, 6, 3, 11,
8 | psrvscacl 21143 |
. . . 4
⊢ (𝜑 → (𝐴 · 𝑌) ∈ 𝐵) |
71 | 1, 6, 14, 5, 4, 7,
70 | psrmulfval 21135 |
. . 3
⊢ (𝜑 → (𝑋 × (𝐴 · 𝑌)) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)((𝐴 · 𝑌)‘(𝑘 ∘f − 𝑥))))))) |
72 | 1, 6, 5, 3, 7, 8 | psrmulcl 21138 |
. . . . 5
⊢ (𝜑 → (𝑋 × 𝑌) ∈ 𝐵) |
73 | 1, 10, 9, 6, 14, 4,
11, 72 | psrvsca 21141 |
. . . 4
⊢ (𝜑 → (𝐴 · (𝑋 × 𝑌)) = ((𝐷 × {𝐴}) ∘f
(.r‘𝑅)(𝑋 × 𝑌))) |
74 | 54 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ V) |
75 | | ovex 7301 |
. . . . . 6
⊢ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ V |
76 | 75 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ V) |
77 | | fconstmpt 5648 |
. . . . . 6
⊢ (𝐷 × {𝐴}) = (𝑘 ∈ 𝐷 ↦ 𝐴) |
78 | 77 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐷 × {𝐴}) = (𝑘 ∈ 𝐷 ↦ 𝐴)) |
79 | 1, 6, 14, 5, 4, 7,
8 | psrmulfval 21135 |
. . . . 5
⊢ (𝜑 → (𝑋 × 𝑌) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
80 | 74, 15, 76, 78, 79 | offval2 7544 |
. . . 4
⊢ (𝜑 → ((𝐷 × {𝐴}) ∘f
(.r‘𝑅)(𝑋 × 𝑌)) = (𝑘 ∈ 𝐷 ↦ (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))) |
81 | 73, 80 | eqtrd 2779 |
. . 3
⊢ (𝜑 → (𝐴 · (𝑋 × 𝑌)) = (𝑘 ∈ 𝐷 ↦ (𝐴(.r‘𝑅)(𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))))) |
82 | 69, 71, 81 | 3eqtr4d 2789 |
. 2
⊢ (𝜑 → (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))) |
83 | 12, 82 | jca 511 |
1
⊢ (𝜑 → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))) |