Step | Hyp | Ref
| Expression |
1 | | psrplusg.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | psrplusg.a |
. . . . 5
⊢ + =
(+g‘𝑅) |
4 | | eqid 2610 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
5 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘𝑅) =
(TopOpen‘𝑅) |
6 | | eqid 2610 |
. . . . 5
⊢ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
7 | | psrplusg.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑆) |
8 | | simpl 472 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐼 ∈ V) |
9 | 1, 2, 6, 7, 8 | psrbas 19199 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ((Base‘𝑅) ↑𝑚
{ℎ ∈
(ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈
Fin})) |
10 | | eqid 2610 |
. . . . 5
⊢ (
∘𝑓 + ↾ (𝐵 × 𝐵)) = ( ∘𝑓 + ↾
(𝐵 × 𝐵)) |
11 | | eqid 2610 |
. . . . 5
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) |
12 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ (({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑥}) ∘𝑓
(.r‘𝑅)𝑓)) = (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ (({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑥}) ∘𝑓
(.r‘𝑅)𝑓)) |
13 | | eqidd 2611 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) →
(∏t‘({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(TopOpen‘𝑅)})) =
(∏t‘({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(TopOpen‘𝑅)}))) |
14 | | simpr 476 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑅 ∈ V) |
15 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 13, 8, 14 | psrval 19183 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑆 = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), ( ∘𝑓 + ↾
(𝐵 × 𝐵))〉,
〈(.r‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ (({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑥}) ∘𝑓
(.r‘𝑅)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(TopOpen‘𝑅)}))〉})) |
16 | 15 | fveq2d 6107 |
. . 3
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) →
(+g‘𝑆) =
(+g‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
∘𝑓 + ↾ (𝐵 × 𝐵))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ (({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑥}) ∘𝑓
(.r‘𝑅)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(TopOpen‘𝑅)}))〉}))) |
17 | | psrplusg.p |
. . 3
⊢ ✚ =
(+g‘𝑆) |
18 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑆)
∈ V |
19 | 7, 18 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
20 | 19, 19 | xpex 6860 |
. . . 4
⊢ (𝐵 × 𝐵) ∈ V |
21 | | ofexg 6799 |
. . . 4
⊢ ((𝐵 × 𝐵) ∈ V → (
∘𝑓 + ↾ (𝐵 × 𝐵)) ∈ V) |
22 | | psrvalstr 19184 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
∘𝑓 + ↾ (𝐵 × 𝐵))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ (({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑥}) ∘𝑓
(.r‘𝑅)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(TopOpen‘𝑅)}))〉}) Struct 〈1,
9〉 |
23 | | plusgid 15804 |
. . . . 5
⊢
+g = Slot (+g‘ndx) |
24 | | snsstp2 4288 |
. . . . . 6
⊢
{〈(+g‘ndx), ( ∘𝑓 + ↾
(𝐵 × 𝐵))〉} ⊆
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
∘𝑓 + ↾ (𝐵 × 𝐵))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} |
25 | | ssun1 3738 |
. . . . . 6
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
∘𝑓 + ↾ (𝐵 × 𝐵))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
∘𝑓 + ↾ (𝐵 × 𝐵))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ (({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑥}) ∘𝑓
(.r‘𝑅)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(TopOpen‘𝑅)}))〉}) |
26 | 24, 25 | sstri 3577 |
. . . . 5
⊢
{〈(+g‘ndx), ( ∘𝑓 + ↾
(𝐵 × 𝐵))〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
∘𝑓 + ↾ (𝐵 × 𝐵))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ (({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑥}) ∘𝑓
(.r‘𝑅)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(TopOpen‘𝑅)}))〉}) |
27 | 22, 23, 26 | strfv 15735 |
. . . 4
⊢ ((
∘𝑓 + ↾ (𝐵 × 𝐵)) ∈ V → (
∘𝑓 + ↾ (𝐵 × 𝐵)) =
(+g‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
∘𝑓 + ↾ (𝐵 × 𝐵))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ (({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑥}) ∘𝑓
(.r‘𝑅)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(TopOpen‘𝑅)}))〉}))) |
28 | 20, 21, 27 | mp2b 10 |
. . 3
⊢ (
∘𝑓 + ↾ (𝐵 × 𝐵)) =
(+g‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), (
∘𝑓 + ↾ (𝐵 × 𝐵))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑥 ∈ {𝑦 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ 𝑦 ∘𝑟
≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑅)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ (({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑥}) ∘𝑓
(.r‘𝑅)𝑓))〉, 〈(TopSet‘ndx),
(∏t‘({ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(TopOpen‘𝑅)}))〉})) |
29 | 16, 17, 28 | 3eqtr4g 2669 |
. 2
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → ✚ = (
∘𝑓 + ↾ (𝐵 × 𝐵))) |
30 | | reldmpsr 19182 |
. . . . . . 7
⊢ Rel dom
mPwSer |
31 | 30 | ovprc 6581 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPwSer 𝑅) = ∅) |
32 | 1, 31 | syl5eq 2656 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑆 = ∅) |
33 | 32 | fveq2d 6107 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) →
(+g‘𝑆) =
(+g‘∅)) |
34 | 23 | str0 15739 |
. . . 4
⊢ ∅ =
(+g‘∅) |
35 | 33, 17, 34 | 3eqtr4g 2669 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ✚ =
∅) |
36 | 32 | fveq2d 6107 |
. . . . . . . 8
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) →
(Base‘𝑆) =
(Base‘∅)) |
37 | | base0 15740 |
. . . . . . . 8
⊢ ∅ =
(Base‘∅) |
38 | 36, 7, 37 | 3eqtr4g 2669 |
. . . . . . 7
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
39 | 38 | xpeq2d 5063 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐵 × 𝐵) = (𝐵 × ∅)) |
40 | | xp0 5471 |
. . . . . 6
⊢ (𝐵 × ∅) =
∅ |
41 | 39, 40 | syl6eq 2660 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐵 × 𝐵) = ∅) |
42 | 41 | reseq2d 5317 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (
∘𝑓 + ↾ (𝐵 × 𝐵)) = ( ∘𝑓 + ↾
∅)) |
43 | | res0 5321 |
. . . 4
⊢ (
∘𝑓 + ↾ ∅) =
∅ |
44 | 42, 43 | syl6eq 2660 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (
∘𝑓 + ↾ (𝐵 × 𝐵)) = ∅) |
45 | 35, 44 | eqtr4d 2647 |
. 2
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ✚ = (
∘𝑓 + ↾ (𝐵 × 𝐵))) |
46 | 29, 45 | pm2.61i 175 |
1
⊢ ✚ = (
∘𝑓 + ↾ (𝐵 × 𝐵)) |