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 → ( ♯ ‘ 𝐴 ) ∈ ℕ₀ )
12	1 11	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ₀ )
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 ... 𝑁 ) , 𝐴 ) )

Metamath Proof Explorer

Theorem fourierdlem36

Proof