| Step | Hyp | Ref
| Expression |
| 1 | | resspsr.u |
. . 3
⊢ 𝑈 = (𝐼 mPwSer 𝐻) |
| 2 | | resspsr.b |
. . 3
⊢ 𝐵 = (Base‘𝑈) |
| 3 | | eqid 2737 |
. . 3
⊢
(+g‘𝐻) = (+g‘𝐻) |
| 4 | | eqid 2737 |
. . 3
⊢
(+g‘𝑈) = (+g‘𝑈) |
| 5 | | simprl 771 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
| 6 | | simprr 773 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
| 7 | 1, 2, 3, 4, 5, 6 | psradd 21957 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋 ∘f
(+g‘𝐻)𝑌)) |
| 8 | | resspsr.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
| 9 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 10 | | eqid 2737 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 11 | | eqid 2737 |
. . . 4
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 12 | | fvex 6919 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
| 13 | | resspsr.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) |
| 14 | | resspsr.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝑅 ↾s 𝑇) |
| 15 | 14 | subrgbas 20581 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 = (Base‘𝐻)) |
| 16 | 13, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 = (Base‘𝐻)) |
| 17 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 18 | 17 | subrgss 20572 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 ⊆ (Base‘𝑅)) |
| 19 | 13, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆ (Base‘𝑅)) |
| 20 | 16, 19 | eqsstrrd 4019 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐻) ⊆ (Base‘𝑅)) |
| 21 | | mapss 8929 |
. . . . . . . 8
⊢
(((Base‘𝑅)
∈ V ∧ (Base‘𝐻) ⊆ (Base‘𝑅)) → ((Base‘𝐻) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑m {𝑓
∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
| 22 | 12, 20, 21 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → ((Base‘𝐻) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑m {𝑓
∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
| 23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((Base‘𝐻) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑m {𝑓
∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
| 24 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝐻) =
(Base‘𝐻) |
| 25 | | eqid 2737 |
. . . . . . 7
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 26 | | reldmpsr 21934 |
. . . . . . . . . 10
⊢ Rel dom
mPwSer |
| 27 | 26, 1, 2 | elbasov 17254 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝐻 ∈ V)) |
| 28 | 27 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼 ∈ V ∧ 𝐻 ∈ V)) |
| 29 | 28 | simpld 494 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐼 ∈ V) |
| 30 | 1, 24, 25, 2, 29 | psrbas 21953 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 = ((Base‘𝐻) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin})) |
| 31 | 8, 17, 25, 9, 29 | psrbas 21953 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (Base‘𝑆) = ((Base‘𝑅) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin})) |
| 32 | 23, 30, 31 | 3sstr4d 4039 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 ⊆ (Base‘𝑆)) |
| 33 | 32, 5 | sseldd 3984 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ (Base‘𝑆)) |
| 34 | 32, 6 | sseldd 3984 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ (Base‘𝑆)) |
| 35 | 8, 9, 10, 11, 33, 34 | psradd 21957 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑆)𝑌) = (𝑋 ∘f
(+g‘𝑅)𝑌)) |
| 36 | 14, 10 | ressplusg 17334 |
. . . . . . 7
⊢ (𝑇 ∈ (SubRing‘𝑅) →
(+g‘𝑅) =
(+g‘𝐻)) |
| 37 | 13, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (+g‘𝑅) = (+g‘𝐻)) |
| 38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (+g‘𝑅) = (+g‘𝐻)) |
| 39 | 38 | ofeqd 7699 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ∘f
(+g‘𝑅) =
∘f (+g‘𝐻)) |
| 40 | 39 | oveqd 7448 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∘f
(+g‘𝑅)𝑌) = (𝑋 ∘f
(+g‘𝐻)𝑌)) |
| 41 | 35, 40 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑆)𝑌) = (𝑋 ∘f
(+g‘𝐻)𝑌)) |
| 42 | 2 | fvexi 6920 |
. . . 4
⊢ 𝐵 ∈ V |
| 43 | | resspsr.p |
. . . . 5
⊢ 𝑃 = (𝑆 ↾s 𝐵) |
| 44 | 43, 11 | ressplusg 17334 |
. . . 4
⊢ (𝐵 ∈ V →
(+g‘𝑆) =
(+g‘𝑃)) |
| 45 | 42, 44 | mp1i 13 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (+g‘𝑆) = (+g‘𝑃)) |
| 46 | 45 | oveqd 7448 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑆)𝑌) = (𝑋(+g‘𝑃)𝑌)) |
| 47 | 7, 41, 46 | 3eqtr2d 2783 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋(+g‘𝑃)𝑌)) |