vdwpc

Description: The predicate " The coloring F contains a polychromatic M -tuple of AP's of length K ". A polychromatic M -tuple of AP's is a set of AP's with the same base point but different step lengths, such that each individual AP is monochromatic, but the AP's all have mutually distinct colors. (The common basepoint is not required to have the same color as any of the AP's.) (Contributed by Mario Carneiro, 18-Aug-2014)

	Ref	Expression
Hypotheses	vdwmc.1	$⊢ X \in V$
	vdwmc.2	$⊢ φ \to K \in ℕ_{0}$
	vdwmc.3	$⊢ φ \to F : X ⟶ R$
	vdwpc.4	$⊢ φ \to M \in ℕ$
	vdwpc.5	$⊢ J = (1 \dots M)$
Assertion	vdwpc	$⊢ φ \to (⟨M, K⟩ PolyAP F \leftrightarrow \exists a \in ℕ \exists d \in (ℕ^{J}) (\forall i \in J (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in J ⟼ F (a + d (i)))\| = M))$

Proof

Step	Hyp	Ref	Expression
1		vdwmc.1	$⊢ X \in V$
2		vdwmc.2	$⊢ φ \to K \in ℕ_{0}$
3		vdwmc.3	$⊢ φ \to F : X ⟶ R$
4		vdwpc.4	$⊢ φ \to M \in ℕ$
5		vdwpc.5	$⊢ J = (1 \dots M)$
6		fex	$⊢ (F : X ⟶ R \land X \in V) \to F \in V$
7	3 1 6	sylancl	$⊢ φ \to F \in V$
8		df-br	$⊢ ⟨M, K⟩ PolyAP F \leftrightarrow ⟨⟨M, K⟩, F⟩ \in PolyAP$
9		df-vdwpc	$⊢ PolyAP = \{⟨⟨m, k⟩, f⟩ \| \exists a \in ℕ \exists d \in (ℕ^{(1 \dots m)}) (\forall i \in (1 \dots m) (a + d (i)) AP (k) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots m) ⟼ f (a + d (i)))\| = m)\}$
10	9	eleq2i	$⊢ ⟨⟨M, K⟩, F⟩ \in PolyAP \leftrightarrow ⟨⟨M, K⟩, F⟩ \in \{⟨⟨m, k⟩, f⟩ \| \exists a \in ℕ \exists d \in (ℕ^{(1 \dots m)}) (\forall i \in (1 \dots m) (a + d (i)) AP (k) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots m) ⟼ f (a + d (i)))\| = m)\}$
11	8 10	bitri	$⊢ ⟨M, K⟩ PolyAP F \leftrightarrow ⟨⟨M, K⟩, F⟩ \in \{⟨⟨m, k⟩, f⟩ \| \exists a \in ℕ \exists d \in (ℕ^{(1 \dots m)}) (\forall i \in (1 \dots m) (a + d (i)) AP (k) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots m) ⟼ f (a + d (i)))\| = m)\}$
12		simp1	$⊢ (m = M \land k = K \land f = F) \to m = M$
13	12	oveq2d	$⊢ (m = M \land k = K \land f = F) \to (1 \dots m) = (1 \dots M)$
14	13 5	eqtr4di	$⊢ (m = M \land k = K \land f = F) \to (1 \dots m) = J$
15	14	oveq2d	$⊢ (m = M \land k = K \land f = F) \to ℕ^{(1 \dots m)} = ℕ^{J}$
16		simp2	$⊢ (m = M \land k = K \land f = F) \to k = K$
17	16	fveq2d	$⊢ (m = M \land k = K \land f = F) \to AP (k) = AP (K)$
18	17	oveqd	$⊢ (m = M \land k = K \land f = F) \to (a + d (i)) AP (k) d (i) = (a + d (i)) AP (K) d (i)$
19		simp3	$⊢ (m = M \land k = K \land f = F) \to f = F$
20	19	cnveqd	$⊢ (m = M \land k = K \land f = F) \to f^{-1} = F^{-1}$
21	19	fveq1d	$⊢ (m = M \land k = K \land f = F) \to f (a + d (i)) = F (a + d (i))$
22	21	sneqd	$⊢ (m = M \land k = K \land f = F) \to \{f (a + d (i))\} = \{F (a + d (i))\}$
23	20 22	imaeq12d	$⊢ (m = M \land k = K \land f = F) \to f^{-1} [\{f (a + d (i))\}] = F^{-1} [\{F (a + d (i))\}]$
24	18 23	sseq12d	$⊢ (m = M \land k = K \land f = F) \to ((a + d (i)) AP (k) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \leftrightarrow (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}])$
25	14 24	raleqbidv	$⊢ (m = M \land k = K \land f = F) \to (\forall i \in (1 \dots m) (a + d (i)) AP (k) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \leftrightarrow \forall i \in J (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}])$
26	14 21	mpteq12dv	$⊢ (m = M \land k = K \land f = F) \to (i \in (1 \dots m) ⟼ f (a + d (i))) = (i \in J ⟼ F (a + d (i)))$
27	26	rneqd	$⊢ (m = M \land k = K \land f = F) \to ran (i \in (1 \dots m) ⟼ f (a + d (i))) = ran (i \in J ⟼ F (a + d (i)))$
28	27	fveq2d	$⊢ (m = M \land k = K \land f = F) \to \|ran (i \in (1 \dots m) ⟼ f (a + d (i)))\| = \|ran (i \in J ⟼ F (a + d (i)))\|$
29	28 12	eqeq12d	$⊢ (m = M \land k = K \land f = F) \to (\|ran (i \in (1 \dots m) ⟼ f (a + d (i)))\| = m \leftrightarrow \|ran (i \in J ⟼ F (a + d (i)))\| = M)$
30	25 29	anbi12d	$⊢ (m = M \land k = K \land f = F) \to ((\forall i \in (1 \dots m) (a + d (i)) AP (k) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots m) ⟼ f (a + d (i)))\| = m) \leftrightarrow (\forall i \in J (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in J ⟼ F (a + d (i)))\| = M))$
31	15 30	rexeqbidv	$⊢ (m = M \land k = K \land f = F) \to (\exists d \in (ℕ^{(1 \dots m)}) (\forall i \in (1 \dots m) (a + d (i)) AP (k) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots m) ⟼ f (a + d (i)))\| = m) \leftrightarrow \exists d \in (ℕ^{J}) (\forall i \in J (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in J ⟼ F (a + d (i)))\| = M))$
32	31	rexbidv	$⊢ (m = M \land k = K \land f = F) \to (\exists a \in ℕ \exists d \in (ℕ^{(1 \dots m)}) (\forall i \in (1 \dots m) (a + d (i)) AP (k) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots m) ⟼ f (a + d (i)))\| = m) \leftrightarrow \exists a \in ℕ \exists d \in (ℕ^{J}) (\forall i \in J (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in J ⟼ F (a + d (i)))\| = M))$
33	32	eloprabga	$⊢ (M \in ℕ \land K \in ℕ_{0} \land F \in V) \to (⟨⟨M, K⟩, F⟩ \in \{⟨⟨m, k⟩, f⟩ \| \exists a \in ℕ \exists d \in (ℕ^{(1 \dots m)}) (\forall i \in (1 \dots m) (a + d (i)) AP (k) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots m) ⟼ f (a + d (i)))\| = m)\} \leftrightarrow \exists a \in ℕ \exists d \in (ℕ^{J}) (\forall i \in J (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in J ⟼ F (a + d (i)))\| = M))$
34	11 33	bitrid	$⊢ (M \in ℕ \land K \in ℕ_{0} \land F \in V) \to (⟨M, K⟩ PolyAP F \leftrightarrow \exists a \in ℕ \exists d \in (ℕ^{J}) (\forall i \in J (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in J ⟼ F (a + d (i)))\| = M))$
35	4 2 7 34	syl3anc	$⊢ φ \to (⟨M, K⟩ PolyAP F \leftrightarrow \exists a \in ℕ \exists d \in (ℕ^{J}) (\forall i \in J (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in J ⟼ F (a + d (i)))\| = M))$

Metamath Proof Explorer

Theorem vdwpc

Proof