Step | Hyp | Ref
| Expression |
1 | | psrval.s |
. 2
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | df-psr 19863 |
. . . 4
⊢ mPwSer =
(𝑖 ∈ V, 𝑟 ∈ V ↦
⦋{ℎ ∈
(ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑
× {(TopOpen‘𝑟)}))〉})) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑
× {(TopOpen‘𝑟)}))〉}))) |
4 | | simprl 759 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝑖 = 𝐼) |
5 | 4 | oveq2d 6991 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → (ℕ0
↑𝑚 𝑖) = (ℕ0
↑𝑚 𝐼)) |
6 | | rabeq 3401 |
. . . . . . 7
⊢
((ℕ0 ↑𝑚 𝑖) = (ℕ0
↑𝑚 𝐼) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈
Fin}) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈
Fin}) |
8 | | psrval.d |
. . . . . 6
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
9 | 7, 8 | syl6eqr 2827 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = 𝐷) |
10 | 9 | csbeq1d 3788 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → ⦋{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑
× {(TopOpen‘𝑟)}))〉}) = ⦋𝐷 / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑
× {(TopOpen‘𝑟)}))〉})) |
11 | | ovex 7007 |
. . . . . . 7
⊢
(ℕ0 ↑𝑚 𝑖) ∈ V |
12 | 11 | rabex 5088 |
. . . . . 6
⊢ {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V |
13 | 9, 12 | syl6eqelr 2870 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝐷 ∈ V) |
14 | | simplrr 766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑟 = 𝑅) |
15 | 14 | fveq2d 6501 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = (Base‘𝑅)) |
16 | | psrval.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝑅) |
17 | 15, 16 | syl6eqr 2827 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = 𝐾) |
18 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
19 | 17, 18 | oveq12d 6993 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑𝑚 𝑑) = (𝐾 ↑𝑚 𝐷)) |
20 | | psrval.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = (𝐾 ↑𝑚 𝐷)) |
21 | 20 | ad2antrr 714 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 = (𝐾 ↑𝑚 𝐷)) |
22 | 19, 21 | eqtr4d 2812 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑𝑚 𝑑) = 𝐵) |
23 | 22 | csbeq1d 3788 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ⦋((Base‘𝑟) ↑𝑚
𝑑) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉}) = ⦋𝐵 / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉})) |
24 | | ovex 7007 |
. . . . . . . 8
⊢
((Base‘𝑟)
↑𝑚 𝑑) ∈ V |
25 | 22, 24 | syl6eqelr 2870 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 ∈ V) |
26 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
27 | 26 | opeq2d 4681 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐵〉) |
28 | 14 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑟 = 𝑅) |
29 | 28 | fveq2d 6501 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = (+g‘𝑅)) |
30 | | psrval.a |
. . . . . . . . . . . . . 14
⊢ + =
(+g‘𝑅) |
31 | 29, 30 | syl6eqr 2827 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = + ) |
32 | | ofeq 7228 |
. . . . . . . . . . . . 13
⊢
((+g‘𝑟) = + →
∘𝑓 (+g‘𝑟) = ∘𝑓 +
) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘𝑓
(+g‘𝑟) =
∘𝑓 + ) |
34 | 26, 26 | xpeq12d 5435 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
35 | 33, 34 | reseq12d 5694 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏)) = (
∘𝑓 + ↾ (𝐵 × 𝐵))) |
36 | | psrval.p |
. . . . . . . . . . 11
⊢ ✚ = (
∘𝑓 + ↾ (𝐵 × 𝐵)) |
37 | 35, 36 | syl6eqr 2827 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏)) = ✚ ) |
38 | 37 | opeq2d 4681 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 〈(+g‘ndx), (
∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))〉 = 〈(+g‘ndx),
✚
〉) |
39 | 18 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷) |
40 | | rabeq 3401 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝐷 → {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘}) |
42 | 28 | fveq2d 6501 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = (.r‘𝑅)) |
43 | | psrval.m |
. . . . . . . . . . . . . . . . 17
⊢ · =
(.r‘𝑅) |
44 | 42, 43 | syl6eqr 2827 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = · ) |
45 | 44 | oveqd 6992 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))) = ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))) |
46 | 41, 45 | mpteq12dv 5009 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))) |
47 | 28, 46 | oveq12d 6993 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))) |
48 | 39, 47 | mpteq12dv 5009 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) |
49 | 26, 26, 48 | mpoeq123dv 7046 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))) |
50 | | psrval.t |
. . . . . . . . . . 11
⊢ × =
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) |
51 | 49, 50 | syl6eqr 2827 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) = × ) |
52 | 51 | opeq2d 4681 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 〈(.r‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉 =
〈(.r‘ndx), ×
〉) |
53 | 27, 38, 52 | tpeq123d 4555 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} =
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
✚
〉, 〈(.r‘ndx), ×
〉}) |
54 | 28 | opeq2d 4681 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 〈(Scalar‘ndx), 𝑟〉 =
〈(Scalar‘ndx), 𝑅〉) |
55 | 17 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (Base‘𝑟) = 𝐾) |
56 | | ofeq 7228 |
. . . . . . . . . . . . . 14
⊢
((.r‘𝑟) = · →
∘𝑓 (.r‘𝑟) = ∘𝑓 ·
) |
57 | 44, 56 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘𝑓
(.r‘𝑟) =
∘𝑓 · ) |
58 | 39 | xpeq1d 5433 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {𝑥}) = (𝐷 × {𝑥})) |
59 | | eqidd 2774 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓) |
60 | 57, 58, 59 | oveq123d 6996 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓) = ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) |
61 | 55, 26, 60 | mpoeq123dv 7046 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓)) = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))) |
62 | | psrval.v |
. . . . . . . . . . 11
⊢ ∙ =
(𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) |
63 | 61, 62 | syl6eqr 2827 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓)) = ∙ ) |
64 | 63 | opeq2d 4681 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉 = 〈(
·𝑠 ‘ndx), ∙
〉) |
65 | 28 | fveq2d 6501 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = (TopOpen‘𝑅)) |
66 | | psrval.o |
. . . . . . . . . . . . . . 15
⊢ 𝑂 = (TopOpen‘𝑅) |
67 | 65, 66 | syl6eqr 2827 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = 𝑂) |
68 | 67 | sneqd 4448 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {(TopOpen‘𝑟)} = {𝑂}) |
69 | 39, 68 | xpeq12d 5435 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {(TopOpen‘𝑟)}) = (𝐷 × {𝑂})) |
70 | 69 | fveq2d 6501 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) =
(∏t‘(𝐷 × {𝑂}))) |
71 | | psrval.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 = (∏t‘(𝐷 × {𝑂}))) |
72 | 71 | ad3antrrr 718 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝐽 = (∏t‘(𝐷 × {𝑂}))) |
73 | 70, 72 | eqtr4d 2812 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) = 𝐽) |
74 | 73 | opeq2d 4681 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 〈(TopSet‘ndx),
(∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉 = 〈(TopSet‘ndx), 𝐽〉) |
75 | 54, 64, 74 | tpeq123d 4555 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉} = {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉}) |
76 | 53, 75 | uneq12d 4024 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ({〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉}) = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), ✚ 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉})) |
77 | 25, 76 | csbied 3810 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ⦋𝐵 / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉}) = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), ✚ 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉})) |
78 | 23, 77 | eqtrd 2809 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ⦋((Base‘𝑟) ↑𝑚
𝑑) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉}) = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), ✚ 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉})) |
79 | 13, 78 | csbied 3810 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → ⦋𝐷 / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑
× {(TopOpen‘𝑟)}))〉}) = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), ✚ 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉})) |
80 | 10, 79 | eqtrd 2809 |
. . 3
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → ⦋{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), ( ∘𝑓
(+g‘𝑟)
↾ (𝑏 × 𝑏))〉,
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑟〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓
(.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝑑
× {(TopOpen‘𝑟)}))〉}) = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), ✚ 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉})) |
81 | | psrval.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
82 | 81 | elexd 3430 |
. . 3
⊢ (𝜑 → 𝐼 ∈ V) |
83 | | psrval.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑋) |
84 | 83 | elexd 3430 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
85 | | tpex 7286 |
. . . . 5
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
✚
〉, 〈(.r‘ndx), × 〉} ∈
V |
86 | | tpex 7286 |
. . . . 5
⊢
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉} ∈ V |
87 | 85, 86 | unex 7285 |
. . . 4
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
✚
〉, 〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉}) ∈ V |
88 | 87 | a1i 11 |
. . 3
⊢ (𝜑 → ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), ✚ 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉}) ∈ V) |
89 | 3, 80, 82, 84, 88 | ovmpod 7117 |
. 2
⊢ (𝜑 → (𝐼 mPwSer 𝑅) = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), ✚ 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉})) |
90 | 1, 89 | syl5eq 2821 |
1
⊢ (𝜑 → 𝑆 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), ✚ 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), ∙ 〉,
〈(TopSet‘ndx), 𝐽〉})) |