Proof of Theorem psrmulr
Step | Hyp | Ref
| Expression |
1 | | psrmulr.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | eqid 2610 |
. . . . 5
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | psrmulr.m |
. . . . 5
⊢ · =
(.r‘𝑅) |
5 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘𝑅) =
(TopOpen‘𝑅) |
6 | | psrmulr.d |
. . . . 5
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
7 | | psrmulr.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑆) |
8 | | simpl 472 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐼 ∈ V) |
9 | 1, 2, 6, 7, 8 | psrbas 19199 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ((Base‘𝑅) ↑𝑚
𝐷)) |
10 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝑆) = (+g‘𝑆) |
11 | 1, 7, 3, 10 | psrplusg 19202 |
. . . . 5
⊢
(+g‘𝑆) = ( ∘𝑓
(+g‘𝑅)
↾ (𝐵 × 𝐵)) |
12 | | eqid 2610 |
. . . . 5
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) |
13 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) = (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) |
14 | | eqidd 2611 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) →
(∏t‘(𝐷 × {(TopOpen‘𝑅)})) = (∏t‘(𝐷 × {(TopOpen‘𝑅)}))) |
15 | | simpr 476 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑅 ∈ V) |
16 | 1, 2, 3, 4, 5, 6, 9, 11, 12, 13, 14, 8, 15 | psrval 19183 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑆 = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑆)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉})) |
17 | 16 | fveq2d 6107 |
. . 3
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) →
(.r‘𝑆) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}))) |
18 | | psrmulr.t |
. . 3
⊢ ∙ =
(.r‘𝑆) |
19 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑆)
∈ V |
20 | 7, 19 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
21 | 20, 20 | mpt2ex 7136 |
. . . 4
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) ∈
V |
22 | | psrvalstr 19184 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) Struct 〈1,
9〉 |
23 | | mulrid 15822 |
. . . . 5
⊢
.r = Slot (.r‘ndx) |
24 | | snsstp3 4289 |
. . . . . 6
⊢
{〈(.r‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ⊆
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} |
25 | | ssun1 3738 |
. . . . . 6
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) |
26 | 24, 25 | sstri 3577 |
. . . . 5
⊢
{〈(.r‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}) |
27 | 22, 23, 26 | strfv 15735 |
. . . 4
⊢ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) ∈ V → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉}))) |
28 | 21, 27 | ax-mp 5 |
. . 3
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑆)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪
{〈(Scalar‘ndx), 𝑅〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))〉,
〈(TopSet‘ndx), (∏t‘(𝐷 × {(TopOpen‘𝑅)}))〉})) |
29 | 17, 18, 28 | 3eqtr4g 2669 |
. 2
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))) |
30 | | mpt20 6623 |
. . . 4
⊢ (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) =
∅ |
31 | 23 | str0 15739 |
. . . 4
⊢ ∅ =
(.r‘∅) |
32 | 30, 31 | eqtr2i 2633 |
. . 3
⊢
(.r‘∅) = (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) |
33 | | reldmpsr 19182 |
. . . . . . 7
⊢ Rel dom
mPwSer |
34 | 33 | ovprc 6581 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPwSer 𝑅) = ∅) |
35 | 1, 34 | syl5eq 2656 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑆 = ∅) |
36 | 35 | fveq2d 6107 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) →
(.r‘𝑆) =
(.r‘∅)) |
37 | 18, 36 | syl5eq 2656 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
(.r‘∅)) |
38 | 35 | fveq2d 6107 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) →
(Base‘𝑆) =
(Base‘∅)) |
39 | | base0 15740 |
. . . . 5
⊢ ∅ =
(Base‘∅) |
40 | 38, 7, 39 | 3eqtr4g 2669 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
41 | | mpt2eq12 6613 |
. . . 4
⊢ ((𝐵 = ∅ ∧ 𝐵 = ∅) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) = (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))) |
42 | 40, 40, 41 | syl2anc 691 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) = (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))) |
43 | 32, 37, 42 | 3eqtr4a 2670 |
. 2
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → ∙ =
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))) |
44 | 29, 43 | pm2.61i 175 |
1
⊢ ∙ =
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) |