Metamath Proof Explorer


Theorem xpsdsval

Description: Value of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses xpsds.t 𝑇 = ( 𝑅 ×s 𝑆 )
xpsds.x 𝑋 = ( Base ‘ 𝑅 )
xpsds.y 𝑌 = ( Base ‘ 𝑆 )
xpsds.1 ( 𝜑𝑅𝑉 )
xpsds.2 ( 𝜑𝑆𝑊 )
xpsds.p 𝑃 = ( dist ‘ 𝑇 )
xpsds.m 𝑀 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) )
xpsds.n 𝑁 = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) )
xpsds.3 ( 𝜑𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
xpsds.4 ( 𝜑𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
xpsds.a ( 𝜑𝐴𝑋 )
xpsds.b ( 𝜑𝐵𝑌 )
xpsds.c ( 𝜑𝐶𝑋 )
xpsds.d ( 𝜑𝐷𝑌 )
Assertion xpsdsval ( 𝜑 → ( ⟨ 𝐴 , 𝐵𝑃𝐶 , 𝐷 ⟩ ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 xpsds.t 𝑇 = ( 𝑅 ×s 𝑆 )
2 xpsds.x 𝑋 = ( Base ‘ 𝑅 )
3 xpsds.y 𝑌 = ( Base ‘ 𝑆 )
4 xpsds.1 ( 𝜑𝑅𝑉 )
5 xpsds.2 ( 𝜑𝑆𝑊 )
6 xpsds.p 𝑃 = ( dist ‘ 𝑇 )
7 xpsds.m 𝑀 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) )
8 xpsds.n 𝑁 = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) )
9 xpsds.3 ( 𝜑𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
10 xpsds.4 ( 𝜑𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
11 xpsds.a ( 𝜑𝐴𝑋 )
12 xpsds.b ( 𝜑𝐵𝑌 )
13 xpsds.c ( 𝜑𝐶𝑋 )
14 xpsds.d ( 𝜑𝐷𝑌 )
15 eqid ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
16 eqid ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
17 eqid ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
18 1 2 3 4 5 15 16 17 xpsval ( 𝜑𝑇 = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
19 1 2 3 4 5 15 16 17 xpsrnbas ( 𝜑 → ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
20 15 xpsff1o2 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
21 f1ocnv ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
22 20 21 mp1i ( 𝜑 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
23 ovexd ( 𝜑 → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ V )
24 eqid ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) = ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
25 1 2 3 4 5 6 7 8 9 10 xpsxmetlem ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
26 ssid ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
27 xmetres2 ( ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ∧ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) ∈ ( ∞Met ‘ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
28 25 26 27 sylancl ( 𝜑 → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) ∈ ( ∞Met ‘ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
29 df-ov ( 𝐴 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐵 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
30 15 xpsfval ( ( 𝐴𝑋𝐵𝑌 ) → ( 𝐴 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐵 ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
31 11 12 30 syl2anc ( 𝜑 → ( 𝐴 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐵 ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
32 29 31 eqtr3id ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
33 11 12 opelxpd ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) )
34 f1of ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
35 20 34 ax-mp ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
36 35 ffvelrni ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
37 33 36 syl ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
38 32 37 eqeltrrd ( 𝜑 → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
39 df-ov ( 𝐶 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐷 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ )
40 15 xpsfval ( ( 𝐶𝑋𝐷𝑌 ) → ( 𝐶 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐷 ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } )
41 13 14 40 syl2anc ( 𝜑 → ( 𝐶 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐷 ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } )
42 39 41 eqtr3id ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } )
43 13 14 opelxpd ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) )
44 35 ffvelrni ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
45 43 44 syl ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
46 42 45 eqeltrrd ( 𝜑 → { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
47 18 19 22 23 24 6 28 38 46 imasdsf1o ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) 𝑃 ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) )
48 38 46 ovresd ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) )
49 47 48 eqtrd ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) 𝑃 ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) )
50 f1ocnvfv ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) = ⟨ 𝐴 , 𝐵 ⟩ ) )
51 20 33 50 sylancr ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) = ⟨ 𝐴 , 𝐵 ⟩ ) )
52 32 51 mpd ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) = ⟨ 𝐴 , 𝐵 ⟩ )
53 f1ocnvfv ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = ⟨ 𝐶 , 𝐷 ⟩ ) )
54 20 43 53 sylancr ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = ⟨ 𝐶 , 𝐷 ⟩ ) )
55 42 54 mpd ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = ⟨ 𝐶 , 𝐷 ⟩ )
56 52 55 oveq12d ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) 𝑃 ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ) = ( ⟨ 𝐴 , 𝐵𝑃𝐶 , 𝐷 ⟩ ) )
57 eqid ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
58 fvexd ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
59 2on 2o ∈ On
60 59 a1i ( 𝜑 → 2o ∈ On )
61 fnpr2o ( ( 𝑅𝑉𝑆𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
62 4 5 61 syl2anc ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
63 38 19 eleqtrd ( 𝜑 → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
64 46 19 eleqtrd ( 𝜑 → { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
65 eqid ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
66 17 57 58 60 62 63 64 65 prdsdsval ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = sup ( ( ran ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
67 df2o3 2o = { ∅ , 1o }
68 67 rexeqi ( ∃ 𝑘 ∈ 2o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ ∃ 𝑘 ∈ { ∅ , 1o } 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) )
69 0ex ∅ ∈ V
70 1oex 1o ∈ V
71 2fveq3 ( 𝑘 = ∅ → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) )
72 fveq2 ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) )
73 fveq2 ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) )
74 71 72 73 oveq123d ( 𝑘 = ∅ → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ) )
75 74 eqeq2d ( 𝑘 = ∅ → ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ) ) )
76 2fveq3 ( 𝑘 = 1o → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) )
77 fveq2 ( 𝑘 = 1o → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) )
78 fveq2 ( 𝑘 = 1o → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) )
79 76 77 78 oveq123d ( 𝑘 = 1o → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) )
80 79 eqeq2d ( 𝑘 = 1o → ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) ) )
81 69 70 75 80 rexpr ( ∃ 𝑘 ∈ { ∅ , 1o } 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ) ∨ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) ) )
82 68 81 bitri ( ∃ 𝑘 ∈ 2o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ) ∨ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) ) )
83 fvpr0o ( 𝑅𝑉 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
84 4 83 syl ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
85 84 fveq2d ( 𝜑 → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) = ( dist ‘ 𝑅 ) )
86 fvpr0o ( 𝐴𝑋 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
87 11 86 syl ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
88 fvpr0o ( 𝐶𝑋 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) = 𝐶 )
89 13 88 syl ( 𝜑 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) = 𝐶 )
90 85 87 89 oveq123d ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ) = ( 𝐴 ( dist ‘ 𝑅 ) 𝐶 ) )
91 7 oveqi ( 𝐴 𝑀 𝐶 ) = ( 𝐴 ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐶 )
92 11 13 ovresd ( 𝜑 → ( 𝐴 ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐶 ) = ( 𝐴 ( dist ‘ 𝑅 ) 𝐶 ) )
93 91 92 eqtrid ( 𝜑 → ( 𝐴 𝑀 𝐶 ) = ( 𝐴 ( dist ‘ 𝑅 ) 𝐶 ) )
94 90 93 eqtr4d ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ) = ( 𝐴 𝑀 𝐶 ) )
95 94 eqeq2d ( 𝜑 → ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ) ↔ 𝑥 = ( 𝐴 𝑀 𝐶 ) ) )
96 fvpr1o ( 𝑆𝑊 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
97 5 96 syl ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
98 97 fveq2d ( 𝜑 → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) = ( dist ‘ 𝑆 ) )
99 fvpr1o ( 𝐵𝑌 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) = 𝐵 )
100 12 99 syl ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) = 𝐵 )
101 fvpr1o ( 𝐷𝑌 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) = 𝐷 )
102 14 101 syl ( 𝜑 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) = 𝐷 )
103 98 100 102 oveq123d ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) = ( 𝐵 ( dist ‘ 𝑆 ) 𝐷 ) )
104 8 oveqi ( 𝐵 𝑁 𝐷 ) = ( 𝐵 ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) ) 𝐷 )
105 12 14 ovresd ( 𝜑 → ( 𝐵 ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) ) 𝐷 ) = ( 𝐵 ( dist ‘ 𝑆 ) 𝐷 ) )
106 104 105 eqtrid ( 𝜑 → ( 𝐵 𝑁 𝐷 ) = ( 𝐵 ( dist ‘ 𝑆 ) 𝐷 ) )
107 103 106 eqtr4d ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) = ( 𝐵 𝑁 𝐷 ) )
108 107 eqeq2d ( 𝜑 → ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) ↔ 𝑥 = ( 𝐵 𝑁 𝐷 ) ) )
109 95 108 orbi12d ( 𝜑 → ( ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ) ∨ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) ) ↔ ( 𝑥 = ( 𝐴 𝑀 𝐶 ) ∨ 𝑥 = ( 𝐵 𝑁 𝐷 ) ) ) )
110 82 109 syl5bb ( 𝜑 → ( ∃ 𝑘 ∈ 2o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ ( 𝑥 = ( 𝐴 𝑀 𝐶 ) ∨ 𝑥 = ( 𝐵 𝑁 𝐷 ) ) ) )
111 eqid ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) )
112 111 elrnmpt ( 𝑥 ∈ V → ( 𝑥 ∈ ran ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ↔ ∃ 𝑘 ∈ 2o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) )
113 112 elv ( 𝑥 ∈ ran ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ↔ ∃ 𝑘 ∈ 2o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) )
114 vex 𝑥 ∈ V
115 114 elpr ( 𝑥 ∈ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ↔ ( 𝑥 = ( 𝐴 𝑀 𝐶 ) ∨ 𝑥 = ( 𝐵 𝑁 𝐷 ) ) )
116 110 113 115 3bitr4g ( 𝜑 → ( 𝑥 ∈ ran ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ↔ 𝑥 ∈ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ) )
117 116 eqrdv ( 𝜑 → ran ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) = { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } )
118 117 uneq1d ( 𝜑 → ( ran ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ∪ { 0 } ) = ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ∪ { 0 } ) )
119 uncom ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ∪ { 0 } ) = ( { 0 } ∪ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } )
120 118 119 eqtrdi ( 𝜑 → ( ran ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ∪ { 0 } ) = ( { 0 } ∪ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ) )
121 120 supeq1d ( 𝜑 → sup ( ( ran ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) = sup ( ( { 0 } ∪ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ) , ℝ* , < ) )
122 0xr 0 ∈ ℝ*
123 122 a1i ( 𝜑 → 0 ∈ ℝ* )
124 123 snssd ( 𝜑 → { 0 } ⊆ ℝ* )
125 xmetcl ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴𝑋𝐶𝑋 ) → ( 𝐴 𝑀 𝐶 ) ∈ ℝ* )
126 9 11 13 125 syl3anc ( 𝜑 → ( 𝐴 𝑀 𝐶 ) ∈ ℝ* )
127 xmetcl ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐵𝑌𝐷𝑌 ) → ( 𝐵 𝑁 𝐷 ) ∈ ℝ* )
128 10 12 14 127 syl3anc ( 𝜑 → ( 𝐵 𝑁 𝐷 ) ∈ ℝ* )
129 126 128 prssd ( 𝜑 → { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ⊆ ℝ* )
130 xrltso < Or ℝ*
131 supsn ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
132 130 122 131 mp2an sup ( { 0 } , ℝ* , < ) = 0
133 supxrcl ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ⊆ ℝ* → sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) ∈ ℝ* )
134 129 133 syl ( 𝜑 → sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) ∈ ℝ* )
135 xmetge0 ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴𝑋𝐶𝑋 ) → 0 ≤ ( 𝐴 𝑀 𝐶 ) )
136 9 11 13 135 syl3anc ( 𝜑 → 0 ≤ ( 𝐴 𝑀 𝐶 ) )
137 ovex ( 𝐴 𝑀 𝐶 ) ∈ V
138 137 prid1 ( 𝐴 𝑀 𝐶 ) ∈ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) }
139 supxrub ( ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ⊆ ℝ* ∧ ( 𝐴 𝑀 𝐶 ) ∈ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ) → ( 𝐴 𝑀 𝐶 ) ≤ sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )
140 129 138 139 sylancl ( 𝜑 → ( 𝐴 𝑀 𝐶 ) ≤ sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )
141 123 126 134 136 140 xrletrd ( 𝜑 → 0 ≤ sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )
142 132 141 eqbrtrid ( 𝜑 → sup ( { 0 } , ℝ* , < ) ≤ sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )
143 supxrun ( ( { 0 } ⊆ ℝ* ∧ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ⊆ ℝ* ∧ sup ( { 0 } , ℝ* , < ) ≤ sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) ) → sup ( ( { 0 } ∪ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ) , ℝ* , < ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )
144 124 129 142 143 syl3anc ( 𝜑 → sup ( ( { 0 } ∪ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ) , ℝ* , < ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )
145 66 121 144 3eqtrd ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )
146 49 56 145 3eqtr3d ( 𝜑 → ( ⟨ 𝐴 , 𝐵𝑃𝐶 , 𝐷 ⟩ ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ* , < ) )