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 ( ( 𝐴 𝑀 𝐶 ) ≤ ( 𝐵 𝑁 𝐷 ) , ( 𝐵 𝑁 𝐷 ) , ( 𝐴 𝑀 𝐶 ) ) )

Metamath Proof Explorer

Theorem tmsxpsval2

Proof