Metamath Proof Explorer

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 ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )