vdwlem7

	Ref	Expression
Hypotheses	vdwlem3.v	$⊢ φ \to V \in ℕ$
	vdwlem3.w	$⊢ φ \to W \in ℕ$
	vdwlem4.r	$⊢ φ \to R \in Fin$
	vdwlem4.h	$⊢ φ \to H : (1 \dots W 2 V) ⟶ R$
	vdwlem4.f	$⊢ F = (x \in (1 \dots V) ⟼ (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))))$
	vdwlem7.m	$⊢ φ \to M \in ℕ$
	vdwlem7.g	$⊢ φ \to G : (1 \dots W) ⟶ R$
	vdwlem7.k	$⊢ φ \to K \in ℤ_{\geq 2}$
	vdwlem7.a	$⊢ φ \to A \in ℕ$
	vdwlem7.d	$⊢ φ \to D \in ℕ$
	vdwlem7.s	$⊢ φ \to A AP (K) D \subseteq F^{-1} [\{G\}]$
Assertion	vdwlem7	$⊢ φ \to (⟨M, K⟩ PolyAP G \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP G))$

Proof

Step	Hyp	Ref	Expression
1		vdwlem3.v	$⊢ φ \to V \in ℕ$
2		vdwlem3.w	$⊢ φ \to W \in ℕ$
3		vdwlem4.r	$⊢ φ \to R \in Fin$
4		vdwlem4.h	$⊢ φ \to H : (1 \dots W 2 V) ⟶ R$
5		vdwlem4.f	$⊢ F = (x \in (1 \dots V) ⟼ (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))))$
6		vdwlem7.m	$⊢ φ \to M \in ℕ$
7		vdwlem7.g	$⊢ φ \to G : (1 \dots W) ⟶ R$
8		vdwlem7.k	$⊢ φ \to K \in ℤ_{\geq 2}$
9		vdwlem7.a	$⊢ φ \to A \in ℕ$
10		vdwlem7.d	$⊢ φ \to D \in ℕ$
11		vdwlem7.s	$⊢ φ \to A AP (K) D \subseteq F^{-1} [\{G\}]$
12		ovex	$⊢ (1 \dots W) \in V$
13		2nn0	$⊢ 2 \in ℕ_{0}$
14		eluznn0	$⊢ (2 \in ℕ_{0} \land K \in ℤ_{\geq 2}) \to K \in ℕ_{0}$
15	13 8 14	sylancr	$⊢ φ \to K \in ℕ_{0}$
16		eqid	$⊢ (1 \dots M) = (1 \dots M)$
17	12 15 7 6 16	vdwpc	$⊢ φ \to (⟨M, K⟩ PolyAP G \leftrightarrow \exists a \in ℕ \exists d \in (ℕ^{(1 \dots M)}) (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M))$
18	1	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to V \in ℕ$
19	2	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to W \in ℕ$
20	3	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to R \in Fin$
21	4	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to H : (1 \dots W 2 V) ⟶ R$
22	6	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to M \in ℕ$
23	7	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to G : (1 \dots W) ⟶ R$
24	8	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to K \in ℤ_{\geq 2}$
25	9	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to A \in ℕ$
26	10	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to D \in ℕ$
27	11	ad2antrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to A AP (K) D \subseteq F^{-1} [\{G\}]$
28		simplrl	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to a \in ℕ$
29		simplrr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to d \in (ℕ^{(1 \dots M)})$
30		nnex	$⊢ ℕ \in V$
31		ovex	$⊢ (1 \dots M) \in V$
32	30 31	elmap	$⊢ d \in (ℕ^{(1 \dots M)}) \leftrightarrow d : (1 \dots M) ⟶ ℕ$
33	29 32	sylib	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to d : (1 \dots M) ⟶ ℕ$
34		simprl	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to \forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}]$
35		fveq2	$⊢ i = k \to d (i) = d (k)$
36	35	oveq2d	$⊢ i = k \to a + d (i) = a + d (k)$
37	36 35	oveq12d	$⊢ i = k \to (a + d (i)) AP (K) d (i) = (a + d (k)) AP (K) d (k)$
38	36	fveq2d	$⊢ i = k \to G (a + d (i)) = G (a + d (k))$
39	38	sneqd	$⊢ i = k \to \{G (a + d (i))\} = \{G (a + d (k))\}$
40	39	imaeq2d	$⊢ i = k \to G^{-1} [\{G (a + d (i))\}] = G^{-1} [\{G (a + d (k))\}]$
41	37 40	sseq12d	$⊢ i = k \to ((a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \leftrightarrow (a + d (k)) AP (K) d (k) \subseteq G^{-1} [\{G (a + d (k))\}])$
42	41	cbvralvw	$⊢ \forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \leftrightarrow \forall k \in (1 \dots M) (a + d (k)) AP (K) d (k) \subseteq G^{-1} [\{G (a + d (k))\}]$
43	34 42	sylib	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to \forall k \in (1 \dots M) (a + d (k)) AP (K) d (k) \subseteq G^{-1} [\{G (a + d (k))\}]$
44	38	cbvmptv	$⊢ (i \in (1 \dots M) ⟼ G (a + d (i))) = (k \in (1 \dots M) ⟼ G (a + d (k)))$
45		simprr	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M$
46		eqid	$⊢ a + W (A + (V - D) - 1) = a + W (A + (V - D) - 1)$
47		eqid	$⊢ (j \in (1 \dots M + 1) ⟼ if (j = M + 1, 0, d (j)) + W D) = (j \in (1 \dots M + 1) ⟼ if (j = M + 1, 0, d (j)) + W D)$
48	18 19 20 21 5 22 23 24 25 26 27 28 33 43 44 45 46 47	vdwlem6	$⊢ ((φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \land (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M)) \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP G)$
49	48	ex	$⊢ (φ \land (a \in ℕ \land d \in (ℕ^{(1 \dots M)}))) \to ((\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M) \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP G))$
50	49	rexlimdvva	$⊢ φ \to (\exists a \in ℕ \exists d \in (ℕ^{(1 \dots M)}) (\forall i \in (1 \dots M) (a + d (i)) AP (K) d (i) \subseteq G^{-1} [\{G (a + d (i))\}] \land \|ran (i \in (1 \dots M) ⟼ G (a + d (i)))\| = M) \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP G))$
51	17 50	sylbid	$⊢ φ \to (⟨M, K⟩ PolyAP G \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP G))$

Metamath Proof Explorer

Theorem vdwlem7

Proof