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