fourierdlem34

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

	Ref	Expression
Hypotheses	fourierdlem34.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem34.m	$⊢ φ \to M \in ℕ$
	fourierdlem34.q	$⊢ φ \to Q \in P (M)$
Assertion	fourierdlem34	$⊢ φ \to Q : (0 \dots M) \underset{1-1}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem34.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
2		fourierdlem34.m	$⊢ φ \to M \in ℕ$
3		fourierdlem34.q	$⊢ φ \to Q \in P (M)$
4	1	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
5	2 4	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
6	3 5	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
7	6	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
8		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
9	7 8	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
10		simplr	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land Q (i) = Q (j)) \land \neg i = j) \to Q (i) = Q (j)$
11	9	ffvelcdmda	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in ℝ$
12	11	ad2antrr	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land i < j) \to Q (i) \in ℝ$
13	9	ffvelcdmda	$⊢ (φ \land k \in (0 \dots M)) \to Q (k) \in ℝ$
14	13	ad4ant14	$⊢ (((φ \land i \in (0 \dots M)) \land i < j) \land k \in (0 \dots M)) \to Q (k) \in ℝ$
15	14	adantllr	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land i < j) \land k \in (0 \dots M)) \to Q (k) \in ℝ$
16		eleq1w	$⊢ i = k \to (i \in (0 ..^M) \leftrightarrow k \in (0 ..^M))$
17	16	anbi2d	$⊢ i = k \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land k \in (0 ..^M)))$
18		fveq2	$⊢ i = k \to Q (i) = Q (k)$
19		oveq1	$⊢ i = k \to i + 1 = k + 1$
20	19	fveq2d	$⊢ i = k \to Q (i + 1) = Q (k + 1)$
21	18 20	breq12d	$⊢ i = k \to (Q (i) < Q (i + 1) \leftrightarrow Q (k) < Q (k + 1))$
22	17 21	imbi12d	$⊢ i = k \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land k \in (0 ..^M)) \to Q (k) < Q (k + 1)))$
23	6	simprrd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
24	23	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
25	22 24	chvarvv	$⊢ (φ \land k \in (0 ..^M)) \to Q (k) < Q (k + 1)$
26	25	ad4ant14	$⊢ (((φ \land i \in (0 \dots M)) \land i < j) \land k \in (0 ..^M)) \to Q (k) < Q (k + 1)$
27	26	adantllr	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land i < j) \land k \in (0 ..^M)) \to Q (k) < Q (k + 1)$
28		simpllr	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land i < j) \to i \in (0 \dots M)$
29		simplr	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land i < j) \to j \in (0 \dots M)$
30		simpr	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land i < j) \to i < j$
31	15 27 28 29 30	monoords	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land i < j) \to Q (i) < Q (j)$
32	12 31	ltned	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land i < j) \to Q (i) \neq Q (j)$
33	32	neneqd	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land i < j) \to \neg Q (i) = Q (j)$
34	33	adantlr	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land \neg i = j) \land i < j) \to \neg Q (i) = Q (j)$
35		simpll	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land \neg i = j) \land \neg i < j) \to ((φ \land i \in (0 \dots M)) \land j \in (0 \dots M))$
36		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
37	36	zred	$⊢ j \in (0 \dots M) \to j \in ℝ$
38	37	ad3antlr	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land \neg i = j) \land \neg i < j) \to j \in ℝ$
39		elfzelz	$⊢ i \in (0 \dots M) \to i \in ℤ$
40	39	zred	$⊢ i \in (0 \dots M) \to i \in ℝ$
41	40	ad4antlr	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land \neg i = j) \land \neg i < j) \to i \in ℝ$
42		neqne	$⊢ \neg i = j \to i \neq j$
43	42	necomd	$⊢ \neg i = j \to j \neq i$
44	43	ad2antlr	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land \neg i = j) \land \neg i < j) \to j \neq i$
45		simpr	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land \neg i = j) \land \neg i < j) \to \neg i < j$
46	38 41 44 45	lttri5d	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land \neg i = j) \land \neg i < j) \to j < i$
47	9	ffvelcdmda	$⊢ (φ \land j \in (0 \dots M)) \to Q (j) \in ℝ$
48	47	adantr	$⊢ ((φ \land j \in (0 \dots M)) \land j < i) \to Q (j) \in ℝ$
49	48	adantllr	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \to Q (j) \in ℝ$
50		simp-4l	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \land k \in (0 \dots M)) \to φ$
51	50 13	sylancom	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \land k \in (0 \dots M)) \to Q (k) \in ℝ$
52		simp-4l	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \land k \in (0 ..^M)) \to φ$
53	52 25	sylancom	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \land k \in (0 ..^M)) \to Q (k) < Q (k + 1)$
54		simplr	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \to j \in (0 \dots M)$
55		simpllr	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \to i \in (0 \dots M)$
56		simpr	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \to j < i$
57	51 53 54 55 56	monoords	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \to Q (j) < Q (i)$
58	49 57	gtned	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \to Q (i) \neq Q (j)$
59	58	neneqd	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land j < i) \to \neg Q (i) = Q (j)$
60	35 46 59	syl2anc	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land \neg i = j) \land \neg i < j) \to \neg Q (i) = Q (j)$
61	34 60	pm2.61dan	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land \neg i = j) \to \neg Q (i) = Q (j)$
62	61	adantlr	$⊢ ((((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land Q (i) = Q (j)) \land \neg i = j) \to \neg Q (i) = Q (j)$
63	10 62	condan	$⊢ (((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \land Q (i) = Q (j)) \to i = j$
64	63	ex	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots M)) \to (Q (i) = Q (j) \to i = j)$
65	64	ralrimiva	$⊢ (φ \land i \in (0 \dots M)) \to \forall j \in (0 \dots M) (Q (i) = Q (j) \to i = j)$
66	65	ralrimiva	$⊢ φ \to \forall i \in (0 \dots M) \forall j \in (0 \dots M) (Q (i) = Q (j) \to i = j)$
67		dff13	$⊢ Q : (0 \dots M) \underset{1-1}{⟶} ℝ \leftrightarrow (Q : (0 \dots M) ⟶ ℝ \land \forall i \in (0 \dots M) \forall j \in (0 \dots M) (Q (i) = Q (j) \to i = j))$
68	9 66 67	sylanbrc	$⊢ φ \to Q : (0 \dots M) \underset{1-1}{⟶} ℝ$

Metamath Proof Explorer

Theorem fourierdlem34

Proof