vdwlem2

	Ref	Expression
Hypotheses	vdwlem2.r	$⊢ φ \to R \in Fin$
	vdwlem2.k	$⊢ φ \to K \in ℕ_{0}$
	vdwlem2.w	$⊢ φ \to W \in ℕ$
	vdwlem2.n	$⊢ φ \to N \in ℕ$
	vdwlem2.f	$⊢ φ \to F : (1 \dots M) ⟶ R$
	vdwlem2.m	$⊢ φ \to M \in ℤ_{\geq (W + N)}$
	vdwlem2.g	$⊢ G = (x \in (1 \dots W) ⟼ F (x + N))$
Assertion	vdwlem2	$⊢ φ \to (K MonoAP G \to K MonoAP F)$

Proof

Step	Hyp	Ref	Expression
1		vdwlem2.r	$⊢ φ \to R \in Fin$
2		vdwlem2.k	$⊢ φ \to K \in ℕ_{0}$
3		vdwlem2.w	$⊢ φ \to W \in ℕ$
4		vdwlem2.n	$⊢ φ \to N \in ℕ$
5		vdwlem2.f	$⊢ φ \to F : (1 \dots M) ⟶ R$
6		vdwlem2.m	$⊢ φ \to M \in ℤ_{\geq (W + N)}$
7		vdwlem2.g	$⊢ G = (x \in (1 \dots W) ⟼ F (x + N))$
8		id	$⊢ a \in ℕ \to a \in ℕ$
9		nnaddcl	$⊢ (a \in ℕ \land N \in ℕ) \to a + N \in ℕ$
10	8 4 9	syl2anr	$⊢ (φ \land a \in ℕ) \to a + N \in ℕ$
11		simpllr	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to a \in ℕ$
12	11	nncnd	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to a \in ℂ$
13	4	ad3antrrr	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to N \in ℕ$
14	13	nncnd	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to N \in ℂ$
15		elfznn0	$⊢ m \in (0 \dots K - 1) \to m \in ℕ_{0}$
16	15	adantl	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to m \in ℕ_{0}$
17	16	nn0cnd	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to m \in ℂ$
18		simplrl	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to d \in ℕ$
19	18	nncnd	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to d \in ℂ$
20	17 19	mulcld	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to m d \in ℂ$
21	12 14 20	add32d	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to a + N + m d = a + m d + N$
22		oveq1	$⊢ x = a + m d \to x + N = a + m d + N$
23	22	eleq1d	$⊢ x = a + m d \to (x + N \in (1 \dots M) \leftrightarrow a + m d + N \in (1 \dots M))$
24		elfznn	$⊢ x \in (1 \dots W) \to x \in ℕ$
25		nnaddcl	$⊢ (x \in ℕ \land N \in ℕ) \to x + N \in ℕ$
26	24 4 25	syl2anr	$⊢ (φ \land x \in (1 \dots W)) \to x + N \in ℕ$
27		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
28	26 27	eleqtrdi	$⊢ (φ \land x \in (1 \dots W)) \to x + N \in ℤ_{\geq 1}$
29		elfzuz3	$⊢ x \in (1 \dots W) \to W \in ℤ_{\geq x}$
30	4	nnzd	$⊢ φ \to N \in ℤ$
31		eluzadd	$⊢ (W \in ℤ_{\geq x} \land N \in ℤ) \to W + N \in ℤ_{\geq (x + N)}$
32	29 30 31	syl2anr	$⊢ (φ \land x \in (1 \dots W)) \to W + N \in ℤ_{\geq (x + N)}$
33		uztrn	$⊢ (M \in ℤ_{\geq (W + N)} \land W + N \in ℤ_{\geq (x + N)}) \to M \in ℤ_{\geq (x + N)}$
34	6 32 33	syl2an2r	$⊢ (φ \land x \in (1 \dots W)) \to M \in ℤ_{\geq (x + N)}$
35		elfzuzb	$⊢ x + N \in (1 \dots M) \leftrightarrow (x + N \in ℤ_{\geq 1} \land M \in ℤ_{\geq (x + N)})$
36	28 34 35	sylanbrc	$⊢ (φ \land x \in (1 \dots W)) \to x + N \in (1 \dots M)$
37	36	ralrimiva	$⊢ φ \to \forall x \in (1 \dots W) x + N \in (1 \dots M)$
38	37	ad3antrrr	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to \forall x \in (1 \dots W) x + N \in (1 \dots M)$
39		simplrr	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to a AP (K) d \subseteq G^{-1} [\{c\}]$
40		eqid	$⊢ a + m d = a + m d$
41		oveq1	$⊢ n = m \to n d = m d$
42	41	oveq2d	$⊢ n = m \to a + n d = a + m d$
43	42	rspceeqv	$⊢ (m \in (0 \dots K - 1) \land a + m d = a + m d) \to \exists n \in (0 \dots K - 1) a + m d = a + n d$
44	40 43	mpan2	$⊢ m \in (0 \dots K - 1) \to \exists n \in (0 \dots K - 1) a + m d = a + n d$
45	44	adantl	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to \exists n \in (0 \dots K - 1) a + m d = a + n d$
46	2	ad2antrr	$⊢ ((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \to K \in ℕ_{0}$
47	46	adantr	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to K \in ℕ_{0}$
48		vdwapval	$⊢ (K \in ℕ_{0} \land a \in ℕ \land d \in ℕ) \to (a + m d \in (a AP (K) d) \leftrightarrow \exists n \in (0 \dots K - 1) a + m d = a + n d)$
49	47 11 18 48	syl3anc	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to (a + m d \in (a AP (K) d) \leftrightarrow \exists n \in (0 \dots K - 1) a + m d = a + n d)$
50	45 49	mpbird	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to a + m d \in (a AP (K) d)$
51	39 50	sseldd	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to a + m d \in G^{-1} [\{c\}]$
52	5	ffvelcdmda	$⊢ (φ \land x + N \in (1 \dots M)) \to F (x + N) \in R$
53	36 52	syldan	$⊢ (φ \land x \in (1 \dots W)) \to F (x + N) \in R$
54	53 7	fmptd	$⊢ φ \to G : (1 \dots W) ⟶ R$
55	54	ffnd	$⊢ φ \to G Fn (1 \dots W)$
56	55	ad3antrrr	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to G Fn (1 \dots W)$
57		fniniseg	$⊢ G Fn (1 \dots W) \to (a + m d \in G^{-1} [\{c\}] \leftrightarrow (a + m d \in (1 \dots W) \land G (a + m d) = c))$
58	56 57	syl	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to (a + m d \in G^{-1} [\{c\}] \leftrightarrow (a + m d \in (1 \dots W) \land G (a + m d) = c))$
59	51 58	mpbid	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to (a + m d \in (1 \dots W) \land G (a + m d) = c)$
60	59	simpld	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to a + m d \in (1 \dots W)$
61	23 38 60	rspcdva	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to a + m d + N \in (1 \dots M)$
62	21 61	eqeltrd	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to a + N + m d \in (1 \dots M)$
63	21	fveq2d	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to F (a + N + m d) = F (a + m d + N)$
64	22	fveq2d	$⊢ x = a + m d \to F (x + N) = F (a + m d + N)$
65		fvex	$⊢ F (a + m d + N) \in V$
66	64 7 65	fvmpt	$⊢ a + m d \in (1 \dots W) \to G (a + m d) = F (a + m d + N)$
67	60 66	syl	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to G (a + m d) = F (a + m d + N)$
68	59	simprd	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to G (a + m d) = c$
69	63 67 68	3eqtr2d	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to F (a + N + m d) = c$
70	62 69	jca	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to (a + N + m d \in (1 \dots M) \land F (a + N + m d) = c)$
71		eleq1	$⊢ x = a + N + m d \to (x \in (1 \dots M) \leftrightarrow a + N + m d \in (1 \dots M))$
72		fveqeq2	$⊢ x = a + N + m d \to (F (x) = c \leftrightarrow F (a + N + m d) = c)$
73	71 72	anbi12d	$⊢ x = a + N + m d \to ((x \in (1 \dots M) \land F (x) = c) \leftrightarrow (a + N + m d \in (1 \dots M) \land F (a + N + m d) = c))$
74	70 73	syl5ibrcom	$⊢ (((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \land m \in (0 \dots K - 1)) \to (x = a + N + m d \to (x \in (1 \dots M) \land F (x) = c))$
75	74	rexlimdva	$⊢ ((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \to (\exists m \in (0 \dots K - 1) x = a + N + m d \to (x \in (1 \dots M) \land F (x) = c))$
76	10	adantr	$⊢ ((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \to a + N \in ℕ$
77		simprl	$⊢ ((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \to d \in ℕ$
78		vdwapval	$⊢ (K \in ℕ_{0} \land a + N \in ℕ \land d \in ℕ) \to (x \in ((a + N) AP (K) d) \leftrightarrow \exists m \in (0 \dots K - 1) x = a + N + m d)$
79	46 76 77 78	syl3anc	$⊢ ((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \to (x \in ((a + N) AP (K) d) \leftrightarrow \exists m \in (0 \dots K - 1) x = a + N + m d)$
80	5	ffnd	$⊢ φ \to F Fn (1 \dots M)$
81	80	ad2antrr	$⊢ ((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \to F Fn (1 \dots M)$
82		fniniseg	$⊢ F Fn (1 \dots M) \to (x \in F^{-1} [\{c\}] \leftrightarrow (x \in (1 \dots M) \land F (x) = c))$
83	81 82	syl	$⊢ ((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \to (x \in F^{-1} [\{c\}] \leftrightarrow (x \in (1 \dots M) \land F (x) = c))$
84	75 79 83	3imtr4d	$⊢ ((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \to (x \in ((a + N) AP (K) d) \to x \in F^{-1} [\{c\}])$
85	84	ssrdv	$⊢ ((φ \land a \in ℕ) \land (d \in ℕ \land a AP (K) d \subseteq G^{-1} [\{c\}])) \to (a + N) AP (K) d \subseteq F^{-1} [\{c\}]$
86	85	expr	$⊢ ((φ \land a \in ℕ) \land d \in ℕ) \to (a AP (K) d \subseteq G^{-1} [\{c\}] \to (a + N) AP (K) d \subseteq F^{-1} [\{c\}])$
87	86	reximdva	$⊢ (φ \land a \in ℕ) \to (\exists d \in ℕ a AP (K) d \subseteq G^{-1} [\{c\}] \to \exists d \in ℕ (a + N) AP (K) d \subseteq F^{-1} [\{c\}])$
88		oveq1	$⊢ b = a + N \to b AP (K) d = (a + N) AP (K) d$
89	88	sseq1d	$⊢ b = a + N \to (b AP (K) d \subseteq F^{-1} [\{c\}] \leftrightarrow (a + N) AP (K) d \subseteq F^{-1} [\{c\}])$
90	89	rexbidv	$⊢ b = a + N \to (\exists d \in ℕ b AP (K) d \subseteq F^{-1} [\{c\}] \leftrightarrow \exists d \in ℕ (a + N) AP (K) d \subseteq F^{-1} [\{c\}])$
91	90	rspcev	$⊢ (a + N \in ℕ \land \exists d \in ℕ (a + N) AP (K) d \subseteq F^{-1} [\{c\}]) \to \exists b \in ℕ \exists d \in ℕ b AP (K) d \subseteq F^{-1} [\{c\}]$
92	10 87 91	syl6an	$⊢ (φ \land a \in ℕ) \to (\exists d \in ℕ a AP (K) d \subseteq G^{-1} [\{c\}] \to \exists b \in ℕ \exists d \in ℕ b AP (K) d \subseteq F^{-1} [\{c\}])$
93	92	rexlimdva	$⊢ φ \to (\exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq G^{-1} [\{c\}] \to \exists b \in ℕ \exists d \in ℕ b AP (K) d \subseteq F^{-1} [\{c\}])$
94	93	eximdv	$⊢ φ \to (\exists c \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq G^{-1} [\{c\}] \to \exists c \exists b \in ℕ \exists d \in ℕ b AP (K) d \subseteq F^{-1} [\{c\}])$
95		ovex	$⊢ (1 \dots W) \in V$
96	95 2 54	vdwmc	$⊢ φ \to (K MonoAP G \leftrightarrow \exists c \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq G^{-1} [\{c\}])$
97		ovex	$⊢ (1 \dots M) \in V$
98	97 2 5	vdwmc	$⊢ φ \to (K MonoAP F \leftrightarrow \exists c \exists b \in ℕ \exists d \in ℕ b AP (K) d \subseteq F^{-1} [\{c\}])$
99	94 96 98	3imtr4d	$⊢ φ \to (K MonoAP G \to K MonoAP F)$

Metamath Proof Explorer

Theorem vdwlem2

Proof