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 ⊢ 𝑃 = ( dist ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) )
tmsxps.1 ⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
tmsxps.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
tmsxpsval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
tmsxpsval.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
tmsxpsval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
tmsxpsval.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
Assertion tmsxpsval2 ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑃 ⟨ 𝐶 , 𝐷 ⟩ ) = if ( ( 𝐴 𝑀 𝐶 ) ≤ ( 𝐵 𝑁 𝐷 ) , ( 𝐵 𝑁 𝐷 ) , ( 𝐴 𝑀 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 tmsxps.p ⊢ 𝑃 = ( dist ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) )
2 tmsxps.1 ⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
3 tmsxps.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
4 tmsxpsval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
5 tmsxpsval.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
6 tmsxpsval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
7 tmsxpsval.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
8 1 2 3 4 5 6 7 tmsxpsval ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑃 ⟨ 𝐶 , 𝐷 ⟩ ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )
9 xrltso ⊢ < Or ℝ*
10 xmetcl ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐶 ) ∈ ℝ* )
11 2 4 6 10 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝑀 𝐶 ) ∈ ℝ* )
12 xmetcl ⊢ ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌 ) → ( 𝐵 𝑁 𝐷 ) ∈ ℝ* )
13 3 5 7 12 syl3anc ⊢ ( 𝜑 → ( 𝐵 𝑁 𝐷 ) ∈ ℝ* )
14 suppr ⊢ ( ( < Or ℝ* ∧ ( 𝐴 𝑀 𝐶 ) ∈ ℝ* ∧ ( 𝐵 𝑁 𝐷 ) ∈ ℝ* ) → sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) = if ( ( 𝐵 𝑁 𝐷 ) < ( 𝐴 𝑀 𝐶 ) , ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) ) )
15 9 11 13 14 mp3an2i ⊢ ( 𝜑 → sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) = if ( ( 𝐵 𝑁 𝐷 ) < ( 𝐴 𝑀 𝐶 ) , ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) ) )
16 xrltnle ⊢ ( ( ( 𝐵 𝑁 𝐷 ) ∈ ℝ* ∧ ( 𝐴 𝑀 𝐶 ) ∈ ℝ* ) → ( ( 𝐵 𝑁 𝐷 ) < ( 𝐴 𝑀 𝐶 ) ↔ ¬ ( 𝐴 𝑀 𝐶 ) ≤ ( 𝐵 𝑁 𝐷 ) ) )
17 13 11 16 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 𝑁 𝐷 ) < ( 𝐴 𝑀 𝐶 ) ↔ ¬ ( 𝐴 𝑀 𝐶 ) ≤ ( 𝐵 𝑁 𝐷 ) ) )
18 17 ifbid ⊢ ( 𝜑 → if ( ( 𝐵 𝑁 𝐷 ) < ( 𝐴 𝑀 𝐶 ) , ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) ) = if ( ¬ ( 𝐴 𝑀 𝐶 ) ≤ ( 𝐵 𝑁 𝐷 ) , ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) ) )
19 ifnot ⊢ if ( ¬ ( 𝐴 𝑀 𝐶 ) ≤ ( 𝐵 𝑁 𝐷 ) , ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) ) = if ( ( 𝐴 𝑀 𝐶 ) ≤ ( 𝐵 𝑁 𝐷 ) , ( 𝐵 𝑁 𝐷 ) , ( 𝐴 𝑀 𝐶 ) )
20 18 19 eqtrdi ⊢ ( 𝜑 → if ( ( 𝐵 𝑁 𝐷 ) < ( 𝐴 𝑀 𝐶 ) , ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) ) = if ( ( 𝐴 𝑀 𝐶 ) ≤ ( 𝐵 𝑁 𝐷 ) , ( 𝐵 𝑁 𝐷 ) , ( 𝐴 𝑀 𝐶 ) ) )
21 8 15 20 3eqtrd ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑃 ⟨ 𝐶 , 𝐷 ⟩ ) = if ( ( 𝐴 𝑀 𝐶 ) ≤ ( 𝐵 𝑁 𝐷 ) , ( 𝐵 𝑁 𝐷 ) , ( 𝐴 𝑀 𝐶 ) ) )