fourierdlem3

Description: Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	fourierdlem3.1	$⊢ P = (m \in ℕ ⟼ \{p \in ({[- π, π]}^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	Assertion	fourierdlem3	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in ({[- π, π]}^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem3.1	$⊢ P = (m \in ℕ ⟼ \{p \in ({[- π, π]}^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
2		oveq2	$⊢ m = M \to (0 \dots m) = (0 \dots M)$
3	2	oveq2d	$⊢ m = M \to {[- π, π]}^{(0 \dots m)} = {[- π, π]}^{(0 \dots M)}$
4		fveqeq2	$⊢ m = M \to (p (m) = π \leftrightarrow p (M) = π)$
5	4	anbi2d	$⊢ m = M \to ((p (0) = - π \land p (m) = π) \leftrightarrow (p (0) = - π \land p (M) = π))$
6		oveq2	$⊢ m = M \to (0 ..^m) = (0 ..^M)$
7	6	raleqdv	$⊢ m = M \to (\forall i \in (0 ..^m) p (i) < p (i + 1) \leftrightarrow \forall i \in (0 ..^M) p (i) < p (i + 1))$
8	5 7	anbi12d	$⊢ m = M \to (((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1)) \leftrightarrow ((p (0) = - π \land p (M) = π) \land \forall i \in (0 ..^M) p (i) < p (i + 1)))$
9	3 8	rabeqbidv	$⊢ m = M \to \{p \in ({[- π, π]}^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\} = \{p \in ({[- π, π]}^{(0 \dots M)}) \| ((p (0) = - π \land p (M) = π) \land \forall i \in (0 ..^M) p (i) < p (i + 1))\}$
10		ovex	$⊢ {[- π, π]}^{(0 \dots M)} \in V$
11	10	rabex	$⊢ \{p \in ({[- π, π]}^{(0 \dots M)}) \| ((p (0) = - π \land p (M) = π) \land \forall i \in (0 ..^M) p (i) < p (i + 1))\} \in V$
12	9 1 11	fvmpt	$⊢ M \in ℕ \to P (M) = \{p \in ({[- π, π]}^{(0 \dots M)}) \| ((p (0) = - π \land p (M) = π) \land \forall i \in (0 ..^M) p (i) < p (i + 1))\}$
13	12	eleq2d	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow Q \in \{p \in ({[- π, π]}^{(0 \dots M)}) \| ((p (0) = - π \land p (M) = π) \land \forall i \in (0 ..^M) p (i) < p (i + 1))\})$
14		fveq1	$⊢ p = Q \to p (0) = Q (0)$
15	14	eqeq1d	$⊢ p = Q \to (p (0) = - π \leftrightarrow Q (0) = - π)$
16		fveq1	$⊢ p = Q \to p (M) = Q (M)$
17	16	eqeq1d	$⊢ p = Q \to (p (M) = π \leftrightarrow Q (M) = π)$
18	15 17	anbi12d	$⊢ p = Q \to ((p (0) = - π \land p (M) = π) \leftrightarrow (Q (0) = - π \land Q (M) = π))$
19		fveq1	$⊢ p = Q \to p (i) = Q (i)$
20		fveq1	$⊢ p = Q \to p (i + 1) = Q (i + 1)$
21	19 20	breq12d	$⊢ p = Q \to (p (i) < p (i + 1) \leftrightarrow Q (i) < Q (i + 1))$
22	21	ralbidv	$⊢ p = Q \to (\forall i \in (0 ..^M) p (i) < p (i + 1) \leftrightarrow \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
23	18 22	anbi12d	$⊢ p = Q \to (((p (0) = - π \land p (M) = π) \land \forall i \in (0 ..^M) p (i) < p (i + 1)) \leftrightarrow ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
24	23	elrab	$⊢ Q \in \{p \in ({[- π, π]}^{(0 \dots M)}) \| ((p (0) = - π \land p (M) = π) \land \forall i \in (0 ..^M) p (i) < p (i + 1))\} \leftrightarrow (Q \in ({[- π, π]}^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
25	13 24	bitrdi	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in ({[- π, π]}^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$

Metamath Proof Explorer

Theorem fourierdlem3

Proof