This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem36

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

Ref Expression
Hypotheses fourierdlem36.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fourierdlem36.assr ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
fourierdlem36.f ⊢ 𝐹 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) )
fourierdlem36.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐴 ) − 1 )
Assertion fourierdlem36 ( 𝜑 → 𝐹 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem36.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fourierdlem36.assr ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 fourierdlem36.f ⊢ 𝐹 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) )
4 fourierdlem36.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐴 ) − 1 )
5 ltso ⊢ < Or ℝ
6 soss ⊢ ( 𝐴 ⊆ ℝ → ( < Or ℝ → < Or 𝐴 ) )
7 2 5 6 mpisyl ⊢ ( 𝜑 → < Or 𝐴 )
8 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
9 eqid ⊢ ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) ) = ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) )
10 1 7 8 9 fzisoeu ⊢ ( 𝜑 → ∃! 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) ) ) , 𝐴 ) )
11 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
12 1 11 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
13 12 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℂ )
14 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
15 13 14 negsubd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) + - 1 ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
16 df-neg ⊢ - 1 = ( 0 − 1 )
17 16 eqcomi ⊢ ( 0 − 1 ) = - 1
18 17 oveq2i ⊢ ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) ) = ( ( ♯ ‘ 𝐴 ) + - 1 )
19 15 18 4 3eqtr4g ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) ) = 𝑁 )
20 19 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) ) ) = ( 0 ... 𝑁 ) )
21 isoeq4 ⊢ ( ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) ) ) = ( 0 ... 𝑁 ) → ( 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) ) ) , 𝐴 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) ) )
22 20 21 syl ⊢ ( 𝜑 → ( 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) ) ) , 𝐴 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) ) )
23 22 eubidv ⊢ ( 𝜑 → ( ∃! 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( 0 − 1 ) ) ) , 𝐴 ) ↔ ∃! 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) ) )
24 10 23 mpbid ⊢ ( 𝜑 → ∃! 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) )
25 iotacl ⊢ ( ∃! 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) → ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) ) ∈ { 𝑓 ∣ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) } )
26 24 25 syl ⊢ ( 𝜑 → ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) ) ∈ { 𝑓 ∣ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) } )
27 3 26 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ { 𝑓 ∣ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) } )
28 iotaex ⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) ) ∈ V
29 3 28 eqeltri ⊢ 𝐹 ∈ V
30 isoeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) ↔ 𝐹 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) ) )
31 29 30 elab ⊢ ( 𝐹 ∈ { 𝑓 ∣ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) } ↔ 𝐹 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) )
32 27 31 sylib ⊢ ( 𝜑 → 𝐹 Isom < , < ( ( 0 ... 𝑁 ) , 𝐴 ) )