| Step | Hyp | Ref
| Expression |
| 1 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) → 𝜑) |
| 2 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
| 3 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 4 | | eqid 2737 |
. . . . . . . . . . 11
⊢ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin} = {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈
Fin} |
| 5 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
| 6 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅))) |
| 7 | 2, 3, 4, 5, 6 | psrelbas 21954 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑎:{𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 8 | 7 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑎‘𝑑) ∈ (Base‘𝑅)) |
| 9 | | psrplusgpropd.b1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
| 10 | 1, 9 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) → 𝐵 = (Base‘𝑅)) |
| 11 | 8, 10 | eleqtrrd 2844 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑎‘𝑑) ∈ 𝐵) |
| 12 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) |
| 13 | 2, 3, 4, 5, 12 | psrelbas 21954 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑏:{𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 14 | 13 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑏‘𝑑) ∈ (Base‘𝑅)) |
| 15 | 14, 10 | eleqtrrd 2844 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑏‘𝑑) ∈ 𝐵) |
| 16 | | psrplusgpropd.p |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) |
| 17 | 16 | oveqrspc2v 7458 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎‘𝑑) ∈ 𝐵 ∧ (𝑏‘𝑑) ∈ 𝐵)) → ((𝑎‘𝑑)(+g‘𝑅)(𝑏‘𝑑)) = ((𝑎‘𝑑)(+g‘𝑆)(𝑏‘𝑑))) |
| 18 | 1, 11, 15, 17 | syl12anc 837 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) → ((𝑎‘𝑑)(+g‘𝑅)(𝑏‘𝑑)) = ((𝑎‘𝑑)(+g‘𝑆)(𝑏‘𝑑))) |
| 19 | 18 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → (𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin} ↦ ((𝑎‘𝑑)(+g‘𝑅)(𝑏‘𝑑))) = (𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin} ↦ ((𝑎‘𝑑)(+g‘𝑆)(𝑏‘𝑑)))) |
| 20 | 7 | ffnd 6737 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑎 Fn {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈
Fin}) |
| 21 | 13 | ffnd 6737 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑏 Fn {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈
Fin}) |
| 22 | | ovex 7464 |
. . . . . . . . 9
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 23 | 22 | rabex 5339 |
. . . . . . . 8
⊢ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin} ∈
V |
| 24 | 23 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin} ∈
V) |
| 25 | | inidm 4227 |
. . . . . . 7
⊢ ({𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin} ∩ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) = {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈
Fin} |
| 26 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑎‘𝑑) = (𝑎‘𝑑)) |
| 27 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑏‘𝑑) = (𝑏‘𝑑)) |
| 28 | 20, 21, 24, 24, 25, 26, 27 | offval 7706 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → (𝑎 ∘f
(+g‘𝑅)𝑏) = (𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin} ↦ ((𝑎‘𝑑)(+g‘𝑅)(𝑏‘𝑑)))) |
| 29 | 20, 21, 24, 24, 25, 26, 27 | offval 7706 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → (𝑎 ∘f
(+g‘𝑆)𝑏) = (𝑑 ∈ {𝑐 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑐 “ ℕ) ∈ Fin} ↦ ((𝑎‘𝑑)(+g‘𝑆)(𝑏‘𝑑)))) |
| 30 | 19, 28, 29 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → (𝑎 ∘f
(+g‘𝑅)𝑏) = (𝑎 ∘f
(+g‘𝑆)𝑏)) |
| 31 | 30 | mpoeq3dva 7510 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘f
(+g‘𝑅)𝑏)) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘f
(+g‘𝑆)𝑏))) |
| 32 | | psrplusgpropd.b2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝑆)) |
| 33 | 9, 32 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑆)) |
| 34 | 33 | psrbaspropd 22236 |
. . . . 5
⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆))) |
| 35 | | mpoeq12 7506 |
. . . . 5
⊢
(((Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑆)) ∧ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆))) → (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘f
(+g‘𝑆)𝑏)) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑆)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑆)) ↦ (𝑎 ∘f
(+g‘𝑆)𝑏))) |
| 36 | 34, 34, 35 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘f
(+g‘𝑆)𝑏)) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑆)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑆)) ↦ (𝑎 ∘f
(+g‘𝑆)𝑏))) |
| 37 | 31, 36 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘f
(+g‘𝑅)𝑏)) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑆)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑆)) ↦ (𝑎 ∘f
(+g‘𝑆)𝑏))) |
| 38 | | ofmres 8009 |
. . 3
⊢ (
∘f (+g‘𝑅) ↾ ((Base‘(𝐼 mPwSer 𝑅)) × (Base‘(𝐼 mPwSer 𝑅)))) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘f
(+g‘𝑅)𝑏)) |
| 39 | | ofmres 8009 |
. . 3
⊢ (
∘f (+g‘𝑆) ↾ ((Base‘(𝐼 mPwSer 𝑆)) × (Base‘(𝐼 mPwSer 𝑆)))) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑆)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑆)) ↦ (𝑎 ∘f
(+g‘𝑆)𝑏)) |
| 40 | 37, 38, 39 | 3eqtr4g 2802 |
. 2
⊢ (𝜑 → ( ∘f
(+g‘𝑅)
↾ ((Base‘(𝐼
mPwSer 𝑅)) ×
(Base‘(𝐼 mPwSer 𝑅)))) = ( ∘f
(+g‘𝑆)
↾ ((Base‘(𝐼
mPwSer 𝑆)) ×
(Base‘(𝐼 mPwSer 𝑆))))) |
| 41 | | eqid 2737 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 42 | | eqid 2737 |
. . 3
⊢
(+g‘(𝐼 mPwSer 𝑅)) = (+g‘(𝐼 mPwSer 𝑅)) |
| 43 | 2, 5, 41, 42 | psrplusg 21956 |
. 2
⊢
(+g‘(𝐼 mPwSer 𝑅)) = ( ∘f
(+g‘𝑅)
↾ ((Base‘(𝐼
mPwSer 𝑅)) ×
(Base‘(𝐼 mPwSer 𝑅)))) |
| 44 | | eqid 2737 |
. . 3
⊢ (𝐼 mPwSer 𝑆) = (𝐼 mPwSer 𝑆) |
| 45 | | eqid 2737 |
. . 3
⊢
(Base‘(𝐼
mPwSer 𝑆)) =
(Base‘(𝐼 mPwSer 𝑆)) |
| 46 | | eqid 2737 |
. . 3
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 47 | | eqid 2737 |
. . 3
⊢
(+g‘(𝐼 mPwSer 𝑆)) = (+g‘(𝐼 mPwSer 𝑆)) |
| 48 | 44, 45, 46, 47 | psrplusg 21956 |
. 2
⊢
(+g‘(𝐼 mPwSer 𝑆)) = ( ∘f
(+g‘𝑆)
↾ ((Base‘(𝐼
mPwSer 𝑆)) ×
(Base‘(𝐼 mPwSer 𝑆)))) |
| 49 | 40, 43, 48 | 3eqtr4g 2802 |
1
⊢ (𝜑 →
(+g‘(𝐼
mPwSer 𝑅)) =
(+g‘(𝐼
mPwSer 𝑆))) |