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	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
16		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
17		eqid	⊢ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } )
18	1 2 3 4 5 15 16 17	xpsval	⊢ ( 𝜑 → 𝑇 = ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) “_s ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
19	1 2 3 4 5 15 16 17	xpsrnbas	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
20	15	xpsff1o2	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
21		f1ocnv	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) → ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
22	20 21	mp1i	⊢ ( 𝜑 → ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
23		ovexd	⊢ ( 𝜑 → ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ∈ V )
24		eqid	⊢ ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ) = ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )
25	1 2 3 4 5 6 7 8 9 10	xpsxmetlem	⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )
26		ssid	⊢ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
27		xmetres2	⊢ ( ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ∧ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )
28	25 26 27	sylancl	⊢ ( 𝜑 → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )
29		df-ov	⊢ ( 𝐴 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) 𝐵 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
30	15	xpsfval	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) 𝐵 ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } )
31	11 12 30	syl2anc	⊢ ( 𝜑 → ( 𝐴 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) 𝐵 ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } )
32	29 31	eqtr3id	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } )
33	11 12	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) )
34		f1of	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
35	20 34	ax-mp	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
36	35	ffvelcdmi	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
37	33 36	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
38	32 37	eqeltrrd	⊢ ( 𝜑 → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
39		df-ov	⊢ ( 𝐶 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) 𝐷 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ )
40	15	xpsfval	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) → ( 𝐶 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) 𝐷 ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } )
41	13 14 40	syl2anc	⊢ ( 𝜑 → ( 𝐶 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) 𝐷 ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } )
42	39 41	eqtr3id	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } )
43	13 14	opelxpd	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) )
44	35	ffvelcdmi	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
45	43 44	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
46	42 45	eqeltrrd	⊢ ( 𝜑 → { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
47	18 19 22 23 24 6 28 38 46	imasdsf1o	⊢ ( 𝜑 → ( ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ) 𝑃 ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) )
48	38 46	ovresd	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) )
49	47 48	eqtrd	⊢ ( 𝜑 → ( ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ) 𝑃 ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) )
50		f1ocnvfv	⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ) = ⟨ 𝐴 , 𝐵 ⟩ ) )
51	20 33 50	sylancr	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ) = ⟨ 𝐴 , 𝐵 ⟩ ) )
52	32 51	mpd	⊢ ( 𝜑 → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ) = ⟨ 𝐴 , 𝐵 ⟩ )
53		f1ocnvfv	⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) = ⟨ 𝐶 , 𝐷 ⟩ ) )
54	20 43 53	sylancr	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) = ⟨ 𝐶 , 𝐷 ⟩ ) )
55	42 54	mpd	⊢ ( 𝜑 → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) = ⟨ 𝐶 , 𝐷 ⟩ )
56	52 55	oveq12d	⊢ ( 𝜑 → ( ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ) 𝑃 ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝑃 ⟨ 𝐶 , 𝐷 ⟩ ) )
57		eqid	⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) )
58		fvexd	⊢ ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
59		2on	⊢ 2_o ∈ On
60	59	a1i	⊢ ( 𝜑 → 2_o ∈ On )
61		fnpr2o	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o )
62	4 5 61	syl2anc	⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o )
63	38 19	eleqtrd	⊢ ( 𝜑 → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
64	46 19	eleqtrd	⊢ ( 𝜑 → { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
65		eqid	⊢ ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) )
66	17 57 58 60 62 63 64 65	prdsdsval	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) = sup ( ( ran ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )
67		df2o3	⊢ 2_o = { ∅ , 1_o }
68	67	rexeqi	⊢ ( ∃ 𝑘 ∈ 2_o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ ∃ 𝑘 ∈ { ∅ , 1_o } 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) )
69		0ex	⊢ ∅ ∈ V
70		1oex	⊢ 1_o ∈ V
71		2fveq3	⊢ ( 𝑘 = ∅ → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) )
72		fveq2	⊢ ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) )
73		fveq2	⊢ ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) )
74	71 72 73	oveq123d	⊢ ( 𝑘 = ∅ → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) ) )
75	74	eqeq2d	⊢ ( 𝑘 = ∅ → ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) ) ) )
76		2fveq3	⊢ ( 𝑘 = 1_o → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) )
77		fveq2	⊢ ( 𝑘 = 1_o → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) )
78		fveq2	⊢ ( 𝑘 = 1_o → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) )
79	76 77 78	oveq123d	⊢ ( 𝑘 = 1_o → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) ) )
80	79	eqeq2d	⊢ ( 𝑘 = 1_o → ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) ) ) )
81	69 70 75 80	rexpr	⊢ ( ∃ 𝑘 ∈ { ∅ , 1_o } 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) ) ∨ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) ) ) )
82	68 81	bitri	⊢ ( ∃ 𝑘 ∈ 2_o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) ) ∨ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) ) ) )
83		fvpr0o	⊢ ( 𝑅 ∈ 𝑉 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
84	4 83	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
85	84	fveq2d	⊢ ( 𝜑 → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) = ( dist ‘ 𝑅 ) )
86		fvpr0o	⊢ ( 𝐴 ∈ 𝑋 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
87	11 86	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
88		fvpr0o	⊢ ( 𝐶 ∈ 𝑋 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) = 𝐶 )
89	13 88	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) = 𝐶 )
90	85 87 89	oveq123d	⊢ ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) ) = ( 𝐴 ( dist ‘ 𝑅 ) 𝐶 ) )
91	7	oveqi	⊢ ( 𝐴 𝑀 𝐶 ) = ( 𝐴 ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐶 )
92	11 13	ovresd	⊢ ( 𝜑 → ( 𝐴 ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐶 ) = ( 𝐴 ( dist ‘ 𝑅 ) 𝐶 ) )
93	91 92	eqtrid	⊢ ( 𝜑 → ( 𝐴 𝑀 𝐶 ) = ( 𝐴 ( dist ‘ 𝑅 ) 𝐶 ) )
94	90 93	eqtr4d	⊢ ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) ) = ( 𝐴 𝑀 𝐶 ) )
95	94	eqeq2d	⊢ ( 𝜑 → ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) ) ↔ 𝑥 = ( 𝐴 𝑀 𝐶 ) ) )
96		fvpr1o	⊢ ( 𝑆 ∈ 𝑊 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) = 𝑆 )
97	5 96	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) = 𝑆 )
98	97	fveq2d	⊢ ( 𝜑 → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) = ( dist ‘ 𝑆 ) )
99		fvpr1o	⊢ ( 𝐵 ∈ 𝑌 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) = 𝐵 )
100	12 99	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) = 𝐵 )
101		fvpr1o	⊢ ( 𝐷 ∈ 𝑌 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) = 𝐷 )
102	14 101	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) = 𝐷 )
103	98 100 102	oveq123d	⊢ ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) ) = ( 𝐵 ( dist ‘ 𝑆 ) 𝐷 ) )
104	8	oveqi	⊢ ( 𝐵 𝑁 𝐷 ) = ( 𝐵 ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) ) 𝐷 )
105	12 14	ovresd	⊢ ( 𝜑 → ( 𝐵 ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) ) 𝐷 ) = ( 𝐵 ( dist ‘ 𝑆 ) 𝐷 ) )
106	104 105	eqtrid	⊢ ( 𝜑 → ( 𝐵 𝑁 𝐷 ) = ( 𝐵 ( dist ‘ 𝑆 ) 𝐷 ) )
107	103 106	eqtr4d	⊢ ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) ) = ( 𝐵 𝑁 𝐷 ) )
108	107	eqeq2d	⊢ ( 𝜑 → ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) ) ↔ 𝑥 = ( 𝐵 𝑁 𝐷 ) ) )
109	95 108	orbi12d	⊢ ( 𝜑 → ( ( 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ ∅ ) ) ∨ 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 1_o ) ) ) ↔ ( 𝑥 = ( 𝐴 𝑀 𝐶 ) ∨ 𝑥 = ( 𝐵 𝑁 𝐷 ) ) ) )
110	82 109	bitrid	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 2_o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ↔ ( 𝑥 = ( 𝐴 𝑀 𝐶 ) ∨ 𝑥 = ( 𝐵 𝑁 𝐷 ) ) ) )
111		eqid	⊢ ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) )
112	111	elrnmpt	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ran ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ↔ ∃ 𝑘 ∈ 2_o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) )
113	112	elv	⊢ ( 𝑥 ∈ ran ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ↔ ∃ 𝑘 ∈ 2_o 𝑥 = ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) )
114		vex	⊢ 𝑥 ∈ V
115	114	elpr	⊢ ( 𝑥 ∈ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ↔ ( 𝑥 = ( 𝐴 𝑀 𝐶 ) ∨ 𝑥 = ( 𝐵 𝑁 𝐷 ) ) )
116	110 113 115	3bitr4g	⊢ ( 𝜑 → ( 𝑥 ∈ ran ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ↔ 𝑥 ∈ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ) )
117	116	eqrdv	⊢ ( 𝜑 → ran ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) = { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } )
118	117	uneq1d	⊢ ( 𝜑 → ( ran ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ∪ { 0 } ) = ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ∪ { 0 } ) )
119		uncom	⊢ ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ∪ { 0 } ) = ( { 0 } ∪ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } )
120	118 119	eqtrdi	⊢ ( 𝜑 → ( ran ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ∪ { 0 } ) = ( { 0 } ∪ { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } ) )
121	120	supeq1d	⊢ ( 𝜑 → sup ( ( ran ( 𝑘 ∈ 2_o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝑘 ) ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) ∪ { 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	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1_o , 𝐷 ⟩ } ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ^* , < ) )
146	49 56 145	3eqtr3d	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑃 ⟨ 𝐶 , 𝐷 ⟩ ) = sup ( { ( 𝐴 𝑀 𝐶 ) , ( 𝐵 𝑁 𝐷 ) } , ℝ^* , < ) )

Metamath Proof Explorer

Theorem xpsdsval

Proof