Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) → 𝜑) |
2 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
3 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
4 | | eqid 2610 |
. . . . . . . . . . 11
⊢ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin} = {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin} |
5 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
6 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅))) |
7 | 2, 3, 4, 5, 6 | psrelbas 19200 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑎:{𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
8 | 7 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑎‘𝑑) ∈ (Base‘𝑅)) |
9 | | psrplusgpropd.b1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
10 | 1, 9 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) → 𝐵 = (Base‘𝑅)) |
11 | 8, 10 | eleqtrrd 2691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑎‘𝑑) ∈ 𝐵) |
12 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) |
13 | 2, 3, 4, 5, 12 | psrelbas 19200 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑏:{𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
14 | 13 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑏‘𝑑) ∈ (Base‘𝑅)) |
15 | 14, 10 | eleqtrrd 2691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑏‘𝑑) ∈ 𝐵) |
16 | | psrplusgpropd.p |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) |
17 | 16 | oveqrspc2v 6572 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎‘𝑑) ∈ 𝐵 ∧ (𝑏‘𝑑) ∈ 𝐵)) → ((𝑎‘𝑑)(+g‘𝑅)(𝑏‘𝑑)) = ((𝑎‘𝑑)(+g‘𝑆)(𝑏‘𝑑))) |
18 | 1, 11, 15, 17 | syl12anc 1316 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) → ((𝑎‘𝑑)(+g‘𝑅)(𝑏‘𝑑)) = ((𝑎‘𝑑)(+g‘𝑆)(𝑏‘𝑑))) |
19 | 18 | mpteq2dva 4672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → (𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin} ↦ ((𝑎‘𝑑)(+g‘𝑅)(𝑏‘𝑑))) = (𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin} ↦ ((𝑎‘𝑑)(+g‘𝑆)(𝑏‘𝑑)))) |
20 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑎:{𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin}⟶(Base‘𝑅)
→ 𝑎 Fn {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin}) |
21 | 7, 20 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑎 Fn {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin}) |
22 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑏:{𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin}⟶(Base‘𝑅)
→ 𝑏 Fn {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin}) |
23 | 13, 22 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → 𝑏 Fn {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin}) |
24 | | ovex 6577 |
. . . . . . . . 9
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
25 | 24 | rabex 4740 |
. . . . . . . 8
⊢ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin} ∈
V |
26 | 25 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin} ∈
V) |
27 | | inidm 3784 |
. . . . . . 7
⊢ ({𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin} ∩ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) = {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈
Fin} |
28 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑎‘𝑑) = (𝑎‘𝑑)) |
29 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) ∧ 𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin}) → (𝑏‘𝑑) = (𝑏‘𝑑)) |
30 | 21, 23, 26, 26, 27, 28, 29 | offval 6802 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → (𝑎 ∘𝑓
(+g‘𝑅)𝑏) = (𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin} ↦ ((𝑎‘𝑑)(+g‘𝑅)(𝑏‘𝑑)))) |
31 | 21, 23, 26, 26, 27, 28, 29 | offval 6802 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → (𝑎 ∘𝑓
(+g‘𝑆)𝑏) = (𝑑 ∈ {𝑐 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑐 “ ℕ) ∈ Fin} ↦ ((𝑎‘𝑑)(+g‘𝑆)(𝑏‘𝑑)))) |
32 | 19, 30, 31 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅))) → (𝑎 ∘𝑓
(+g‘𝑅)𝑏) = (𝑎 ∘𝑓
(+g‘𝑆)𝑏)) |
33 | 32 | mpt2eq3dva 6617 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘𝑓
(+g‘𝑅)𝑏)) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘𝑓
(+g‘𝑆)𝑏))) |
34 | | psrplusgpropd.b2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝑆)) |
35 | 9, 34 | eqtr3d 2646 |
. . . . . 6
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑆)) |
36 | 35 | psrbaspropd 19426 |
. . . . 5
⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆))) |
37 | | mpt2eq12 6613 |
. . . . 5
⊢
(((Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑆)) ∧ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆))) → (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘𝑓
(+g‘𝑆)𝑏)) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑆)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑆)) ↦ (𝑎 ∘𝑓
(+g‘𝑆)𝑏))) |
38 | 36, 36, 37 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘𝑓
(+g‘𝑆)𝑏)) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑆)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑆)) ↦ (𝑎 ∘𝑓
(+g‘𝑆)𝑏))) |
39 | 33, 38 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘𝑓
(+g‘𝑅)𝑏)) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑆)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑆)) ↦ (𝑎 ∘𝑓
(+g‘𝑆)𝑏))) |
40 | | ofmres 7055 |
. . 3
⊢ (
∘𝑓 (+g‘𝑅) ↾ ((Base‘(𝐼 mPwSer 𝑅)) × (Base‘(𝐼 mPwSer 𝑅)))) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑅)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑅)) ↦ (𝑎 ∘𝑓
(+g‘𝑅)𝑏)) |
41 | | ofmres 7055 |
. . 3
⊢ (
∘𝑓 (+g‘𝑆) ↾ ((Base‘(𝐼 mPwSer 𝑆)) × (Base‘(𝐼 mPwSer 𝑆)))) = (𝑎 ∈ (Base‘(𝐼 mPwSer 𝑆)), 𝑏 ∈ (Base‘(𝐼 mPwSer 𝑆)) ↦ (𝑎 ∘𝑓
(+g‘𝑆)𝑏)) |
42 | 39, 40, 41 | 3eqtr4g 2669 |
. 2
⊢ (𝜑 → (
∘𝑓 (+g‘𝑅) ↾ ((Base‘(𝐼 mPwSer 𝑅)) × (Base‘(𝐼 mPwSer 𝑅)))) = ( ∘𝑓
(+g‘𝑆)
↾ ((Base‘(𝐼
mPwSer 𝑆)) ×
(Base‘(𝐼 mPwSer 𝑆))))) |
43 | | eqid 2610 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
44 | | eqid 2610 |
. . 3
⊢
(+g‘(𝐼 mPwSer 𝑅)) = (+g‘(𝐼 mPwSer 𝑅)) |
45 | 2, 5, 43, 44 | psrplusg 19202 |
. 2
⊢
(+g‘(𝐼 mPwSer 𝑅)) = ( ∘𝑓
(+g‘𝑅)
↾ ((Base‘(𝐼
mPwSer 𝑅)) ×
(Base‘(𝐼 mPwSer 𝑅)))) |
46 | | eqid 2610 |
. . 3
⊢ (𝐼 mPwSer 𝑆) = (𝐼 mPwSer 𝑆) |
47 | | eqid 2610 |
. . 3
⊢
(Base‘(𝐼
mPwSer 𝑆)) =
(Base‘(𝐼 mPwSer 𝑆)) |
48 | | eqid 2610 |
. . 3
⊢
(+g‘𝑆) = (+g‘𝑆) |
49 | | eqid 2610 |
. . 3
⊢
(+g‘(𝐼 mPwSer 𝑆)) = (+g‘(𝐼 mPwSer 𝑆)) |
50 | 46, 47, 48, 49 | psrplusg 19202 |
. 2
⊢
(+g‘(𝐼 mPwSer 𝑆)) = ( ∘𝑓
(+g‘𝑆)
↾ ((Base‘(𝐼
mPwSer 𝑆)) ×
(Base‘(𝐼 mPwSer 𝑆)))) |
51 | 42, 45, 50 | 3eqtr4g 2669 |
1
⊢ (𝜑 →
(+g‘(𝐼
mPwSer 𝑅)) =
(+g‘(𝐼
mPwSer 𝑆))) |