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