Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2739 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | psrmulcl.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) |
5 | | ringcmn 19801 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ CMnd) |
7 | | psrmulcl.d |
. . . . . . 7
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
8 | 7 | psrbaglefi 21116 |
. . . . . 6
⊢ (𝑘 ∈ 𝐷 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
9 | 8 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ∈ Fin) |
10 | 3 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑅 ∈ Ring) |
11 | | psrmulcl.s |
. . . . . . . . . 10
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
12 | | psrmulcl.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑆) |
13 | | psrmulcl.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
14 | 11, 1, 7, 12, 13 | psrelbas 21129 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
15 | 14 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
16 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) |
17 | | breq1 5081 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦 ∘r ≤ 𝑘 ↔ 𝑥 ∘r ≤ 𝑘)) |
18 | 17 | elrab 3625 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∘r ≤ 𝑘)) |
19 | 16, 18 | sylib 217 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑥 ∈ 𝐷 ∧ 𝑥 ∘r ≤ 𝑘)) |
20 | 19 | simpld 494 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
21 | 15, 20 | ffvelrnd 6956 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
22 | | psrmulcl.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
23 | 11, 1, 7, 12, 22 | psrelbas 21129 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
24 | 23 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
25 | | simplr 765 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
26 | 7 | psrbagf 21102 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → 𝑥:𝐼⟶ℕ0) |
27 | 20, 26 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥:𝐼⟶ℕ0) |
28 | 19 | simprd 495 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → 𝑥 ∘r ≤ 𝑘) |
29 | 7 | psrbagcon 21114 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝐷 ∧ 𝑥:𝐼⟶ℕ0 ∧ 𝑥 ∘r ≤ 𝑘) → ((𝑘 ∘f − 𝑥) ∈ 𝐷 ∧ (𝑘 ∘f − 𝑥) ∘r ≤ 𝑘)) |
30 | 25, 27, 28, 29 | syl3anc 1369 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑘 ∘f − 𝑥) ∈ 𝐷 ∧ (𝑘 ∘f − 𝑥) ∘r ≤ 𝑘)) |
31 | 30 | simpld 494 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑘 ∘f − 𝑥) ∈ 𝐷) |
32 | 24, 31 | ffvelrnd 6956 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) |
33 | | eqid 2739 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
34 | 1, 33 | ringcl 19781 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘f − 𝑥)) ∈ (Base‘𝑅)) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
35 | 10, 21, 32, 34 | syl3anc 1369 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))) ∈ (Base‘𝑅)) |
36 | 35 | fmpttd 6983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))):{𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘}⟶(Base‘𝑅)) |
37 | | fvexd 6783 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (0g‘𝑅) ∈ V) |
38 | 36, 9, 37 | fdmfifsupp 9099 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp
(0g‘𝑅)) |
39 | 1, 2, 6, 9, 36, 38 | gsumcl 19497 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ (Base‘𝑅)) |
40 | 39 | fmpttd 6983 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))):𝐷⟶(Base‘𝑅)) |
41 | | fvex 6781 |
. . . 4
⊢
(Base‘𝑅)
∈ V |
42 | | ovex 7301 |
. . . . 5
⊢
(ℕ0 ↑m 𝐼) ∈ V |
43 | 7, 42 | rabex2 5261 |
. . . 4
⊢ 𝐷 ∈ V |
44 | 41, 43 | elmap 8633 |
. . 3
⊢ ((𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) ∈ ((Base‘𝑅) ↑m 𝐷) ↔ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))):𝐷⟶(Base‘𝑅)) |
45 | 40, 44 | sylibr 233 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))))) ∈ ((Base‘𝑅) ↑m 𝐷)) |
46 | | psrmulcl.t |
. . 3
⊢ · =
(.r‘𝑆) |
47 | 11, 12, 33, 46, 7, 13, 22 | psrmulfval 21135 |
. 2
⊢ (𝜑 → (𝑋 · 𝑌) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))))) |
48 | | reldmpsr 21098 |
. . . . . 6
⊢ Rel dom
mPwSer |
49 | 48, 11, 12 | elbasov 16900 |
. . . . 5
⊢ (𝑋 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
50 | 13, 49 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
51 | 50 | simpld 494 |
. . 3
⊢ (𝜑 → 𝐼 ∈ V) |
52 | 11, 1, 7, 12, 51 | psrbas 21128 |
. 2
⊢ (𝜑 → 𝐵 = ((Base‘𝑅) ↑m 𝐷)) |
53 | 45, 47, 52 | 3eltr4d 2855 |
1
⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) |