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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 )