Description: Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prdsbas.p | |
|
prdsbas.s | |
||
prdsbas.r | |
||
prdsbas.b | |
||
prdsbas.i | |
||
prdsds.l | |
||
Assertion | prdsds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prdsbas.p | |
|
2 | prdsbas.s | |
|
3 | prdsbas.r | |
|
4 | prdsbas.b | |
|
5 | prdsbas.i | |
|
6 | prdsds.l | |
|
7 | eqid | |
|
8 | 1 2 3 4 5 | prdsbas | |
9 | eqid | |
|
10 | 1 2 3 4 5 9 | prdsplusg | |
11 | eqid | |
|
12 | 1 2 3 4 5 11 | prdsmulr | |
13 | eqid | |
|
14 | 1 2 3 4 5 7 13 | prdsvsca | |
15 | eqidd | |
|
16 | eqidd | |
|
17 | eqid | |
|
18 | 1 2 3 4 5 17 | prdsle | |
19 | eqidd | |
|
20 | eqidd | |
|
21 | eqidd | |
|
22 | 1 7 5 8 10 12 14 15 16 18 19 20 21 2 3 | prdsval | |
23 | dsid | |
|
24 | 4 | fvexi | |
25 | xrex | |
|
26 | 25 | uniex | |
27 | 26 | pwex | |
28 | df-sup | |
|
29 | ssrab2 | |
|
30 | 29 | unissi | |
31 | 26 30 | elpwi2 | |
32 | 28 31 | eqeltri | |
33 | 32 | rgen2w | |
34 | 24 24 27 33 | mpoexw | |
35 | 34 | a1i | |
36 | snsstp3 | |
|
37 | ssun1 | |
|
38 | 36 37 | sstri | |
39 | ssun2 | |
|
40 | 38 39 | sstri | |
41 | 22 6 23 35 40 | prdsbaslem | |