Theorem tmsxpsval

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	tmsxpsval	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑃 ⟨ 𝐶 , 𝐷 ⟩ ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )

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		eqid	⊢ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) = ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) )
9		eqid	⊢ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) = ( Base ‘ ( toMetSp ‘ 𝑀 ) )
10		eqid	⊢ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) = ( Base ‘ ( toMetSp ‘ 𝑁 ) )
11		eqid	⊢ ( toMetSp ‘ 𝑀 ) = ( toMetSp ‘ 𝑀 )
12	11	tmsxms	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( toMetSp ‘ 𝑀 ) ∈ ∞MetSp )
13	2 12	syl	⊢ ( 𝜑 → ( toMetSp ‘ 𝑀 ) ∈ ∞MetSp )
14		eqid	⊢ ( toMetSp ‘ 𝑁 ) = ( toMetSp ‘ 𝑁 )
15	14	tmsxms	⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → ( toMetSp ‘ 𝑁 ) ∈ ∞MetSp )
16	3 15	syl	⊢ ( 𝜑 → ( toMetSp ‘ 𝑁 ) ∈ ∞MetSp )
17		eqid	⊢ ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) ) = ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) )
18		eqid	⊢ ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑁 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) ) = ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑁 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) )
19	11	tmsds	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝑀 = ( dist ‘ ( toMetSp ‘ 𝑀 ) ) )
20	2 19	syl	⊢ ( 𝜑 → 𝑀 = ( dist ‘ ( toMetSp ‘ 𝑀 ) ) )
21	11	tmsbas	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ ( toMetSp ‘ 𝑀 ) ) )
22	2 21	syl	⊢ ( 𝜑 → 𝑋 = ( Base ‘ ( toMetSp ‘ 𝑀 ) ) )
23	22	fveq2d	⊢ ( 𝜑 → ( ∞Met ‘ 𝑋 ) = ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) )
24	2 20 23	3eltr3d	⊢ ( 𝜑 → ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ∈ ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) )
25		ssid	⊢ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ⊆ ( Base ‘ ( toMetSp ‘ 𝑀 ) )
26		xmetres2	⊢ ( ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ∈ ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) ∧ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ⊆ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) → ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) )
27	24 25 26	sylancl	⊢ ( 𝜑 → ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) )
28	14	tmsds	⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝑁 = ( dist ‘ ( toMetSp ‘ 𝑁 ) ) )
29	3 28	syl	⊢ ( 𝜑 → 𝑁 = ( dist ‘ ( toMetSp ‘ 𝑁 ) ) )
30	14	tmsbas	⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝑌 = ( Base ‘ ( toMetSp ‘ 𝑁 ) ) )
31	3 30	syl	⊢ ( 𝜑 → 𝑌 = ( Base ‘ ( toMetSp ‘ 𝑁 ) ) )
32	31	fveq2d	⊢ ( 𝜑 → ( ∞Met ‘ 𝑌 ) = ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) )
33	3 29 32	3eltr3d	⊢ ( 𝜑 → ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ∈ ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) )
34		ssid	⊢ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ⊆ ( Base ‘ ( toMetSp ‘ 𝑁 ) )
35		xmetres2	⊢ ( ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ∈ ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) ∧ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ⊆ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) → ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑁 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) )
36	33 34 35	sylancl	⊢ ( 𝜑 → ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑁 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) )
37	4 22	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) )
38	5 31	eleqtrd	⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) )
39	6 22	eleqtrd	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) )
40	7 31	eleqtrd	⊢ ( 𝜑 → 𝐷 ∈ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) )
41	8 9 10 13 16 1 17 18 27 36 37 38 39 40	xpsdsval	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑃 ⟨ 𝐶 , 𝐷 ⟩ ) = sup ( { ( 𝐴 ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) ) 𝐶 ) , ( 𝐵 ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑁 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) ) 𝐷 ) } , ℝ* , < ) )
42	37 39	ovresd	⊢ ( 𝜑 → ( 𝐴 ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) ) 𝐶 ) = ( 𝐴 ( dist ‘ ( toMetSp ‘ 𝑀 ) ) 𝐶 ) )
43	20	oveqd	⊢ ( 𝜑 → ( 𝐴 𝑀 𝐶 ) = ( 𝐴 ( dist ‘ ( toMetSp ‘ 𝑀 ) ) 𝐶 ) )
44	42 43	eqtr4d	⊢ ( 𝜑 → ( 𝐴 ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) ) 𝐶 ) = ( 𝐴 𝑀 𝐶 ) )
45	38 40	ovresd	⊢ ( 𝜑 → ( 𝐵 ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑁 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) ) 𝐷 ) = ( 𝐵 ( dist ‘ ( toMetSp ‘ 𝑁 ) ) 𝐷 ) )
46	29	oveqd	⊢ ( 𝜑 → ( 𝐵 𝑁 𝐷 ) = ( 𝐵 ( dist ‘ ( toMetSp ‘ 𝑁 ) ) 𝐷 ) )
47	45 46	eqtr4d	⊢ ( 𝜑 → ( 𝐵 ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑁 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) ) 𝐷 ) = ( 𝐵 𝑁 𝐷 ) )
48	44 47	preq12d	⊢ ( 𝜑 → { ( 𝐴 ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) ) 𝐶 ) , ( 𝐵 ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑁 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) ) 𝐷 ) } = { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } )
49	48	supeq1d	⊢ ( 𝜑 → sup ( { ( 𝐴 ( ( dist ‘ ( toMetSp ‘ 𝑀 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑀 ) ) ) ) 𝐶 ) , ( 𝐵 ( ( dist ‘ ( toMetSp ‘ 𝑁 ) ) ↾ ( ( Base ‘ ( toMetSp ‘ 𝑁 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) ) 𝐷 ) } , ℝ* , < ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )
50	41 49	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑃 ⟨ 𝐶 , 𝐷 ⟩ ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )