Description: The mapping from fiducial co-atom w to its set of lattice dilations. (Contributed by NM, 11-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ldilset.b | |
|
ldilset.l | |
||
ldilset.h | |
||
ldilset.i | |
||
Assertion | ldilfset | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ldilset.b | |
|
2 | ldilset.l | |
|
3 | ldilset.h | |
|
4 | ldilset.i | |
|
5 | elex | |
|
6 | fveq2 | |
|
7 | 6 3 | eqtr4di | |
8 | fveq2 | |
|
9 | 8 4 | eqtr4di | |
10 | fveq2 | |
|
11 | 10 1 | eqtr4di | |
12 | fveq2 | |
|
13 | 12 2 | eqtr4di | |
14 | 13 | breqd | |
15 | 14 | imbi1d | |
16 | 11 15 | raleqbidv | |
17 | 9 16 | rabeqbidv | |
18 | 7 17 | mpteq12dv | |
19 | df-ldil | |
|
20 | 18 19 3 | mptfvmpt | |
21 | 5 20 | syl | |