Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem2.1 |
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) |
2 |
|
oveq2 |
|- ( m = M -> ( 0 ... m ) = ( 0 ... M ) ) |
3 |
2
|
oveq2d |
|- ( m = M -> ( RR ^m ( 0 ... m ) ) = ( RR ^m ( 0 ... M ) ) ) |
4 |
|
fveqeq2 |
|- ( m = M -> ( ( p ` m ) = B <-> ( p ` M ) = B ) ) |
5 |
4
|
anbi2d |
|- ( m = M -> ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) <-> ( ( p ` 0 ) = A /\ ( p ` M ) = B ) ) ) |
6 |
|
oveq2 |
|- ( m = M -> ( 0 ..^ m ) = ( 0 ..^ M ) ) |
7 |
6
|
raleqdv |
|- ( m = M -> ( A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) ) |
8 |
5 7
|
anbi12d |
|- ( m = M -> ( ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = A /\ ( p ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) ) ) |
9 |
3 8
|
rabeqbidv |
|- ( m = M -> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } = { p e. ( RR ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = A /\ ( p ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) |
10 |
|
ovex |
|- ( RR ^m ( 0 ... M ) ) e. _V |
11 |
10
|
rabex |
|- { p e. ( RR ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = A /\ ( p ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } e. _V |
12 |
9 1 11
|
fvmpt |
|- ( M e. NN -> ( P ` M ) = { p e. ( RR ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = A /\ ( p ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) |
13 |
12
|
eleq2d |
|- ( M e. NN -> ( Q e. ( P ` M ) <-> Q e. { p e. ( RR ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = A /\ ( p ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ) |
14 |
|
fveq1 |
|- ( p = Q -> ( p ` 0 ) = ( Q ` 0 ) ) |
15 |
14
|
eqeq1d |
|- ( p = Q -> ( ( p ` 0 ) = A <-> ( Q ` 0 ) = A ) ) |
16 |
|
fveq1 |
|- ( p = Q -> ( p ` M ) = ( Q ` M ) ) |
17 |
16
|
eqeq1d |
|- ( p = Q -> ( ( p ` M ) = B <-> ( Q ` M ) = B ) ) |
18 |
15 17
|
anbi12d |
|- ( p = Q -> ( ( ( p ` 0 ) = A /\ ( p ` M ) = B ) <-> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) ) ) |
19 |
|
fveq1 |
|- ( p = Q -> ( p ` i ) = ( Q ` i ) ) |
20 |
|
fveq1 |
|- ( p = Q -> ( p ` ( i + 1 ) ) = ( Q ` ( i + 1 ) ) ) |
21 |
19 20
|
breq12d |
|- ( p = Q -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) |
22 |
21
|
ralbidv |
|- ( p = Q -> ( A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) |
23 |
18 22
|
anbi12d |
|- ( p = Q -> ( ( ( ( p ` 0 ) = A /\ ( p ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) |
24 |
23
|
elrab |
|- ( Q e. { p e. ( RR ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = A /\ ( p ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) |
25 |
13 24
|
bitrdi |
|- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) ) |