Metamath Proof Explorer


Theorem fourierdlem34

Description: A partition is one to one. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem34.p
|- 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 ) ) ) } )
fourierdlem34.m
|- ( ph -> M e. NN )
fourierdlem34.q
|- ( ph -> Q e. ( P ` M ) )
Assertion fourierdlem34
|- ( ph -> Q : ( 0 ... M ) -1-1-> RR )

Proof

Step Hyp Ref Expression
1 fourierdlem34.p
 |-  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 fourierdlem34.m
 |-  ( ph -> M e. NN )
3 fourierdlem34.q
 |-  ( ph -> Q e. ( P ` M ) )
4 1 fourierdlem2
 |-  ( 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 ) ) ) ) ) )
5 2 4 syl
 |-  ( ph -> ( 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 ) ) ) ) ) )
6 3 5 mpbid
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7 6 simpld
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
8 elmapi
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
9 7 8 syl
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
10 simplr
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` i ) = ( Q ` j ) ) /\ -. i = j ) -> ( Q ` i ) = ( Q ` j ) )
11 9 ffvelrnda
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
12 11 ad2antrr
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( Q ` i ) e. RR )
13 9 ffvelrnda
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( Q ` k ) e. RR )
14 13 ad4ant14
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < j ) /\ k e. ( 0 ... M ) ) -> ( Q ` k ) e. RR )
15 14 adantllr
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ k e. ( 0 ... M ) ) -> ( Q ` k ) e. RR )
16 eleq1w
 |-  ( i = k -> ( i e. ( 0 ..^ M ) <-> k e. ( 0 ..^ M ) ) )
17 16 anbi2d
 |-  ( i = k -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ k e. ( 0 ..^ M ) ) ) )
18 fveq2
 |-  ( i = k -> ( Q ` i ) = ( Q ` k ) )
19 oveq1
 |-  ( i = k -> ( i + 1 ) = ( k + 1 ) )
20 19 fveq2d
 |-  ( i = k -> ( Q ` ( i + 1 ) ) = ( Q ` ( k + 1 ) ) )
21 18 20 breq12d
 |-  ( i = k -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` k ) < ( Q ` ( k + 1 ) ) ) )
22 17 21 imbi12d
 |-  ( i = k -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( Q ` k ) < ( Q ` ( k + 1 ) ) ) ) )
23 6 simprrd
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
24 23 r19.21bi
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
25 22 24 chvarvv
 |-  ( ( ph /\ k e. ( 0 ..^ M ) ) -> ( Q ` k ) < ( Q ` ( k + 1 ) ) )
26 25 ad4ant14
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < j ) /\ k e. ( 0 ..^ M ) ) -> ( Q ` k ) < ( Q ` ( k + 1 ) ) )
27 26 adantllr
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ k e. ( 0 ..^ M ) ) -> ( Q ` k ) < ( Q ` ( k + 1 ) ) )
28 simpllr
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> i e. ( 0 ... M ) )
29 simplr
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> j e. ( 0 ... M ) )
30 simpr
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> i < j )
31 15 27 28 29 30 monoords
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( Q ` i ) < ( Q ` j ) )
32 12 31 ltned
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( Q ` i ) =/= ( Q ` j ) )
33 32 neneqd
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> -. ( Q ` i ) = ( Q ` j ) )
34 33 adantlr
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ -. i = j ) /\ i < j ) -> -. ( Q ` i ) = ( Q ` j ) )
35 simpll
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ -. i = j ) /\ -. i < j ) -> ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) )
36 elfzelz
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
37 36 zred
 |-  ( j e. ( 0 ... M ) -> j e. RR )
38 37 ad3antlr
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ -. i = j ) /\ -. i < j ) -> j e. RR )
39 elfzelz
 |-  ( i e. ( 0 ... M ) -> i e. ZZ )
40 39 zred
 |-  ( i e. ( 0 ... M ) -> i e. RR )
41 40 ad4antlr
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ -. i = j ) /\ -. i < j ) -> i e. RR )
42 neqne
 |-  ( -. i = j -> i =/= j )
43 42 necomd
 |-  ( -. i = j -> j =/= i )
44 43 ad2antlr
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ -. i = j ) /\ -. i < j ) -> j =/= i )
45 simpr
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ -. i = j ) /\ -. i < j ) -> -. i < j )
46 38 41 44 45 lttri5d
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ -. i = j ) /\ -. i < j ) -> j < i )
47 9 ffvelrnda
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
48 47 adantr
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ j < i ) -> ( Q ` j ) e. RR )
49 48 adantllr
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) -> ( Q ` j ) e. RR )
50 simp-4l
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) /\ k e. ( 0 ... M ) ) -> ph )
51 50 13 sylancom
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) /\ k e. ( 0 ... M ) ) -> ( Q ` k ) e. RR )
52 simp-4l
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) /\ k e. ( 0 ..^ M ) ) -> ph )
53 52 25 sylancom
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) /\ k e. ( 0 ..^ M ) ) -> ( Q ` k ) < ( Q ` ( k + 1 ) ) )
54 simplr
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) -> j e. ( 0 ... M ) )
55 simpllr
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) -> i e. ( 0 ... M ) )
56 simpr
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) -> j < i )
57 51 53 54 55 56 monoords
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) -> ( Q ` j ) < ( Q ` i ) )
58 49 57 gtned
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) -> ( Q ` i ) =/= ( Q ` j ) )
59 58 neneqd
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ j < i ) -> -. ( Q ` i ) = ( Q ` j ) )
60 35 46 59 syl2anc
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ -. i = j ) /\ -. i < j ) -> -. ( Q ` i ) = ( Q ` j ) )
61 34 60 pm2.61dan
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ -. i = j ) -> -. ( Q ` i ) = ( Q ` j ) )
62 61 adantlr
 |-  ( ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` i ) = ( Q ` j ) ) /\ -. i = j ) -> -. ( Q ` i ) = ( Q ` j ) )
63 10 62 condan
 |-  ( ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` i ) = ( Q ` j ) ) -> i = j )
64 63 ex
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... M ) ) -> ( ( Q ` i ) = ( Q ` j ) -> i = j ) )
65 64 ralrimiva
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> A. j e. ( 0 ... M ) ( ( Q ` i ) = ( Q ` j ) -> i = j ) )
66 65 ralrimiva
 |-  ( ph -> A. i e. ( 0 ... M ) A. j e. ( 0 ... M ) ( ( Q ` i ) = ( Q ` j ) -> i = j ) )
67 dff13
 |-  ( Q : ( 0 ... M ) -1-1-> RR <-> ( Q : ( 0 ... M ) --> RR /\ A. i e. ( 0 ... M ) A. j e. ( 0 ... M ) ( ( Q ` i ) = ( Q ` j ) -> i = j ) ) )
68 9 66 67 sylanbrc
 |-  ( ph -> Q : ( 0 ... M ) -1-1-> RR )