Proof of Theorem tmsxpsval
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
((toMetSp‘𝑀)
×s (toMetSp‘𝑁)) = ((toMetSp‘𝑀) ×s
(toMetSp‘𝑁)) |
| 2 | | eqid 2737 |
. . 3
⊢
(Base‘(toMetSp‘𝑀)) = (Base‘(toMetSp‘𝑀)) |
| 3 | | eqid 2737 |
. . 3
⊢
(Base‘(toMetSp‘𝑁)) = (Base‘(toMetSp‘𝑁)) |
| 4 | | tmsxps.1 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(toMetSp‘𝑀) =
(toMetSp‘𝑀) |
| 6 | 5 | tmsxms 24499 |
. . . 4
⊢ (𝑀 ∈ (∞Met‘𝑋) → (toMetSp‘𝑀) ∈
∞MetSp) |
| 7 | 4, 6 | syl 17 |
. . 3
⊢ (𝜑 → (toMetSp‘𝑀) ∈
∞MetSp) |
| 8 | | tmsxps.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) |
| 9 | | eqid 2737 |
. . . . 5
⊢
(toMetSp‘𝑁) =
(toMetSp‘𝑁) |
| 10 | 9 | tmsxms 24499 |
. . . 4
⊢ (𝑁 ∈ (∞Met‘𝑌) → (toMetSp‘𝑁) ∈
∞MetSp) |
| 11 | 8, 10 | syl 17 |
. . 3
⊢ (𝜑 → (toMetSp‘𝑁) ∈
∞MetSp) |
| 12 | | tmsxps.p |
. . 3
⊢ 𝑃 =
(dist‘((toMetSp‘𝑀) ×s
(toMetSp‘𝑁))) |
| 13 | | eqid 2737 |
. . 3
⊢
((dist‘(toMetSp‘𝑀)) ↾ ((Base‘(toMetSp‘𝑀)) ×
(Base‘(toMetSp‘𝑀)))) = ((dist‘(toMetSp‘𝑀)) ↾
((Base‘(toMetSp‘𝑀)) × (Base‘(toMetSp‘𝑀)))) |
| 14 | | eqid 2737 |
. . 3
⊢
((dist‘(toMetSp‘𝑁)) ↾ ((Base‘(toMetSp‘𝑁)) ×
(Base‘(toMetSp‘𝑁)))) = ((dist‘(toMetSp‘𝑁)) ↾
((Base‘(toMetSp‘𝑁)) × (Base‘(toMetSp‘𝑁)))) |
| 15 | 5 | tmsds 24497 |
. . . . . 6
⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝑀 = (dist‘(toMetSp‘𝑀))) |
| 16 | 4, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑀 = (dist‘(toMetSp‘𝑀))) |
| 17 | 5 | tmsbas 24496 |
. . . . . . 7
⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝑋 = (Base‘(toMetSp‘𝑀))) |
| 18 | 4, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 = (Base‘(toMetSp‘𝑀))) |
| 19 | 18 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (∞Met‘𝑋) =
(∞Met‘(Base‘(toMetSp‘𝑀)))) |
| 20 | 4, 16, 19 | 3eltr3d 2855 |
. . . 4
⊢ (𝜑 →
(dist‘(toMetSp‘𝑀)) ∈
(∞Met‘(Base‘(toMetSp‘𝑀)))) |
| 21 | | ssid 4006 |
. . . 4
⊢
(Base‘(toMetSp‘𝑀)) ⊆ (Base‘(toMetSp‘𝑀)) |
| 22 | | xmetres2 24371 |
. . . 4
⊢
(((dist‘(toMetSp‘𝑀)) ∈
(∞Met‘(Base‘(toMetSp‘𝑀))) ∧ (Base‘(toMetSp‘𝑀)) ⊆
(Base‘(toMetSp‘𝑀))) → ((dist‘(toMetSp‘𝑀)) ↾
((Base‘(toMetSp‘𝑀)) × (Base‘(toMetSp‘𝑀)))) ∈
(∞Met‘(Base‘(toMetSp‘𝑀)))) |
| 23 | 20, 21, 22 | sylancl 586 |
. . 3
⊢ (𝜑 →
((dist‘(toMetSp‘𝑀)) ↾ ((Base‘(toMetSp‘𝑀)) ×
(Base‘(toMetSp‘𝑀)))) ∈
(∞Met‘(Base‘(toMetSp‘𝑀)))) |
| 24 | 9 | tmsds 24497 |
. . . . . 6
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝑁 = (dist‘(toMetSp‘𝑁))) |
| 25 | 8, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 = (dist‘(toMetSp‘𝑁))) |
| 26 | 9 | tmsbas 24496 |
. . . . . . 7
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝑌 = (Base‘(toMetSp‘𝑁))) |
| 27 | 8, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑌 = (Base‘(toMetSp‘𝑁))) |
| 28 | 27 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (∞Met‘𝑌) =
(∞Met‘(Base‘(toMetSp‘𝑁)))) |
| 29 | 8, 25, 28 | 3eltr3d 2855 |
. . . 4
⊢ (𝜑 →
(dist‘(toMetSp‘𝑁)) ∈
(∞Met‘(Base‘(toMetSp‘𝑁)))) |
| 30 | | ssid 4006 |
. . . 4
⊢
(Base‘(toMetSp‘𝑁)) ⊆ (Base‘(toMetSp‘𝑁)) |
| 31 | | xmetres2 24371 |
. . . 4
⊢
(((dist‘(toMetSp‘𝑁)) ∈
(∞Met‘(Base‘(toMetSp‘𝑁))) ∧ (Base‘(toMetSp‘𝑁)) ⊆
(Base‘(toMetSp‘𝑁))) → ((dist‘(toMetSp‘𝑁)) ↾
((Base‘(toMetSp‘𝑁)) × (Base‘(toMetSp‘𝑁)))) ∈
(∞Met‘(Base‘(toMetSp‘𝑁)))) |
| 32 | 29, 30, 31 | sylancl 586 |
. . 3
⊢ (𝜑 →
((dist‘(toMetSp‘𝑁)) ↾ ((Base‘(toMetSp‘𝑁)) ×
(Base‘(toMetSp‘𝑁)))) ∈
(∞Met‘(Base‘(toMetSp‘𝑁)))) |
| 33 | | tmsxpsval.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
| 34 | 33, 18 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝐴 ∈ (Base‘(toMetSp‘𝑀))) |
| 35 | | tmsxpsval.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
| 36 | 35, 27 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝐵 ∈ (Base‘(toMetSp‘𝑁))) |
| 37 | | tmsxpsval.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
| 38 | 37, 18 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (Base‘(toMetSp‘𝑀))) |
| 39 | | tmsxpsval.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
| 40 | 39, 27 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (Base‘(toMetSp‘𝑁))) |
| 41 | 1, 2, 3, 7, 11, 12, 13, 14, 23, 32, 34, 36, 38, 40 | xpsdsval 24391 |
. 2
⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = sup({(𝐴((dist‘(toMetSp‘𝑀)) ↾
((Base‘(toMetSp‘𝑀)) × (Base‘(toMetSp‘𝑀))))𝐶), (𝐵((dist‘(toMetSp‘𝑁)) ↾
((Base‘(toMetSp‘𝑁)) × (Base‘(toMetSp‘𝑁))))𝐷)}, ℝ*, <
)) |
| 42 | 34, 38 | ovresd 7600 |
. . . . 5
⊢ (𝜑 → (𝐴((dist‘(toMetSp‘𝑀)) ↾
((Base‘(toMetSp‘𝑀)) × (Base‘(toMetSp‘𝑀))))𝐶) = (𝐴(dist‘(toMetSp‘𝑀))𝐶)) |
| 43 | 16 | oveqd 7448 |
. . . . 5
⊢ (𝜑 → (𝐴𝑀𝐶) = (𝐴(dist‘(toMetSp‘𝑀))𝐶)) |
| 44 | 42, 43 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → (𝐴((dist‘(toMetSp‘𝑀)) ↾
((Base‘(toMetSp‘𝑀)) × (Base‘(toMetSp‘𝑀))))𝐶) = (𝐴𝑀𝐶)) |
| 45 | 36, 40 | ovresd 7600 |
. . . . 5
⊢ (𝜑 → (𝐵((dist‘(toMetSp‘𝑁)) ↾
((Base‘(toMetSp‘𝑁)) × (Base‘(toMetSp‘𝑁))))𝐷) = (𝐵(dist‘(toMetSp‘𝑁))𝐷)) |
| 46 | 25 | oveqd 7448 |
. . . . 5
⊢ (𝜑 → (𝐵𝑁𝐷) = (𝐵(dist‘(toMetSp‘𝑁))𝐷)) |
| 47 | 45, 46 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → (𝐵((dist‘(toMetSp‘𝑁)) ↾
((Base‘(toMetSp‘𝑁)) × (Base‘(toMetSp‘𝑁))))𝐷) = (𝐵𝑁𝐷)) |
| 48 | 44, 47 | preq12d 4741 |
. . 3
⊢ (𝜑 → {(𝐴((dist‘(toMetSp‘𝑀)) ↾
((Base‘(toMetSp‘𝑀)) × (Base‘(toMetSp‘𝑀))))𝐶), (𝐵((dist‘(toMetSp‘𝑁)) ↾
((Base‘(toMetSp‘𝑁)) × (Base‘(toMetSp‘𝑁))))𝐷)} = {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) |
| 49 | 48 | supeq1d 9486 |
. 2
⊢ (𝜑 → sup({(𝐴((dist‘(toMetSp‘𝑀)) ↾
((Base‘(toMetSp‘𝑀)) × (Base‘(toMetSp‘𝑀))))𝐶), (𝐵((dist‘(toMetSp‘𝑁)) ↾
((Base‘(toMetSp‘𝑁)) × (Base‘(toMetSp‘𝑁))))𝐷)}, ℝ*, < ) =
sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
| 50 | 41, 49 | eqtrd 2777 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |