Database
BASIC STRUCTURES
Extensible structures
Definition of the structure product
prdsdsfn
Next ⟩
prdstset
Metamath Proof Explorer
Ascii
Unicode
Theorem
prdsdsfn
Description:
Structure product distance function.
(Contributed by
Mario Carneiro
, 15-Sep-2015)
Ref
Expression
Hypotheses
prdsbas.p
⊢
P
=
S
⨉
𝑠
R
prdsbas.s
⊢
φ
→
S
∈
V
prdsbas.r
⊢
φ
→
R
∈
W
prdsbas.b
⊢
B
=
Base
P
prdsbas.i
⊢
φ
→
dom
⁡
R
=
I
prdsds.l
⊢
D
=
dist
⁡
P
Assertion
prdsdsfn
⊢
φ
→
D
Fn
B
×
B
Proof
Step
Hyp
Ref
Expression
1
prdsbas.p
⊢
P
=
S
⨉
𝑠
R
2
prdsbas.s
⊢
φ
→
S
∈
V
3
prdsbas.r
⊢
φ
→
R
∈
W
4
prdsbas.b
⊢
B
=
Base
P
5
prdsbas.i
⊢
φ
→
dom
⁡
R
=
I
6
prdsds.l
⊢
D
=
dist
⁡
P
7
eqid
⊢
f
∈
B
,
g
∈
B
⟼
sup
ran
⁡
x
∈
I
⟼
f
⁡
x
dist
⁡
R
⁡
x
g
⁡
x
∪
0
ℝ
*
<
=
f
∈
B
,
g
∈
B
⟼
sup
ran
⁡
x
∈
I
⟼
f
⁡
x
dist
⁡
R
⁡
x
g
⁡
x
∪
0
ℝ
*
<
8
xrltso
⊢
<
Or
ℝ
*
9
8
supex
⊢
sup
ran
⁡
x
∈
I
⟼
f
⁡
x
dist
⁡
R
⁡
x
g
⁡
x
∪
0
ℝ
*
<
∈
V
10
7
9
fnmpoi
⊢
f
∈
B
,
g
∈
B
⟼
sup
ran
⁡
x
∈
I
⟼
f
⁡
x
dist
⁡
R
⁡
x
g
⁡
x
∪
0
ℝ
*
<
Fn
B
×
B
11
1
2
3
4
5
6
prdsds
⊢
φ
→
D
=
f
∈
B
,
g
∈
B
⟼
sup
ran
⁡
x
∈
I
⟼
f
⁡
x
dist
⁡
R
⁡
x
g
⁡
x
∪
0
ℝ
*
<
12
11
fneq1d
⊢
φ
→
D
Fn
B
×
B
↔
f
∈
B
,
g
∈
B
⟼
sup
ran
⁡
x
∈
I
⟼
f
⁡
x
dist
⁡
R
⁡
x
g
⁡
x
∪
0
ℝ
*
<
Fn
B
×
B
13
10
12
mpbiri
⊢
φ
→
D
Fn
B
×
B