| Step | Hyp | Ref
| Expression |
| 1 | | psrvsca.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
| 2 | | psrvsca.k |
. . . . 5
⊢ 𝐾 = (Base‘𝑅) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 4 | | psrvsca.m |
. . . . 5
⊢ · =
(.r‘𝑅) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(TopOpen‘𝑅) =
(TopOpen‘𝑅) |
| 6 | | psrvsca.d |
. . . . 5
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
| 7 | | psrvsca.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑆) |
| 8 | | simpl 482 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐼 ∈ V) |
| 9 | 1, 2, 6, 7, 8 | psrbas 21953 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = (𝐾 ↑m 𝐷)) |
| 10 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 11 | 1, 7, 3, 10 | psrplusg 21956 |
. . . . 5
⊢
(+g‘𝑆) = ( ∘f
(+g‘𝑅)
↾ (𝐵 × 𝐵)) |
| 12 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝑆) = (.r‘𝑆) |
| 13 | 1, 7, 4, 12, 6 | psrmulr 21962 |
. . . . 5
⊢
(.r‘𝑆) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))))) |
| 14 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) |
| 15 | | eqidd 2738 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) →
(∏t‘(𝐷 × {(TopOpen‘𝑅)})) = (∏t‘(𝐷 × {(TopOpen‘𝑅)}))) |
| 16 | | simpr 484 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑅 ∈ V) |
| 17 | 1, 2, 3, 4, 5, 6, 9, 11, 13, 14, 15, 8, 16 | psrval 21935 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑆 = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉})) |
| 18 | 17 | fveq2d 6910 |
. . 3
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (
·𝑠 ‘𝑆) = ( ·𝑠
‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}))) |
| 19 | | psrvsca.n |
. . 3
⊢ ∙ = (
·𝑠 ‘𝑆) |
| 20 | 2 | fvexi 6920 |
. . . . 5
⊢ 𝐾 ∈ V |
| 21 | 7 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 22 | 20, 21 | mpoex 8104 |
. . . 4
⊢ (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) ∈ V |
| 23 | | psrvalstr 21936 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) Struct 〈1,
9〉 |
| 24 | | vscaid 17364 |
. . . . 5
⊢
·𝑠 = Slot (
·𝑠 ‘ndx) |
| 25 | | snsstp2 4817 |
. . . . . 6
⊢ {〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉} ⊆ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉} |
| 26 | | ssun2 4179 |
. . . . . 6
⊢
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) |
| 27 | 25, 26 | sstri 3993 |
. . . . 5
⊢ {〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉} ⊆ ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) |
| 28 | 23, 24, 27 | strfv 17240 |
. . . 4
⊢ ((𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) ∈ V → (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) = ( ·𝑠
‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}))) |
| 29 | 22, 28 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) = ( ·𝑠
‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(.r‘𝑆)〉} ∪ {〈(Scalar‘ndx),
𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))〉, 〈(TopSet‘ndx),
(∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉})) |
| 30 | 18, 19, 29 | 3eqtr4g 2802 |
. 2
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
(𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))) |
| 31 | | eqid 2737 |
. . . . . 6
⊢ ∅ =
∅ |
| 32 | | fn0 6699 |
. . . . . 6
⊢ (∅
Fn ∅ ↔ ∅ = ∅) |
| 33 | 31, 32 | mpbir 231 |
. . . . 5
⊢ ∅
Fn ∅ |
| 34 | | reldmpsr 21934 |
. . . . . . . . . 10
⊢ Rel dom
mPwSer |
| 35 | 34 | ovprc 7469 |
. . . . . . . . 9
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPwSer 𝑅) = ∅) |
| 36 | 1, 35 | eqtrid 2789 |
. . . . . . . 8
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑆 = ∅) |
| 37 | 36 | fveq2d 6910 |
. . . . . . 7
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (
·𝑠 ‘𝑆) = ( ·𝑠
‘∅)) |
| 38 | 24 | str0 17226 |
. . . . . . 7
⊢ ∅ =
( ·𝑠 ‘∅) |
| 39 | 37, 19, 38 | 3eqtr4g 2802 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
∅) |
| 40 | 34, 1, 7 | elbasov 17254 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐵 → (𝐼 ∈ V ∧ 𝑅 ∈ V)) |
| 41 | 40 | con3i 154 |
. . . . . . . . 9
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ¬ 𝑓 ∈ 𝐵) |
| 42 | 41 | eq0rdv 4407 |
. . . . . . . 8
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
| 43 | 42 | xpeq2d 5715 |
. . . . . . 7
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐾 × 𝐵) = (𝐾 × ∅)) |
| 44 | | xp0 6178 |
. . . . . . 7
⊢ (𝐾 × ∅) =
∅ |
| 45 | 43, 44 | eqtrdi 2793 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐾 × 𝐵) = ∅) |
| 46 | 39, 45 | fneq12d 6663 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ( ∙ Fn
(𝐾 × 𝐵) ↔ ∅ Fn
∅)) |
| 47 | 33, 46 | mpbiri 258 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ Fn
(𝐾 × 𝐵)) |
| 48 | | fnov 7564 |
. . . 4
⊢ ( ∙ Fn
(𝐾 × 𝐵) ↔ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ (𝑥 ∙ 𝑓))) |
| 49 | 47, 48 | sylib 218 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
(𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ (𝑥 ∙ 𝑓))) |
| 50 | 41 | pm2.21d 121 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑓 ∈ 𝐵 → ((𝐷 × {𝑥}) ∘f · 𝑓) = (𝑥 ∙ 𝑓))) |
| 51 | 50 | a1d 25 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑥 ∈ 𝐾 → (𝑓 ∈ 𝐵 → ((𝐷 × {𝑥}) ∘f · 𝑓) = (𝑥 ∙ 𝑓)))) |
| 52 | 51 | 3imp 1111 |
. . . 4
⊢ ((¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) ∧ 𝑥 ∈ 𝐾 ∧ 𝑓 ∈ 𝐵) → ((𝐷 × {𝑥}) ∘f · 𝑓) = (𝑥 ∙ 𝑓)) |
| 53 | 52 | mpoeq3dva 7510 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ (𝑥 ∙ 𝑓))) |
| 54 | 49, 53 | eqtr4d 2780 |
. 2
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
(𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))) |
| 55 | 30, 54 | pm2.61i 182 |
1
⊢ ∙ =
(𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) |