Metamath Proof Explorer

Theorem fourierdlem36

Description: F is an isomorphism. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem36.a 
|- ( ph -> A e. Fin )
fourierdlem36.assr 
|- ( ph -> A C_ RR )
fourierdlem36.f 
|- F = ( iota f f Isom < , < ( ( 0 ... N ) , A ) )
fourierdlem36.n 
|- N = ( ( # ` A ) - 1 )
Assertion fourierdlem36 
|- ( ph -> F Isom < , < ( ( 0 ... N ) , A ) )

Proof

Step Hyp Ref Expression
1 fourierdlem36.a 
 |-  ( ph -> A e. Fin )
2 fourierdlem36.assr 
 |-  ( ph -> A C_ RR )
3 fourierdlem36.f 
 |-  F = ( iota f f Isom < , < ( ( 0 ... N ) , A ) )
4 fourierdlem36.n 
 |-  N = ( ( # ` A ) - 1 )
5 ltso 
 |-  < Or RR
6 soss 
 |-  ( A C_ RR -> ( < Or RR -> < Or A ) )
7 2 5 6 mpisyl 
 |-  ( ph -> < Or A )
8 0zd 
 |-  ( ph -> 0 e. ZZ )
9 eqid 
 |-  ( ( # ` A ) + ( 0 - 1 ) ) = ( ( # ` A ) + ( 0 - 1 ) )
10 1 7 8 9 fzisoeu 
 |-  ( ph -> E! f f Isom < , < ( ( 0 ... ( ( # ` A ) + ( 0 - 1 ) ) ) , A ) )
11 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
12 1 11 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
13 12 nn0cnd 
 |-  ( ph -> ( # ` A ) e. CC )
14 1cnd 
 |-  ( ph -> 1 e. CC )
15 13 14 negsubd 
 |-  ( ph -> ( ( # ` A ) + -u 1 ) = ( ( # ` A ) - 1 ) )
16 df-neg 
 |-  -u 1 = ( 0 - 1 )
17 16 eqcomi 
 |-  ( 0 - 1 ) = -u 1
18 17 oveq2i 
 |-  ( ( # ` A ) + ( 0 - 1 ) ) = ( ( # ` A ) + -u 1 )
19 15 18 4 3eqtr4g 
 |-  ( ph -> ( ( # ` A ) + ( 0 - 1 ) ) = N )
20 19 oveq2d 
 |-  ( ph -> ( 0 ... ( ( # ` A ) + ( 0 - 1 ) ) ) = ( 0 ... N ) )
21 isoeq4 
 |-  ( ( 0 ... ( ( # ` A ) + ( 0 - 1 ) ) ) = ( 0 ... N ) -> ( f Isom < , < ( ( 0 ... ( ( # ` A ) + ( 0 - 1 ) ) ) , A ) <-> f Isom < , < ( ( 0 ... N ) , A ) ) )
22 20 21 syl 
 |-  ( ph -> ( f Isom < , < ( ( 0 ... ( ( # ` A ) + ( 0 - 1 ) ) ) , A ) <-> f Isom < , < ( ( 0 ... N ) , A ) ) )
23 22 eubidv 
 |-  ( ph -> ( E! f f Isom < , < ( ( 0 ... ( ( # ` A ) + ( 0 - 1 ) ) ) , A ) <-> E! f f Isom < , < ( ( 0 ... N ) , A ) ) )
24 10 23 mpbid 
 |-  ( ph -> E! f f Isom < , < ( ( 0 ... N ) , A ) )
25 iotacl 
 |-  ( E! f f Isom < , < ( ( 0 ... N ) , A ) -> ( iota f f Isom < , < ( ( 0 ... N ) , A ) ) e. { f | f Isom < , < ( ( 0 ... N ) , A ) } )
26 24 25 syl 
 |-  ( ph -> ( iota f f Isom < , < ( ( 0 ... N ) , A ) ) e. { f | f Isom < , < ( ( 0 ... N ) , A ) } )
27 3 26 eqeltrid 
 |-  ( ph -> F e. { f | f Isom < , < ( ( 0 ... N ) , A ) } )
28 iotaex 
 |-  ( iota f f Isom < , < ( ( 0 ... N ) , A ) ) e. _V
29 3 28 eqeltri 
 |-  F e. _V
30 isoeq1 
 |-  ( f = F -> ( f Isom < , < ( ( 0 ... N ) , A ) <-> F Isom < , < ( ( 0 ... N ) , A ) ) )
31 29 30 elab 
 |-  ( F e. { f | f Isom < , < ( ( 0 ... N ) , A ) } <-> F Isom < , < ( ( 0 ... N ) , A ) )
32 27 31 sylib 
 |-  ( ph -> F Isom < , < ( ( 0 ... N ) , A ) )