Step | Hyp | Ref
| Expression |
1 | | reldmpsr 19858 |
. . . . . . . . . 10
⊢ Rel dom
mPwSer |
2 | | resspsr.u |
. . . . . . . . . 10
⊢ 𝑈 = (𝐼 mPwSer 𝐻) |
3 | | resspsr.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑈) |
4 | 1, 2, 3 | elbasov 16404 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝐻 ∈ V)) |
5 | 4 | ad2antrl 715 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼 ∈ V ∧ 𝐻 ∈ V)) |
6 | 5 | simpld 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐼 ∈ V) |
7 | | eqid 2778 |
. . . . . . . 8
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
8 | 7 | psrbaglefi 19869 |
. . . . . . 7
⊢ ((𝐼 ∈ V ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ∈
Fin) |
9 | 6, 8 | sylan 572 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ∈
Fin) |
10 | | resspsr.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) |
11 | | subrgsubg 19267 |
. . . . . . . . 9
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 ∈ (SubGrp‘𝑅)) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝑅)) |
13 | | subgsubm 18088 |
. . . . . . . 8
⊢ (𝑇 ∈ (SubGrp‘𝑅) → 𝑇 ∈ (SubMnd‘𝑅)) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (SubMnd‘𝑅)) |
15 | 14 | ad2antrr 713 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑇 ∈ (SubMnd‘𝑅)) |
16 | 10 | ad3antrrr 717 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑇 ∈ (SubRing‘𝑅)) |
17 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(Base‘𝐻) =
(Base‘𝐻) |
18 | | simprl 758 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
19 | 2, 17, 7, 3, 18 | psrelbas 19876 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
20 | 19 | adantr 473 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑋:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
21 | | elrabi 3590 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} → 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
22 | | ffvelrn 6676 |
. . . . . . . . . 10
⊢ ((𝑋:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)
∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑋‘𝑥) ∈ (Base‘𝐻)) |
23 | 20, 21, 22 | syl2an 586 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑋‘𝑥) ∈ (Base‘𝐻)) |
24 | | resspsr.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝑅 ↾s 𝑇) |
25 | 24 | subrgbas 19270 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 = (Base‘𝐻)) |
26 | 16, 25 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑇 = (Base‘𝐻)) |
27 | 23, 26 | eleqtrrd 2869 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑋‘𝑥) ∈ 𝑇) |
28 | | simprr 760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
29 | 2, 17, 7, 3, 28 | psrelbas 19876 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
30 | 29 | ad2antrr 713 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑌:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
31 | | ssrab2 3948 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ⊆ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
32 | 6 | ad2antrr 713 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝐼 ∈ V) |
33 | | simplr 756 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
34 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) |
35 | | eqid 2778 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} = {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} |
36 | 7, 35 | psrbagconcl 19870 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ V ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑘 ∘𝑓
− 𝑥) ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) |
37 | 32, 33, 34, 36 | syl3anc 1351 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑘 ∘𝑓
− 𝑥) ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) |
38 | 31, 37 | sseldi 3858 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑘 ∘𝑓
− 𝑥) ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
39 | 30, 38 | ffvelrnd 6679 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ (Base‘𝐻)) |
40 | 39, 26 | eleqtrrd 2869 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ 𝑇) |
41 | | eqid 2778 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
42 | 41 | subrgmcl 19273 |
. . . . . . . 8
⊢ ((𝑇 ∈ (SubRing‘𝑅) ∧ (𝑋‘𝑥) ∈ 𝑇 ∧ (𝑌‘(𝑘 ∘𝑓 − 𝑥)) ∈ 𝑇) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))) ∈ 𝑇) |
43 | 16, 27, 40, 42 | syl3anc 1351 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))) ∈ 𝑇) |
44 | 43 | fmpttd 6704 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))):{𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}⟶𝑇) |
45 | 9, 15, 44, 24 | gsumsubm 17844 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))) = (𝐻 Σg (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) |
46 | 24, 41 | ressmulr 16484 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) →
(.r‘𝑅) =
(.r‘𝐻)) |
47 | 10, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (.r‘𝑅) = (.r‘𝐻)) |
48 | 47 | ad3antrrr 717 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) →
(.r‘𝑅) =
(.r‘𝐻)) |
49 | 48 | oveqd 6995 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘}) → ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))) = ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))) |
50 | 49 | mpteq2dva 5023 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))) |
51 | 50 | oveq2d 6994 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐻 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))) = (𝐻 Σg (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) |
52 | 45, 51 | eqtrd 2814 |
. . . 4
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))) = (𝐻 Σg (𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) |
53 | 52 | mpteq2dva 5023 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥)))))) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝐻 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))))) |
54 | | resspsr.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
55 | | eqid 2778 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
56 | | eqid 2778 |
. . . 4
⊢
(.r‘𝑆) = (.r‘𝑆) |
57 | | fvex 6514 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
58 | 10, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 = (Base‘𝐻)) |
59 | | eqid 2778 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
60 | 59 | subrgss 19262 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 ⊆ (Base‘𝑅)) |
61 | 10, 60 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆ (Base‘𝑅)) |
62 | 58, 61 | eqsstr3d 3898 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐻) ⊆ (Base‘𝑅)) |
63 | | mapss 8253 |
. . . . . . . 8
⊢
(((Base‘𝑅)
∈ V ∧ (Base‘𝐻) ⊆ (Base‘𝑅)) → ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
64 | 57, 62, 63 | sylancr 578 |
. . . . . . 7
⊢ (𝜑 → ((Base‘𝐻) ↑𝑚
{𝑓 ∈
(ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
65 | 64 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
66 | 2, 17, 7, 3, 6 | psrbas 19875 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 = ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
67 | 54, 59, 7, 55, 6 | psrbas 19875 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (Base‘𝑆) = ((Base‘𝑅) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
68 | 65, 66, 67 | 3sstr4d 3906 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 ⊆ (Base‘𝑆)) |
69 | 68, 18 | sseldd 3861 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ (Base‘𝑆)) |
70 | 68, 28 | sseldd 3861 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ (Base‘𝑆)) |
71 | 54, 55, 41, 56, 7, 69, 70 | psrmulfval 19882 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑆)𝑌) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))))) |
72 | | eqid 2778 |
. . . 4
⊢
(.r‘𝐻) = (.r‘𝐻) |
73 | | eqid 2778 |
. . . 4
⊢
(.r‘𝑈) = (.r‘𝑈) |
74 | 2, 3, 72, 73, 7, 18, 28 | psrmulfval 19882 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ (𝐻 Σg
(𝑥 ∈ {𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝐻)(𝑌‘(𝑘 ∘𝑓 − 𝑥))))))) |
75 | 53, 71, 74 | 3eqtr4rd 2825 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑋(.r‘𝑆)𝑌)) |
76 | 3 | fvexi 6515 |
. . . 4
⊢ 𝐵 ∈ V |
77 | | resspsr.p |
. . . . 5
⊢ 𝑃 = (𝑆 ↾s 𝐵) |
78 | 77, 56 | ressmulr 16484 |
. . . 4
⊢ (𝐵 ∈ V →
(.r‘𝑆) =
(.r‘𝑃)) |
79 | 76, 78 | mp1i 13 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (.r‘𝑆) = (.r‘𝑃)) |
80 | 79 | oveqd 6995 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑆)𝑌) = (𝑋(.r‘𝑃)𝑌)) |
81 | 75, 80 | eqtrd 2814 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑋(.r‘𝑃)𝑌)) |