Step | Hyp | Ref
| Expression |
1 | | reldmpsr 19361 |
. . . . . . . . . 10
⊢ Rel dom
mPwSer |
2 | | resspsr.u |
. . . . . . . . . 10
⊢ 𝑈 = (𝐼 mPwSer 𝐻) |
3 | | resspsr.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑈) |
4 | 1, 2, 3 | elbasov 15921 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝐻 ∈ V)) |
5 | 4 | ad2antrl 764 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼 ∈ V ∧ 𝐻 ∈ V)) |
6 | 5 | simpld 475 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐼 ∈ V) |
7 | | eqid 2622 |
. . . . . . . 8
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
8 | 7 | psrbaglefi 19372 |
. . . . . . 7
⊢ ((𝐼 ∈ V ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ∈
Fin) |
9 | 6, 8 | sylan 488 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ∈
Fin) |
10 | | resspsr.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) |
11 | | subrgsubg 18786 |
. . . . . . . . 9
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 ∈ (SubGrp‘𝑅)) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝑅)) |
13 | | subgsubm 17616 |
. . . . . . . 8
⊢ (𝑇 ∈ (SubGrp‘𝑅) → 𝑇 ∈ (SubMnd‘𝑅)) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (SubMnd‘𝑅)) |
15 | 14 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑇 ∈ (SubMnd‘𝑅)) |
16 | 10 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑇 ∈ (SubRing‘𝑅)) |
17 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(Base‘𝐻) =
(Base‘𝐻) |
18 | | simprl 794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
19 | 2, 17, 7, 3, 18 | psrelbas 19379 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
20 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑋:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
21 | | elrabi 3359 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} → 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
22 | | ffvelrn 6357 |
. . . . . . . . . 10
⊢ ((𝑋:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)
∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑋‘𝑥) ∈ (Base‘𝐻)) |
23 | 20, 21, 22 | syl2an 494 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝐻)) |
24 | | resspsr.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝑅 ↾s 𝑇) |
25 | 24 | subrgbas 18789 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 = (Base‘𝐻)) |
26 | 16, 25 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑇 = (Base‘𝐻)) |
27 | 23, 26 | eleqtrrd 2704 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑋‘𝑥) ∈ 𝑇) |
28 | | simprr 796 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
29 | 2, 17, 7, 3, 28 | psrelbas 19379 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
30 | 29 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑌:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
31 | | ssrab2 3687 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ⊆ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
32 | 6 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝐼 ∈ V) |
33 | | simplr 792 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
34 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) |
35 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} = {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} |
36 | 7, 35 | psrbagconcl 19373 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ V ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑘 ∘𝑓
− 𝑥) ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) |
37 | 32, 33, 34, 36 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑘 ∘𝑓
− 𝑥) ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) |
38 | 31, 37 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑘 ∘𝑓
− 𝑥) ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
39 | 30, 38 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝐻)) |
40 | 39, 26 | eleqtrrd 2704 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ 𝑇) |
41 | | eqid 2622 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
42 | 41 | subrgmcl 18792 |
. . . . . . . 8
⊢ ((𝑇 ∈ (SubRing‘𝑅) ∧ (𝑋‘𝑥) ∈ 𝑇 ∧ (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ 𝑇) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))) ∈ 𝑇) |
43 | 16, 27, 40, 42 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))) ∈ 𝑇) |
44 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))) |
45 | 43, 44 | fmptd 6385 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))):{𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}⟶𝑇) |
46 | 9, 15, 45, 24 | gsumsubm 17373 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))) = (𝐻 Σg (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) |
47 | 24, 41 | ressmulr 16006 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) →
(.r‘𝑅) =
(.r‘𝐻)) |
48 | 10, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (.r‘𝑅) = (.r‘𝐻)) |
49 | 48 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) →
(.r‘𝑅) =
(.r‘𝐻)) |
50 | 49 | oveqd 6667 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))) = ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))) |
51 | 50 | mpteq2dva 4744 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))) |
52 | 51 | oveq2d 6666 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐻 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))) = (𝐻 Σg (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) |
53 | 46, 52 | eqtrd 2656 |
. . . 4
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))) = (𝐻 Σg (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) |
54 | 53 | mpteq2dva 4744 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝐻 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))))) |
55 | | resspsr.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
56 | | eqid 2622 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
57 | | eqid 2622 |
. . . 4
⊢
(.r‘𝑆) = (.r‘𝑆) |
58 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
59 | 10, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 = (Base‘𝐻)) |
60 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
61 | 60 | subrgss 18781 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 ⊆ (Base‘𝑅)) |
62 | 10, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆ (Base‘𝑅)) |
63 | 59, 62 | eqsstr3d 3640 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐻) ⊆ (Base‘𝑅)) |
64 | | mapss 7900 |
. . . . . . . 8
⊢
(((Base‘𝑅)
∈ V ∧ (Base‘𝐻) ⊆ (Base‘𝑅)) → ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
65 | 58, 63, 64 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → ((Base‘𝐻) ↑𝑚
{𝑓 ∈
(ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
66 | 65 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
67 | 2, 17, 7, 3, 6 | psrbas 19378 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 = ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
68 | 55, 60, 7, 56, 6 | psrbas 19378 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (Base‘𝑆) = ((Base‘𝑅) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
69 | 66, 67, 68 | 3sstr4d 3648 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 ⊆ (Base‘𝑆)) |
70 | 69, 18 | sseldd 3604 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ (Base‘𝑆)) |
71 | 69, 28 | sseldd 3604 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ (Base‘𝑆)) |
72 | 55, 56, 41, 57, 7, 70, 71 | psrmulfval 19385 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑆)𝑌) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))))) |
73 | | eqid 2622 |
. . . 4
⊢
(.r‘𝐻) = (.r‘𝐻) |
74 | | eqid 2622 |
. . . 4
⊢
(.r‘𝑈) = (.r‘𝑈) |
75 | 2, 3, 73, 74, 7, 18, 28 | psrmulfval 19385 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝐻 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))))) |
76 | 54, 72, 75 | 3eqtr4rd 2667 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑋(.r‘𝑆)𝑌)) |
77 | | fvex 6201 |
. . . . 5
⊢
(Base‘𝑈)
∈ V |
78 | 3, 77 | eqeltri 2697 |
. . . 4
⊢ 𝐵 ∈ V |
79 | | resspsr.p |
. . . . 5
⊢ 𝑃 = (𝑆 ↾s 𝐵) |
80 | 79, 57 | ressmulr 16006 |
. . . 4
⊢ (𝐵 ∈ V →
(.r‘𝑆) =
(.r‘𝑃)) |
81 | 78, 80 | mp1i 13 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (.r‘𝑆) = (.r‘𝑃)) |
82 | 81 | oveqd 6667 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑆)𝑌) = (𝑋(.r‘𝑃)𝑌)) |
83 | 76, 82 | eqtrd 2656 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑋(.r‘𝑃)𝑌)) |