Step | Hyp | Ref
| Expression |
1 | | eqid 2778 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2778 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | psrmulcl.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | 3 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring) |
5 | | ringcmn 18972 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ CMnd) |
7 | | psrmulcl.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
8 | | reldmpsr 19762 |
. . . . . . . . 9
⊢ Rel dom
mPwSer |
9 | | psrmulcl.s |
. . . . . . . . 9
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
10 | | psrmulcl.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑆) |
11 | 8, 9, 10 | elbasov 16321 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
12 | 7, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
13 | 12 | simpld 490 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ V) |
14 | | psrmulcl.d |
. . . . . . 7
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
15 | 14 | psrbaglefi 19773 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) |
16 | 13, 15 | sylan 575 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ∈ Fin) |
17 | 3 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑅 ∈ Ring) |
18 | 9, 1, 14, 10, 7 | psrelbas 19780 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) |
19 | 18 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑋:𝐷⟶(Base‘𝑅)) |
20 | | simpr 479 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
21 | | breq1 4891 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦 ∘𝑟 ≤ 𝑘 ↔ 𝑥 ∘𝑟 ≤ 𝑘)) |
22 | 21 | elrab 3572 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∘𝑟 ≤ 𝑘)) |
23 | 20, 22 | sylib 210 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑥 ∈ 𝐷 ∧ 𝑥 ∘𝑟 ≤ 𝑘)) |
24 | 23 | simpld 490 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 ∈ 𝐷) |
25 | 19, 24 | ffvelrnd 6626 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
26 | | psrmulcl.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
27 | 9, 1, 14, 10, 26 | psrelbas 19780 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) |
28 | 27 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑌:𝐷⟶(Base‘𝑅)) |
29 | 13 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝐼 ∈ V) |
30 | | simplr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑘 ∈ 𝐷) |
31 | 14 | psrbagf 19766 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ V ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐼⟶ℕ0) |
32 | 29, 24, 31 | syl2anc 579 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥:𝐼⟶ℕ0) |
33 | 23 | simprd 491 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → 𝑥 ∘𝑟 ≤ 𝑘) |
34 | 14 | psrbagcon 19772 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ V ∧ (𝑘 ∈ 𝐷 ∧ 𝑥:𝐼⟶ℕ0 ∧ 𝑥 ∘𝑟
≤ 𝑘)) → ((𝑘 ∘𝑓
− 𝑥) ∈ 𝐷 ∧ (𝑘 ∘𝑓 − 𝑥) ∘𝑟
≤ 𝑘)) |
35 | 29, 30, 32, 33, 34 | syl13anc 1440 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑘 ∘𝑓 − 𝑥) ∈ 𝐷 ∧ (𝑘 ∘𝑓 − 𝑥) ∘𝑟
≤ 𝑘)) |
36 | 35 | simpld 490 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑥) ∈ 𝐷) |
37 | 28, 36 | ffvelrnd 6626 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅)) |
38 | | eqid 2778 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
39 | 1, 38 | ringcl 18952 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝑅)) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))) ∈ (Base‘𝑅)) |
40 | 17, 25, 37, 39 | syl3anc 1439 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))) ∈ (Base‘𝑅)) |
41 | 40 | fmpttd 6651 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))):{𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}⟶(Base‘𝑅)) |
42 | | fvexd 6463 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (0g‘𝑅) ∈ V) |
43 | 41, 16, 42 | fdmfifsupp 8575 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))) finSupp
(0g‘𝑅)) |
44 | 1, 2, 6, 16, 41, 43 | gsumcl 18706 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))) ∈ (Base‘𝑅)) |
45 | 44 | fmpttd 6651 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))):𝐷⟶(Base‘𝑅)) |
46 | | fvex 6461 |
. . . 4
⊢
(Base‘𝑅)
∈ V |
47 | | ovex 6956 |
. . . . 5
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
48 | 14, 47 | rabex2 5053 |
. . . 4
⊢ 𝐷 ∈ V |
49 | 46, 48 | elmap 8171 |
. . 3
⊢ ((𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) ∈ ((Base‘𝑅) ↑𝑚
𝐷) ↔ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))):𝐷⟶(Base‘𝑅)) |
50 | 45, 49 | sylibr 226 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) ∈ ((Base‘𝑅) ↑𝑚
𝐷)) |
51 | | psrmulcl.t |
. . 3
⊢ · =
(.r‘𝑆) |
52 | 9, 10, 38, 51, 14, 7, 26 | psrmulfval 19786 |
. 2
⊢ (𝜑 → (𝑋 · 𝑌) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))))) |
53 | 9, 1, 14, 10, 13 | psrbas 19779 |
. 2
⊢ (𝜑 → 𝐵 = ((Base‘𝑅) ↑𝑚 𝐷)) |
54 | 50, 52, 53 | 3eltr4d 2874 |
1
⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) |