Metamath Proof Explorer

Theorem tmsxpsval2

Description: Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tmsxps.p ⊢ P = dist ⁡ toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
tmsxps.1 ⊢ φ → M ∈ ∞Met ⁡ X
tmsxps.2 ⊢ φ → N ∈ ∞Met ⁡ Y
tmsxpsval.a ⊢ φ → A ∈ X
tmsxpsval.b ⊢ φ → B ∈ Y
tmsxpsval.c ⊢ φ → C ∈ X
tmsxpsval.d ⊢ φ → D ∈ Y
Assertion tmsxpsval2 ⊢ φ → A B P C D = if A M C ≤ B N D B N D A M C

Proof

Step Hyp Ref Expression
1 tmsxps.p ⊢ P = dist ⁡ toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
2 tmsxps.1 ⊢ φ → M ∈ ∞Met ⁡ X
3 tmsxps.2 ⊢ φ → N ∈ ∞Met ⁡ Y
4 tmsxpsval.a ⊢ φ → A ∈ X
5 tmsxpsval.b ⊢ φ → B ∈ Y
6 tmsxpsval.c ⊢ φ → C ∈ X
7 tmsxpsval.d ⊢ φ → D ∈ Y
8 1 2 3 4 5 6 7 tmsxpsval ⊢ φ → A B P C D = sup A M C B N D ℝ * <
9 xrltso ⊢ < Or ℝ *
10 xmetcl ⊢ M ∈ ∞Met ⁡ X ∧ A ∈ X ∧ C ∈ X → A M C ∈ ℝ *
11 2 4 6 10 syl3anc ⊢ φ → A M C ∈ ℝ *
12 xmetcl ⊢ N ∈ ∞Met ⁡ Y ∧ B ∈ Y ∧ D ∈ Y → B N D ∈ ℝ *
13 3 5 7 12 syl3anc ⊢ φ → B N D ∈ ℝ *
14 suppr ⊢ < Or ℝ * ∧ A M C ∈ ℝ * ∧ B N D ∈ ℝ * → sup A M C B N D ℝ * < = if B N D < A M C A M C B N D
15 9 11 13 14 mp3an2i ⊢ φ → sup A M C B N D ℝ * < = if B N D < A M C A M C B N D
16 xrltnle ⊢ B N D ∈ ℝ * ∧ A M C ∈ ℝ * → B N D < A M C ↔ ¬ A M C ≤ B N D
17 13 11 16 syl2anc ⊢ φ → B N D < A M C ↔ ¬ A M C ≤ B N D
18 17 ifbid ⊢ φ → if B N D < A M C A M C B N D = if ¬ A M C ≤ B N D A M C B N D
19 ifnot ⊢ if ¬ A M C ≤ B N D A M C B N D = if A M C ≤ B N D B N D A M C
20 18 19 eqtrdi ⊢ φ → if B N D < A M C A M C B N D = if A M C ≤ B N D B N D A M C
21 8 15 20 3eqtrd ⊢ φ → A B P C D = if A M C ≤ B N D B N D A M C