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) \times_{𝑠} toMetSp (N))$
	tmsxps.1	$⊢ φ \to M \in ∞Met (X)$
	tmsxps.2	$⊢ φ \to N \in ∞Met (Y)$
	tmsxpsval.a	$⊢ φ \to A \in X$
	tmsxpsval.b	$⊢ φ \to B \in Y$
	tmsxpsval.c	$⊢ φ \to C \in X$
	tmsxpsval.d	$⊢ φ \to D \in Y$
Assertion	tmsxpsval2	$⊢ φ \to ⟨A, B⟩ P ⟨C, D⟩ = if (A M C \leq B N D, B N D, A M C)$

Step	Hyp	Ref	Expression
1		tmsxps.p	$⊢ P = dist (toMetSp (M) \times_{𝑠} toMetSp (N))$
2		tmsxps.1	$⊢ φ \to M \in ∞Met (X)$
3		tmsxps.2	$⊢ φ \to N \in ∞Met (Y)$
4		tmsxpsval.a	$⊢ φ \to A \in X$
5		tmsxpsval.b	$⊢ φ \to B \in Y$
6		tmsxpsval.c	$⊢ φ \to C \in X$
7		tmsxpsval.d	$⊢ φ \to D \in Y$
8	1 2 3 4 5 6 7	tmsxpsval	$⊢ φ \to ⟨A, B⟩ P ⟨C, D⟩ = sup (\{A M C, B N D\} ℝ^{*} <)$
9		xrltso	$⊢ < Or ℝ^{*}$
10		xmetcl	$⊢ (M \in ∞Met (X) \land A \in X \land C \in X) \to A M C \in ℝ^{*}$
11	2 4 6 10	syl3anc	$⊢ φ \to A M C \in ℝ^{*}$
12		xmetcl	$⊢ (N \in ∞Met (Y) \land B \in Y \land D \in Y) \to B N D \in ℝ^{*}$
13	3 5 7 12	syl3anc	$⊢ φ \to B N D \in ℝ^{*}$
14		suppr	$⊢ (< Or ℝ^{} \land A M C \in ℝ^{} \land B N D \in ℝ^{}) \to 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	$⊢ φ \to 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 \in ℝ^{} \land A M C \in ℝ^{}) \to (B N D < A M C \leftrightarrow \neg A M C \leq B N D)$
17	13 11 16	syl2anc	$⊢ φ \to (B N D < A M C \leftrightarrow \neg A M C \leq B N D)$
18	17	ifbid	$⊢ φ \to if (B N D < A M C, A M C, B N D) = if (\neg A M C \leq B N D, A M C, B N D)$
19		ifnot	$⊢ if (\neg A M C \leq B N D, A M C, B N D) = if (A M C \leq B N D, B N D, A M C)$
20	18 19	eqtrdi	$⊢ φ \to if (B N D < A M C, A M C, B N D) = if (A M C \leq B N D, B N D, A M C)$
21	8 15 20	3eqtrd	$⊢ φ \to ⟨A, B⟩ P ⟨C, D⟩ = if (A M C \leq B N D, B N D, A M C)$

Metamath Proof Explorer