Metamath Proof Explorer

Theorem fourierdlem34

Description: A partition is one to one. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem34.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem34.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem34.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
Assertion fourierdlem34 ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) –1-1→ ℝ )

Proof

Step Hyp Ref Expression
1 fourierdlem34.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem34.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 fourierdlem34.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
4 1 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
5 2 4 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
6 3 5 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
7 6 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
8 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
9 7 8 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
10 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) ) ∧ ¬ 𝑖 = 𝑗 ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) )
11 9 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
12 11 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
13 9 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑘 ) ∈ ℝ )
14 13 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑘 ) ∈ ℝ )
15 14 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑘 ) ∈ ℝ )
16 eleq1w ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
17 16 anbi2d ⊢ ( 𝑖 = 𝑘 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ) )
18 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑘 ) )
19 oveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 + 1 ) = ( 𝑘 + 1 ) )
20 19 fveq2d ⊢ ( 𝑖 = 𝑘 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) )
21 18 20 breq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ 𝑘 ) < ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
22 17 21 imbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑘 ) < ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) )
23 6 simprrd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
24 23 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
25 22 24 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑘 ) < ( 𝑄 ‘ ( 𝑘 + 1 ) ) )
26 25 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑘 ) < ( 𝑄 ‘ ( 𝑘 + 1 ) ) )
27 26 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑘 ) < ( 𝑄 ‘ ( 𝑘 + 1 ) ) )
28 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
29 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
30 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑖 < 𝑗 )
31 15 27 28 29 30 monoords ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ 𝑗 ) )
32 12 31 ltned ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ 𝑖 ) ≠ ( 𝑄 ‘ 𝑗 ) )
33 32 neneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) )
34 33 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑗 ) ∧ 𝑖 < 𝑗 ) → ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) )
35 simpll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑗 ) ∧ ¬ 𝑖 < 𝑗 ) → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) )
36 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
37 36 zred ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℝ )
38 37 ad3antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑗 ) ∧ ¬ 𝑖 < 𝑗 ) → 𝑗 ∈ ℝ )
39 elfzelz ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑖 ∈ ℤ )
40 39 zred ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑖 ∈ ℝ )
41 40 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑗 ) ∧ ¬ 𝑖 < 𝑗 ) → 𝑖 ∈ ℝ )
42 neqne ⊢ ( ¬ 𝑖 = 𝑗 → 𝑖 ≠ 𝑗 )
43 42 necomd ⊢ ( ¬ 𝑖 = 𝑗 → 𝑗 ≠ 𝑖 )
44 43 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑗 ) ∧ ¬ 𝑖 < 𝑗 ) → 𝑗 ≠ 𝑖 )
45 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑗 ) ∧ ¬ 𝑖 < 𝑗 ) → ¬ 𝑖 < 𝑗 )
46 38 41 44 45 lttri5d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑗 ) ∧ ¬ 𝑖 < 𝑗 ) → 𝑗 < 𝑖 )
47 9 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
49 48 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
50 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝜑 )
51 50 13 sylancom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑘 ) ∈ ℝ )
52 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → 𝜑 )
53 52 25 sylancom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑘 ) < ( 𝑄 ‘ ( 𝑘 + 1 ) ) )
54 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
55 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
56 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) → 𝑗 < 𝑖 )
57 51 53 54 55 56 monoords ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) → ( 𝑄 ‘ 𝑗 ) < ( 𝑄 ‘ 𝑖 ) )
58 49 57 gtned ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) → ( 𝑄 ‘ 𝑖 ) ≠ ( 𝑄 ‘ 𝑗 ) )
59 58 neneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 < 𝑖 ) → ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) )
60 35 46 59 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑗 ) ∧ ¬ 𝑖 < 𝑗 ) → ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) )
61 34 60 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 = 𝑗 ) → ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) )
62 61 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) ) ∧ ¬ 𝑖 = 𝑗 ) → ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) )
63 10 62 condan ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) ) → 𝑖 = 𝑗 )
64 63 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
65 64 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
66 65 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
67 dff13 ⊢ ( 𝑄 : ( 0 ... 𝑀 ) –1-1→ ℝ ↔ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
68 9 66 67 sylanbrc ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) –1-1→ ℝ )