tmsxpsval

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	tmsxpsval	$⊢ φ \to ⟨A, B⟩ P ⟨C, D⟩ = sup (\{A M C, B N D\} ℝ^{*} <)$

Proof

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		eqid	$⊢ toMetSp (M) \times_{𝑠} toMetSp (N) = toMetSp (M) \times_{𝑠} toMetSp (N)$
9		eqid	$⊢ {Base}_{toMetSp (M)} = {Base}_{toMetSp (M)}$
10		eqid	$⊢ {Base}_{toMetSp (N)} = {Base}_{toMetSp (N)}$
11		eqid	$⊢ toMetSp (M) = toMetSp (M)$
12	11	tmsxms	$⊢ M \in ∞Met (X) \to toMetSp (M) \in ∞MetSp$
13	2 12	syl	$⊢ φ \to toMetSp (M) \in ∞MetSp$
14		eqid	$⊢ toMetSp (N) = toMetSp (N)$
15	14	tmsxms	$⊢ N \in ∞Met (Y) \to toMetSp (N) \in ∞MetSp$
16	3 15	syl	$⊢ φ \to toMetSp (N) \in ∞MetSp$
17		eqid	$⊢ {dist (toMetSp (M)) ↾}_{({Base}_{toMetSp (M)} \times {Base}_{toMetSp (M)})} = {dist (toMetSp (M)) ↾}_{({Base}_{toMetSp (M)} \times {Base}_{toMetSp (M)})}$
18		eqid	$⊢ {dist (toMetSp (N)) ↾}_{({Base}_{toMetSp (N)} \times {Base}_{toMetSp (N)})} = {dist (toMetSp (N)) ↾}_{({Base}_{toMetSp (N)} \times {Base}_{toMetSp (N)})}$
19	11	tmsds	$⊢ M \in ∞Met (X) \to M = dist (toMetSp (M))$
20	2 19	syl	$⊢ φ \to M = dist (toMetSp (M))$
21	11	tmsbas	$⊢ M \in ∞Met (X) \to X = {Base}_{toMetSp (M)}$
22	2 21	syl	$⊢ φ \to X = {Base}_{toMetSp (M)}$
23	22	fveq2d	$⊢ φ \to ∞Met (X) = ∞Met ({Base}_{toMetSp (M)})$
24	2 20 23	3eltr3d	$⊢ φ \to dist (toMetSp (M)) \in ∞Met ({Base}_{toMetSp (M)})$
25		ssid	$⊢ {Base}_{toMetSp (M)} \subseteq {Base}_{toMetSp (M)}$
26		xmetres2	$⊢ (dist (toMetSp (M)) \in ∞Met ({Base}_{toMetSp (M)}) \land {Base}_{toMetSp (M)} \subseteq {Base}_{toMetSp (M)}) \to {dist (toMetSp (M)) ↾}_{({Base}_{toMetSp (M)} \times {Base}_{toMetSp (M)})} \in ∞Met ({Base}_{toMetSp (M)})$
27	24 25 26	sylancl	$⊢ φ \to {dist (toMetSp (M)) ↾}_{({Base}_{toMetSp (M)} \times {Base}_{toMetSp (M)})} \in ∞Met ({Base}_{toMetSp (M)})$
28	14	tmsds	$⊢ N \in ∞Met (Y) \to N = dist (toMetSp (N))$
29	3 28	syl	$⊢ φ \to N = dist (toMetSp (N))$
30	14	tmsbas	$⊢ N \in ∞Met (Y) \to Y = {Base}_{toMetSp (N)}$
31	3 30	syl	$⊢ φ \to Y = {Base}_{toMetSp (N)}$
32	31	fveq2d	$⊢ φ \to ∞Met (Y) = ∞Met ({Base}_{toMetSp (N)})$
33	3 29 32	3eltr3d	$⊢ φ \to dist (toMetSp (N)) \in ∞Met ({Base}_{toMetSp (N)})$
34		ssid	$⊢ {Base}_{toMetSp (N)} \subseteq {Base}_{toMetSp (N)}$
35		xmetres2	$⊢ (dist (toMetSp (N)) \in ∞Met ({Base}_{toMetSp (N)}) \land {Base}_{toMetSp (N)} \subseteq {Base}_{toMetSp (N)}) \to {dist (toMetSp (N)) ↾}_{({Base}_{toMetSp (N)} \times {Base}_{toMetSp (N)})} \in ∞Met ({Base}_{toMetSp (N)})$
36	33 34 35	sylancl	$⊢ φ \to {dist (toMetSp (N)) ↾}_{({Base}_{toMetSp (N)} \times {Base}_{toMetSp (N)})} \in ∞Met ({Base}_{toMetSp (N)})$
37	4 22	eleqtrd	$⊢ φ \to A \in {Base}_{toMetSp (M)}$
38	5 31	eleqtrd	$⊢ φ \to B \in {Base}_{toMetSp (N)}$
39	6 22	eleqtrd	$⊢ φ \to C \in {Base}_{toMetSp (M)}$
40	7 31	eleqtrd	$⊢ φ \to D \in {Base}_{toMetSp (N)}$
41	8 9 10 13 16 1 17 18 27 36 37 38 39 40	xpsdsval	$⊢ φ \to ⟨A, B⟩ P ⟨C, D⟩ = sup (\{A ({dist (toMetSp (M)) ↾}_{({Base}_{toMetSp (M)} \times {Base}_{toMetSp (M)})}) C, B ({dist (toMetSp (N)) ↾}_{({Base}_{toMetSp (N)} \times {Base}_{toMetSp (N)})}) D\} ℝ^{*} <)$
42	37 39	ovresd	$⊢ φ \to A ({dist (toMetSp (M)) ↾}_{({Base}_{toMetSp (M)} \times {Base}_{toMetSp (M)})}) C = A dist (toMetSp (M)) C$
43	20	oveqd	$⊢ φ \to A M C = A dist (toMetSp (M)) C$
44	42 43	eqtr4d	$⊢ φ \to A ({dist (toMetSp (M)) ↾}_{({Base}_{toMetSp (M)} \times {Base}_{toMetSp (M)})}) C = A M C$
45	38 40	ovresd	$⊢ φ \to B ({dist (toMetSp (N)) ↾}_{({Base}_{toMetSp (N)} \times {Base}_{toMetSp (N)})}) D = B dist (toMetSp (N)) D$
46	29	oveqd	$⊢ φ \to B N D = B dist (toMetSp (N)) D$
47	45 46	eqtr4d	$⊢ φ \to B ({dist (toMetSp (N)) ↾}_{({Base}_{toMetSp (N)} \times {Base}_{toMetSp (N)})}) D = B N D$
48	44 47	preq12d	$⊢ φ \to \{A ({dist (toMetSp (M)) ↾}_{({Base}_{toMetSp (M)} \times {Base}_{toMetSp (M)})}) C, B ({dist (toMetSp (N)) ↾}_{({Base}_{toMetSp (N)} \times {Base}_{toMetSp (N)})}) D\} = \{A M C, B N D\}$
49	48	supeq1d	$⊢ φ \to sup (\{A ({dist (toMetSp (M)) ↾}_{({Base}_{toMetSp (M)} \times {Base}_{toMetSp (M)})}) C, B ({dist (toMetSp (N)) ↾}_{({Base}_{toMetSp (N)} \times {Base}_{toMetSp (N)})}) D\} ℝ^{} <) = sup (\{A M C, B N D\} ℝ^{} <)$
50	41 49	eqtrd	$⊢ φ \to ⟨A, B⟩ P ⟨C, D⟩ = sup (\{A M C, B N D\} ℝ^{*} <)$

Metamath Proof Explorer

Theorem tmsxpsval

Proof