Step | Hyp | Ref
| Expression |
1 | | psrvsca.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | psrvsca.k |
. . . . 5
⊢ 𝐾 = (Base‘𝑅) |
3 | | eqid 2610 |
. . . . 5
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | psrvsca.m |
. . . . 5
⊢ · =
(.r‘𝑅) |
5 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘𝑅) =
(TopOpen‘𝑅) |
6 | | psrvsca.d |
. . . . 5
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
7 | | psrvsca.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑆) |
8 | | simpl 472 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐼 ∈ V) |
9 | 1, 2, 6, 7, 8 | psrbas 19199 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = (𝐾 ↑𝑚 𝐷)) |
10 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝑆) = (+g‘𝑆) |
11 | 1, 7, 3, 10 | psrplusg 19202 |
. . . . 5
⊢
(+g‘𝑆) = ( ∘𝑓
(+g‘𝑅)
↾ (𝐵 × 𝐵)) |
12 | | eqid 2610 |
. . . . . 6
⊢
(.r‘𝑆) = (.r‘𝑆) |
13 | 1, 7, 4, 12, 6 | psrmulr 19205 |
. . . . 5
⊢
(.r‘𝑆) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) |
14 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) |
15 | | eqidd 2611 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) →
(∏t‘(𝐷 × {(TopOpen‘𝑅)})) = (∏t‘(𝐷 × {(TopOpen‘𝑅)}))) |
16 | | simpr 476 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑅 ∈ V) |
17 | 1, 2, 3, 4, 5, 6, 9, 11, 13, 14, 15, 8, 16 | psrval 19183 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑆 = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉})) |
18 | 17 | fveq2d 6107 |
. . 3
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (
·𝑠 ‘𝑆) = ( ·𝑠
‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}))) |
19 | | psrvsca.n |
. . 3
⊢ ∙ = (
·𝑠 ‘𝑆) |
20 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑅)
∈ V |
21 | 2, 20 | eqeltri 2684 |
. . . . 5
⊢ 𝐾 ∈ V |
22 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑆)
∈ V |
23 | 7, 22 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
24 | 21, 23 | mpt2ex 7136 |
. . . 4
⊢ (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) ∈ V |
25 | | psrvalstr 19184 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) Struct 〈1,
9〉 |
26 | | vscaid 15839 |
. . . . 5
⊢
·𝑠 = Slot (
·𝑠 ‘ndx) |
27 | | snsstp2 4288 |
. . . . . 6
⊢ {〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉} ⊆
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉} |
28 | | ssun2 3739 |
. . . . . 6
⊢
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) |
29 | 27, 28 | sstri 3577 |
. . . . 5
⊢ {〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) |
30 | 25, 26, 29 | strfv 15735 |
. . . 4
⊢ ((𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) ∈ V → (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) = (
·𝑠 ‘({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}))) |
31 | 24, 30 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) = (
·𝑠 ‘({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉})) |
32 | 18, 19, 31 | 3eqtr4g 2669 |
. 2
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
(𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))) |
33 | | eqid 2610 |
. . . . . 6
⊢ ∅ =
∅ |
34 | | fn0 5924 |
. . . . . 6
⊢ (∅
Fn ∅ ↔ ∅ = ∅) |
35 | 33, 34 | mpbir 220 |
. . . . 5
⊢ ∅
Fn ∅ |
36 | | reldmpsr 19182 |
. . . . . . . . . 10
⊢ Rel dom
mPwSer |
37 | 36 | ovprc 6581 |
. . . . . . . . 9
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPwSer 𝑅) = ∅) |
38 | 1, 37 | syl5eq 2656 |
. . . . . . . 8
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑆 = ∅) |
39 | 38 | fveq2d 6107 |
. . . . . . 7
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (
·𝑠 ‘𝑆) = ( ·𝑠
‘∅)) |
40 | | df-vsca 15785 |
. . . . . . . 8
⊢
·𝑠 = Slot 6 |
41 | 40 | str0 15739 |
. . . . . . 7
⊢ ∅ =
( ·𝑠 ‘∅) |
42 | 39, 19, 41 | 3eqtr4g 2669 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
∅) |
43 | 36, 1, 7 | elbasov 15749 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
44 | 43 | con3i 149 |
. . . . . . . . 9
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ¬ 𝑓 ∈ 𝐵) |
45 | 44 | eq0rdv 3931 |
. . . . . . . 8
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
46 | 45 | xpeq2d 5063 |
. . . . . . 7
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐾 × 𝐵) = (𝐾 × ∅)) |
47 | | xp0 5471 |
. . . . . . 7
⊢ (𝐾 × ∅) =
∅ |
48 | 46, 47 | syl6eq 2660 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐾 × 𝐵) = ∅) |
49 | 42, 48 | fneq12d 5897 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ( ∙ Fn
(𝐾 × 𝐵) ↔ ∅ Fn
∅)) |
50 | 35, 49 | mpbiri 247 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ Fn
(𝐾 × 𝐵)) |
51 | | fnov 6666 |
. . . 4
⊢ ( ∙ Fn
(𝐾 × 𝐵) ↔ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ (𝑥 ∙ 𝑓))) |
52 | 50, 51 | sylib 207 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
(𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ (𝑥 ∙ 𝑓))) |
53 | 44 | pm2.21d 117 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑓 ∈ 𝐵 → ((𝐷 × {𝑥}) ∘𝑓 · 𝑓) = (𝑥 ∙ 𝑓))) |
54 | 53 | a1d 25 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑥 ∈ 𝐾 → (𝑓 ∈ 𝐵 → ((𝐷 × {𝑥}) ∘𝑓 · 𝑓) = (𝑥 ∙ 𝑓)))) |
55 | 54 | 3imp 1249 |
. . . 4
⊢ ((¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑥 ∈ 𝐾 ∧ 𝑓 ∈ 𝐵) → ((𝐷 × {𝑥}) ∘𝑓 · 𝑓) = (𝑥 ∙ 𝑓)) |
56 | 55 | mpt2eq3dva 6617 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ (𝑥 ∙ 𝑓))) |
57 | 52, 56 | eqtr4d 2647 |
. 2
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
(𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))) |
58 | 32, 57 | pm2.61i 175 |
1
⊢ ∙ =
(𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) |