Step | Hyp | Ref
| Expression |
1 | | resspsr.u |
. . 3
⊢ 𝑈 = (𝐼 mPwSer 𝐻) |
2 | | resspsr.b |
. . 3
⊢ 𝐵 = (Base‘𝑈) |
3 | | eqid 2773 |
. . 3
⊢
(+g‘𝐻) = (+g‘𝐻) |
4 | | eqid 2773 |
. . 3
⊢
(+g‘𝑈) = (+g‘𝑈) |
5 | | simprl 759 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
6 | | simprr 761 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
7 | 1, 2, 3, 4, 5, 6 | psradd 19889 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋 ∘𝑓
(+g‘𝐻)𝑌)) |
8 | | resspsr.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
9 | | eqid 2773 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
10 | | eqid 2773 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
11 | | eqid 2773 |
. . . 4
⊢
(+g‘𝑆) = (+g‘𝑆) |
12 | | fvex 6510 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
13 | | resspsr.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) |
14 | | resspsr.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝑅 ↾s 𝑇) |
15 | 14 | subrgbas 19280 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 = (Base‘𝐻)) |
16 | 13, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 = (Base‘𝐻)) |
17 | | eqid 2773 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
18 | 17 | subrgss 19272 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 ⊆ (Base‘𝑅)) |
19 | 13, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆ (Base‘𝑅)) |
20 | 16, 19 | eqsstr3d 3891 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐻) ⊆ (Base‘𝑅)) |
21 | | mapss 8250 |
. . . . . . . 8
⊢
(((Base‘𝑅)
∈ V ∧ (Base‘𝐻) ⊆ (Base‘𝑅)) → ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
22 | 12, 20, 21 | sylancr 579 |
. . . . . . 7
⊢ (𝜑 → ((Base‘𝐻) ↑𝑚
{𝑓 ∈
(ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
23 | 22 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ⊆
((Base‘𝑅)
↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
24 | | eqid 2773 |
. . . . . . 7
⊢
(Base‘𝐻) =
(Base‘𝐻) |
25 | | eqid 2773 |
. . . . . . 7
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
26 | | reldmpsr 19868 |
. . . . . . . . . 10
⊢ Rel dom
mPwSer |
27 | 26, 1, 2 | elbasov 16400 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝐻 ∈ V)) |
28 | 27 | ad2antrl 716 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼 ∈ V ∧ 𝐻 ∈ V)) |
29 | 28 | simpld 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐼 ∈ V) |
30 | 1, 24, 25, 2, 29 | psrbas 19885 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 = ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
31 | 8, 17, 25, 9, 29 | psrbas 19885 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (Base‘𝑆) = ((Base‘𝑅) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
32 | 23, 30, 31 | 3sstr4d 3899 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 ⊆ (Base‘𝑆)) |
33 | 32, 5 | sseldd 3854 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ (Base‘𝑆)) |
34 | 32, 6 | sseldd 3854 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ (Base‘𝑆)) |
35 | 8, 9, 10, 11, 33, 34 | psradd 19889 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑆)𝑌) = (𝑋 ∘𝑓
(+g‘𝑅)𝑌)) |
36 | 14, 10 | ressplusg 16467 |
. . . . . . 7
⊢ (𝑇 ∈ (SubRing‘𝑅) →
(+g‘𝑅) =
(+g‘𝐻)) |
37 | 13, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (+g‘𝑅) = (+g‘𝐻)) |
38 | 37 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (+g‘𝑅) = (+g‘𝐻)) |
39 | | ofeq 7228 |
. . . . 5
⊢
((+g‘𝑅) = (+g‘𝐻) → ∘𝑓
(+g‘𝑅) =
∘𝑓 (+g‘𝐻)) |
40 | 38, 39 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ∘𝑓
(+g‘𝑅) =
∘𝑓 (+g‘𝐻)) |
41 | 40 | oveqd 6992 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∘𝑓
(+g‘𝑅)𝑌) = (𝑋 ∘𝑓
(+g‘𝐻)𝑌)) |
42 | 35, 41 | eqtrd 2809 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑆)𝑌) = (𝑋 ∘𝑓
(+g‘𝐻)𝑌)) |
43 | 2 | fvexi 6511 |
. . . 4
⊢ 𝐵 ∈ V |
44 | | resspsr.p |
. . . . 5
⊢ 𝑃 = (𝑆 ↾s 𝐵) |
45 | 44, 11 | ressplusg 16467 |
. . . 4
⊢ (𝐵 ∈ V →
(+g‘𝑆) =
(+g‘𝑃)) |
46 | 43, 45 | mp1i 13 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (+g‘𝑆) = (+g‘𝑃)) |
47 | 46 | oveqd 6992 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑆)𝑌) = (𝑋(+g‘𝑃)𝑌)) |
48 | 7, 42, 47 | 3eqtr2d 2815 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋(+g‘𝑃)𝑌)) |