Step | Hyp | Ref
| Expression |
1 | | eqid 2818 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2818 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | psrmulcl.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) |
5 | | ringcmn 19260 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ CMnd) |
7 | | psrmulcl.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
8 | | reldmpsr 20069 |
. . . . . . . . 9
⊢ Rel dom
mPwSer |
9 | | psrmulcl.s |
. . . . . . . . 9
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
10 | | psrmulcl.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑆) |
11 | 8, 9, 10 | elbasov 16533 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
12 | 7, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
13 | 12 | simpld 495 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ V) |
14 | | psrmulcl.d |
. . . . . . 7
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
15 | 14 | psrbaglefi 20080 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
16 | 13, 15 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
17 | 3 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑅 ∈ Ring) |
18 | 9, 1, 14, 10, 7 | psrelbas 20087 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
19 | 18 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
20 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
21 | | breq1 5060 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦 ∘r ≤ 𝑘 ↔ 𝑥 ∘r ≤ 𝑘)) |
22 | 21 | elrab 3677 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∘r ≤ 𝑘)) |
23 | 20, 22 | sylib 219 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑥 ∈ 𝐷 ∧ 𝑥 ∘r ≤ 𝑘)) |
24 | 23 | simpld 495 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
25 | 19, 24 | ffvelrnd 6844 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
26 | | psrmulcl.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
27 | 9, 1, 14, 10, 26 | psrelbas 20087 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
28 | 27 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
29 | 13 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝐼 ∈ V) |
30 | | simplr 765 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
31 | 14 | psrbagf 20073 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ V ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐼⟶ℕ0) |
32 | 29, 24, 31 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥:𝐼⟶ℕ0) |
33 | 23 | simprd 496 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∘r ≤ 𝑘) |
34 | 14 | psrbagcon 20079 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ V ∧ (𝑘 ∈ 𝐷 ∧ 𝑥:𝐼⟶ℕ0 ∧ 𝑥 ∘r ≤ 𝑘)) → ((𝑘 ∘f − 𝑥) ∈ 𝐷 ∧ (𝑘 ∘f − 𝑥) ∘r ≤ 𝑘)) |
35 | 29, 30, 32, 33, 34 | syl13anc 1364 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑘 ∘f − 𝑥) ∈ 𝐷 ∧ (𝑘 ∘f − 𝑥) ∘r ≤ 𝑘)) |
36 | 35 | simpld 495 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ 𝐷) |
37 | 28, 36 | ffvelrnd 6844 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) |
38 | | eqid 2818 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
39 | 1, 38 | ringcl 19240 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
40 | 17, 25, 37, 39 | syl3anc 1363 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
41 | 40 | fmpttd 6871 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))):{𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}⟶(Base‘𝑅)) |
42 | | fvexd 6678 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (0g‘𝑅) ∈ V) |
43 | 41, 16, 42 | fdmfifsupp 8831 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp
(0g‘𝑅)) |
44 | 1, 2, 6, 16, 41, 43 | gsumcl 18964 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ (Base‘𝑅)) |
45 | 44 | fmpttd 6871 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))):𝐷⟶(Base‘𝑅)) |
46 | | fvex 6676 |
. . . 4
⊢
(Base‘𝑅)
∈ V |
47 | | ovex 7178 |
. . . . 5
⊢
(ℕ0 ↑m 𝐼) ∈ V |
48 | 14, 47 | rabex2 5228 |
. . . 4
⊢ 𝐷 ∈ V |
49 | 46, 48 | elmap 8424 |
. . 3
⊢ ((𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) ∈ ((Base‘𝑅) ↑m 𝐷) ↔ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))):𝐷⟶(Base‘𝑅)) |
50 | 45, 49 | sylibr 235 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) ∈ ((Base‘𝑅) ↑m 𝐷)) |
51 | | psrmulcl.t |
. . 3
⊢ · =
(.r‘𝑆) |
52 | 9, 10, 38, 51, 14, 7, 26 | psrmulfval 20093 |
. 2
⊢ (𝜑 → (𝑋 · 𝑌) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
53 | 9, 1, 14, 10, 13 | psrbas 20086 |
. 2
⊢ (𝜑 → 𝐵 = ((Base‘𝑅) ↑m 𝐷)) |
54 | 50, 52, 53 | 3eltr4d 2925 |
1
⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) |