Metamath Proof Explorer

Theorem fourierdlem52

Description: d16:d17,d18:jca |- ( ph -> ( ( S 0 ) <_ A /\ A <_ ( S 0 ) ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem52.tf 
|- ( ph -> T e. Fin )
fourierdlem52.n 
|- N = ( ( # ` T ) - 1 )
fourierdlem52.s 
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
fourierdlem52.a 
|- ( ph -> A e. RR )
fourierdlem52.b 
|- ( ph -> B e. RR )
fourierdlem52.t 
|- ( ph -> T C_ ( A [,] B ) )
fourierdlem52.at 
|- ( ph -> A e. T )
fourierdlem52.bt 
|- ( ph -> B e. T )
Assertion fourierdlem52 
|- ( ph -> ( ( S : ( 0 ... N ) --> ( A [,] B ) /\ ( S ` 0 ) = A ) /\ ( S ` N ) = B ) )

Proof

Step Hyp Ref Expression
1 fourierdlem52.tf 
 |-  ( ph -> T e. Fin )
2 fourierdlem52.n 
 |-  N = ( ( # ` T ) - 1 )
3 fourierdlem52.s 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
4 fourierdlem52.a 
 |-  ( ph -> A e. RR )
5 fourierdlem52.b 
 |-  ( ph -> B e. RR )
6 fourierdlem52.t 
 |-  ( ph -> T C_ ( A [,] B ) )
7 fourierdlem52.at 
 |-  ( ph -> A e. T )
8 fourierdlem52.bt 
 |-  ( ph -> B e. T )
9 4 5 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
10 6 9 sstrd 
 |-  ( ph -> T C_ RR )
11 1 10 3 2 fourierdlem36 
 |-  ( ph -> S Isom < , < ( ( 0 ... N ) , T ) )
12 isof1o 
 |-  ( S Isom < , < ( ( 0 ... N ) , T ) -> S : ( 0 ... N ) -1-1-onto-> T )
13 f1of 
 |-  ( S : ( 0 ... N ) -1-1-onto-> T -> S : ( 0 ... N ) --> T )
14 11 12 13 3syl 
 |-  ( ph -> S : ( 0 ... N ) --> T )
15 14 6 fssd 
 |-  ( ph -> S : ( 0 ... N ) --> ( A [,] B ) )
16 f1ofo 
 |-  ( S : ( 0 ... N ) -1-1-onto-> T -> S : ( 0 ... N ) -onto-> T )
17 11 12 16 3syl 
 |-  ( ph -> S : ( 0 ... N ) -onto-> T )
18 foelrn 
 |-  ( ( S : ( 0 ... N ) -onto-> T /\ A e. T ) -> E. j e. ( 0 ... N ) A = ( S ` j ) )
19 17 7 18 syl2anc 
 |-  ( ph -> E. j e. ( 0 ... N ) A = ( S ` j ) )
20 elfzle1 
 |-  ( j e. ( 0 ... N ) -> 0 <_ j )
21 20 adantl 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> 0 <_ j )
22 11 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> S Isom < , < ( ( 0 ... N ) , T ) )
23 ressxr 
 |-  RR C_ RR*
24 10 23 sstrdi 
 |-  ( ph -> T C_ RR* )
25 24 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> T C_ RR* )
26 fzssz 
 |-  ( 0 ... N ) C_ ZZ
27 zssre 
 |-  ZZ C_ RR
28 27 23 sstri 
 |-  ZZ C_ RR*
29 26 28 sstri 
 |-  ( 0 ... N ) C_ RR*
30 25 29 jctil 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( 0 ... N ) C_ RR* /\ T C_ RR* ) )
31 hashcl 
 |-  ( T e. Fin -> ( # ` T ) e. NN0 )
32 1 31 syl 
 |-  ( ph -> ( # ` T ) e. NN0 )
33 7 ne0d 
 |-  ( ph -> T =/= (/) )
34 hashge1 
 |-  ( ( T e. Fin /\ T =/= (/) ) -> 1 <_ ( # ` T ) )
35 1 33 34 syl2anc 
 |-  ( ph -> 1 <_ ( # ` T ) )
36 elnnnn0c 
 |-  ( ( # ` T ) e. NN <-> ( ( # ` T ) e. NN0 /\ 1 <_ ( # ` T ) ) )
37 32 35 36 sylanbrc 
 |-  ( ph -> ( # ` T ) e. NN )
38 nnm1nn0 
 |-  ( ( # ` T ) e. NN -> ( ( # ` T ) - 1 ) e. NN0 )
39 37 38 syl 
 |-  ( ph -> ( ( # ` T ) - 1 ) e. NN0 )
40 2 39 eqeltrid 
 |-  ( ph -> N e. NN0 )
41 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
42 40 41 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
43 eluzfz1 
 |-  ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) )
44 42 43 syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
45 44 anim1i 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( 0 e. ( 0 ... N ) /\ j e. ( 0 ... N ) ) )
46 leisorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , T ) /\ ( ( 0 ... N ) C_ RR* /\ T C_ RR* ) /\ ( 0 e. ( 0 ... N ) /\ j e. ( 0 ... N ) ) ) -> ( 0 <_ j <-> ( S ` 0 ) <_ ( S ` j ) ) )
47 22 30 45 46 syl3anc 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( 0 <_ j <-> ( S ` 0 ) <_ ( S ` j ) ) )
48 21 47 mpbid 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( S ` 0 ) <_ ( S ` j ) )
49 48 3adant3 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ A = ( S ` j ) ) -> ( S ` 0 ) <_ ( S ` j ) )
50 eqcom 
 |-  ( A = ( S ` j ) <-> ( S ` j ) = A )
51 50 biimpi 
 |-  ( A = ( S ` j ) -> ( S ` j ) = A )
52 51 3ad2ant3 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ A = ( S ` j ) ) -> ( S ` j ) = A )
53 49 52 breqtrd 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ A = ( S ` j ) ) -> ( S ` 0 ) <_ A )
54 53 rexlimdv3a 
 |-  ( ph -> ( E. j e. ( 0 ... N ) A = ( S ` j ) -> ( S ` 0 ) <_ A ) )
55 19 54 mpd 
 |-  ( ph -> ( S ` 0 ) <_ A )
56 4 rexrd 
 |-  ( ph -> A e. RR* )
57 5 rexrd 
 |-  ( ph -> B e. RR* )
58 15 44 ffvelcdmd 
 |-  ( ph -> ( S ` 0 ) e. ( A [,] B ) )
59 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( S ` 0 ) e. ( A [,] B ) ) -> A <_ ( S ` 0 ) )
60 56 57 58 59 syl3anc 
 |-  ( ph -> A <_ ( S ` 0 ) )
61 9 58 sseldd 
 |-  ( ph -> ( S ` 0 ) e. RR )
62 61 4 letri3d 
 |-  ( ph -> ( ( S ` 0 ) = A <-> ( ( S ` 0 ) <_ A /\ A <_ ( S ` 0 ) ) ) )
63 55 60 62 mpbir2and 
 |-  ( ph -> ( S ` 0 ) = A )
64 eluzfz2 
 |-  ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
65 42 64 syl 
 |-  ( ph -> N e. ( 0 ... N ) )
66 15 65 ffvelcdmd 
 |-  ( ph -> ( S ` N ) e. ( A [,] B ) )
67 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( S ` N ) e. ( A [,] B ) ) -> ( S ` N ) <_ B )
68 56 57 66 67 syl3anc 
 |-  ( ph -> ( S ` N ) <_ B )
69 foelrn 
 |-  ( ( S : ( 0 ... N ) -onto-> T /\ B e. T ) -> E. j e. ( 0 ... N ) B = ( S ` j ) )
70 17 8 69 syl2anc 
 |-  ( ph -> E. j e. ( 0 ... N ) B = ( S ` j ) )
71 simp3 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ B = ( S ` j ) ) -> B = ( S ` j ) )
72 elfzle2 
 |-  ( j e. ( 0 ... N ) -> j <_ N )
73 72 3ad2ant2 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ B = ( S ` j ) ) -> j <_ N )
74 11 3ad2ant1 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ B = ( S ` j ) ) -> S Isom < , < ( ( 0 ... N ) , T ) )
75 30 3adant3 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ B = ( S ` j ) ) -> ( ( 0 ... N ) C_ RR* /\ T C_ RR* ) )
76 simp2 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ B = ( S ` j ) ) -> j e. ( 0 ... N ) )
77 65 3ad2ant1 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ B = ( S ` j ) ) -> N e. ( 0 ... N ) )
78 leisorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , T ) /\ ( ( 0 ... N ) C_ RR* /\ T C_ RR* ) /\ ( j e. ( 0 ... N ) /\ N e. ( 0 ... N ) ) ) -> ( j <_ N <-> ( S ` j ) <_ ( S ` N ) ) )
79 74 75 76 77 78 syl112anc 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ B = ( S ` j ) ) -> ( j <_ N <-> ( S ` j ) <_ ( S ` N ) ) )
80 73 79 mpbid 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ B = ( S ` j ) ) -> ( S ` j ) <_ ( S ` N ) )
81 71 80 eqbrtrd 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ B = ( S ` j ) ) -> B <_ ( S ` N ) )
82 81 rexlimdv3a 
 |-  ( ph -> ( E. j e. ( 0 ... N ) B = ( S ` j ) -> B <_ ( S ` N ) ) )
83 70 82 mpd 
 |-  ( ph -> B <_ ( S ` N ) )
84 9 66 sseldd 
 |-  ( ph -> ( S ` N ) e. RR )
85 84 5 letri3d 
 |-  ( ph -> ( ( S ` N ) = B <-> ( ( S ` N ) <_ B /\ B <_ ( S ` N ) ) ) )
86 68 83 85 mpbir2and 
 |-  ( ph -> ( S ` N ) = B )
87 15 63 86 jca31 
 |-  ( ph -> ( ( S : ( 0 ... N ) --> ( A [,] B ) /\ ( S ` 0 ) = A ) /\ ( S ` N ) = B ) )