vdwlem8

	Ref	Expression
Hypotheses	vdwlem8.r	$⊢ φ \to R \in Fin$
	vdwlem8.k	$⊢ φ \to K \in ℤ_{\geq 2}$
	vdwlem8.w	$⊢ φ \to W \in ℕ$
	vdwlem8.f	$⊢ φ \to F : (1 \dots 2 W) ⟶ R$
	vdwlem8.c	$⊢ C \in V$
	vdwlem8.a	$⊢ φ \to A \in ℕ$
	vdwlem8.d	$⊢ φ \to D \in ℕ$
	vdwlem8.s	$⊢ φ \to A AP (K) D \subseteq G^{-1} [\{C\}]$
	vdwlem8.g	$⊢ G = (x \in (1 \dots W) ⟼ F (x + W))$
Assertion	vdwlem8	$⊢ φ \to ⟨1, K⟩ PolyAP F$

Proof

Step	Hyp	Ref	Expression
1		vdwlem8.r	$⊢ φ \to R \in Fin$
2		vdwlem8.k	$⊢ φ \to K \in ℤ_{\geq 2}$
3		vdwlem8.w	$⊢ φ \to W \in ℕ$
4		vdwlem8.f	$⊢ φ \to F : (1 \dots 2 W) ⟶ R$
5		vdwlem8.c	$⊢ C \in V$
6		vdwlem8.a	$⊢ φ \to A \in ℕ$
7		vdwlem8.d	$⊢ φ \to D \in ℕ$
8		vdwlem8.s	$⊢ φ \to A AP (K) D \subseteq G^{-1} [\{C\}]$
9		vdwlem8.g	$⊢ G = (x \in (1 \dots W) ⟼ F (x + W))$
10	6	nncnd	$⊢ φ \to A \in ℂ$
11	7	nncnd	$⊢ φ \to D \in ℂ$
12	10 11	addcomd	$⊢ φ \to A + D = D + A$
13	12	oveq2d	$⊢ φ \to W - (A + D) = W - (D + A)$
14	3	nncnd	$⊢ φ \to W \in ℂ$
15	14 11 10	subsub4d	$⊢ φ \to W - D - A = W - (D + A)$
16	13 15	eqtr4d	$⊢ φ \to W - (A + D) = W - D - A$
17	16	oveq2d	$⊢ φ \to A + A + (W - (A + D)) = A + A + (W - D - A)$
18	14 11	subcld	$⊢ φ \to W - D \in ℂ$
19	10 10 18	ppncand	$⊢ φ \to A + A + (W - D - A) = A + W - D$
20	17 19	eqtrd	$⊢ φ \to A + A + (W - (A + D)) = A + W - D$
21	6 6	nnaddcld	$⊢ φ \to A + A \in ℕ$
22		cnvimass	$⊢ G^{-1} [\{C\}] \subseteq dom G$
23		fvex	$⊢ F (x + W) \in V$
24	23 9	dmmpti	$⊢ dom G = (1 \dots W)$
25	22 24	sseqtri	$⊢ G^{-1} [\{C\}] \subseteq (1 \dots W)$
26	8 25	sstrdi	$⊢ φ \to A AP (K) D \subseteq (1 \dots W)$
27		ssun2	$⊢ (A + D) AP (K - 1) D \subseteq \{A\} \cup ((A + D) AP (K - 1) D)$
28		uz2m1nn	$⊢ K \in ℤ_{\geq 2} \to K - 1 \in ℕ$
29	2 28	syl	$⊢ φ \to K - 1 \in ℕ$
30	6 7	nnaddcld	$⊢ φ \to A + D \in ℕ$
31		vdwapid1	$⊢ (K - 1 \in ℕ \land A + D \in ℕ \land D \in ℕ) \to A + D \in ((A + D) AP (K - 1) D)$
32	29 30 7 31	syl3anc	$⊢ φ \to A + D \in ((A + D) AP (K - 1) D)$
33	27 32	sselid	$⊢ φ \to A + D \in (\{A\} \cup ((A + D) AP (K - 1) D))$
34		eluz2nn	$⊢ K \in ℤ_{\geq 2} \to K \in ℕ$
35	2 34	syl	$⊢ φ \to K \in ℕ$
36	35	nncnd	$⊢ φ \to K \in ℂ$
37		ax-1cn	$⊢ 1 \in ℂ$
38		npcan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K - 1 + 1 = K$
39	36 37 38	sylancl	$⊢ φ \to K - 1 + 1 = K$
40	39	fveq2d	$⊢ φ \to AP (K - 1 + 1) = AP (K)$
41	40	oveqd	$⊢ φ \to A AP (K - 1 + 1) D = A AP (K) D$
42	29	nnnn0d	$⊢ φ \to K - 1 \in ℕ_{0}$
43		vdwapun	$⊢ (K - 1 \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A AP (K - 1 + 1) D = \{A\} \cup ((A + D) AP (K - 1) D)$
44	42 6 7 43	syl3anc	$⊢ φ \to A AP (K - 1 + 1) D = \{A\} \cup ((A + D) AP (K - 1) D)$
45	41 44	eqtr3d	$⊢ φ \to A AP (K) D = \{A\} \cup ((A + D) AP (K - 1) D)$
46	33 45	eleqtrrd	$⊢ φ \to A + D \in (A AP (K) D)$
47	26 46	sseldd	$⊢ φ \to A + D \in (1 \dots W)$
48		elfzuz3	$⊢ A + D \in (1 \dots W) \to W \in ℤ_{\geq (A + D)}$
49		uznn0sub	$⊢ W \in ℤ_{\geq (A + D)} \to W - (A + D) \in ℕ_{0}$
50	47 48 49	3syl	$⊢ φ \to W - (A + D) \in ℕ_{0}$
51		nnnn0addcl	$⊢ (A + A \in ℕ \land W - (A + D) \in ℕ_{0}) \to A + A + (W - (A + D)) \in ℕ$
52	21 50 51	syl2anc	$⊢ φ \to A + A + (W - (A + D)) \in ℕ$
53	20 52	eqeltrrd	$⊢ φ \to A + W - D \in ℕ$
54		1nn	$⊢ 1 \in ℕ$
55		f1osng	$⊢ (1 \in ℕ \land D \in ℕ) \to \{⟨1, D⟩\} : \{1\} \underset{1-1 onto}{⟶} \{D\}$
56	54 7 55	sylancr	$⊢ φ \to \{⟨1, D⟩\} : \{1\} \underset{1-1 onto}{⟶} \{D\}$
57		f1of	$⊢ \{⟨1, D⟩\} : \{1\} \underset{1-1 onto}{⟶} \{D\} \to \{⟨1, D⟩\} : \{1\} ⟶ \{D\}$
58	56 57	syl	$⊢ φ \to \{⟨1, D⟩\} : \{1\} ⟶ \{D\}$
59	7	snssd	$⊢ φ \to \{D\} \subseteq ℕ$
60	58 59	fssd	$⊢ φ \to \{⟨1, D⟩\} : \{1\} ⟶ ℕ$
61		1z	$⊢ 1 \in ℤ$
62		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
63	61 62	ax-mp	$⊢ (1 \dots 1) = \{1\}$
64	63	feq2i	$⊢ \{⟨1, D⟩\} : (1 \dots 1) ⟶ ℕ \leftrightarrow \{⟨1, D⟩\} : \{1\} ⟶ ℕ$
65	60 64	sylibr	$⊢ φ \to \{⟨1, D⟩\} : (1 \dots 1) ⟶ ℕ$
66		nnex	$⊢ ℕ \in V$
67		ovex	$⊢ (1 \dots 1) \in V$
68	66 67	elmap	$⊢ \{⟨1, D⟩\} \in (ℕ^{(1 \dots 1)}) \leftrightarrow \{⟨1, D⟩\} : (1 \dots 1) ⟶ ℕ$
69	65 68	sylibr	$⊢ φ \to \{⟨1, D⟩\} \in (ℕ^{(1 \dots 1)})$
70	6 3	nnaddcld	$⊢ φ \to A + W \in ℕ$
71	70	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + W \in ℕ$
72		elfznn0	$⊢ m \in (0 \dots K - 1) \to m \in ℕ_{0}$
73	7	nnnn0d	$⊢ φ \to D \in ℕ_{0}$
74		nn0mulcl	$⊢ (m \in ℕ_{0} \land D \in ℕ_{0}) \to m D \in ℕ_{0}$
75	72 73 74	syl2anr	$⊢ (φ \land m \in (0 \dots K - 1)) \to m D \in ℕ_{0}$
76		nnnn0addcl	$⊢ (A + W \in ℕ \land m D \in ℕ_{0}) \to A + W + m D \in ℕ$
77	71 75 76	syl2anc	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + W + m D \in ℕ$
78		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
79	77 78	eleqtrdi	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + W + m D \in ℤ_{\geq 1}$
80	8	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to A AP (K) D \subseteq G^{-1} [\{C\}]$
81		eqid	$⊢ A + m D = A + m D$
82		oveq1	$⊢ n = m \to n D = m D$
83	82	oveq2d	$⊢ n = m \to A + n D = A + m D$
84	83	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$
85	81 84	mpan2	$⊢ m \in (0 \dots K - 1) \to \exists n \in (0 \dots K - 1) A + m D = A + n D$
86	35	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
87		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)$
88	86 6 7 87	syl3anc	$⊢ φ \to (A + m D \in (A AP (K) D) \leftrightarrow \exists n \in (0 \dots K - 1) A + m D = A + n D)$
89	88	biimpar	$⊢ (φ \land \exists n \in (0 \dots K - 1) A + m D = A + n D) \to A + m D \in (A AP (K) D)$
90	85 89	sylan2	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + m D \in (A AP (K) D)$
91	80 90	sseldd	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + m D \in G^{-1} [\{C\}]$
92	23 9	fnmpti	$⊢ G Fn (1 \dots W)$
93		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))$
94	92 93	ax-mp	$⊢ A + m D \in G^{-1} [\{C\}] \leftrightarrow (A + m D \in (1 \dots W) \land G (A + m D) = C)$
95	91 94	sylib	$⊢ (φ \land m \in (0 \dots K - 1)) \to (A + m D \in (1 \dots W) \land G (A + m D) = C)$
96	95	simpld	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + m D \in (1 \dots W)$
97		elfzuz3	$⊢ A + m D \in (1 \dots W) \to W \in ℤ_{\geq (A + m D)}$
98		eluzelz	$⊢ W \in ℤ_{\geq (A + m D)} \to W \in ℤ$
99		eluzadd	$⊢ (W \in ℤ_{\geq (A + m D)} \land W \in ℤ) \to W + W \in ℤ_{\geq (A + m D + W)}$
100	98 99	mpdan	$⊢ W \in ℤ_{\geq (A + m D)} \to W + W \in ℤ_{\geq (A + m D + W)}$
101	96 97 100	3syl	$⊢ (φ \land m \in (0 \dots K - 1)) \to W + W \in ℤ_{\geq (A + m D + W)}$
102	14	2timesd	$⊢ φ \to 2 W = W + W$
103	102	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to 2 W = W + W$
104	10	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to A \in ℂ$
105	14	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to W \in ℂ$
106	75	nn0cnd	$⊢ (φ \land m \in (0 \dots K - 1)) \to m D \in ℂ$
107	104 105 106	add32d	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + W + m D = A + m D + W$
108	107	fveq2d	$⊢ (φ \land m \in (0 \dots K - 1)) \to ℤ_{\geq (A + W + m D)} = ℤ_{\geq (A + m D + W)}$
109	101 103 108	3eltr4d	$⊢ (φ \land m \in (0 \dots K - 1)) \to 2 W \in ℤ_{\geq (A + W + m D)}$
110		elfzuzb	$⊢ A + W + m D \in (1 \dots 2 W) \leftrightarrow (A + W + m D \in ℤ_{\geq 1} \land 2 W \in ℤ_{\geq (A + W + m D)})$
111	79 109 110	sylanbrc	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + W + m D \in (1 \dots 2 W)$
112	107	fveq2d	$⊢ (φ \land m \in (0 \dots K - 1)) \to F (A + W + m D) = F (A + m D + W)$
113		fvoveq1	$⊢ x = A + m D \to F (x + W) = F (A + m D + W)$
114		fvex	$⊢ F (A + m D + W) \in V$
115	113 9 114	fvmpt	$⊢ A + m D \in (1 \dots W) \to G (A + m D) = F (A + m D + W)$
116	96 115	syl	$⊢ (φ \land m \in (0 \dots K - 1)) \to G (A + m D) = F (A + m D + W)$
117	95	simprd	$⊢ (φ \land m \in (0 \dots K - 1)) \to G (A + m D) = C$
118	112 116 117	3eqtr2d	$⊢ (φ \land m \in (0 \dots K - 1)) \to F (A + W + m D) = C$
119	111 118	jca	$⊢ (φ \land m \in (0 \dots K - 1)) \to (A + W + m D \in (1 \dots 2 W) \land F (A + W + m D) = C)$
120		eleq1	$⊢ x = A + W + m D \to (x \in (1 \dots 2 W) \leftrightarrow A + W + m D \in (1 \dots 2 W))$
121		fveqeq2	$⊢ x = A + W + m D \to (F (x) = C \leftrightarrow F (A + W + m D) = C)$
122	120 121	anbi12d	$⊢ x = A + W + m D \to ((x \in (1 \dots 2 W) \land F (x) = C) \leftrightarrow (A + W + m D \in (1 \dots 2 W) \land F (A + W + m D) = C))$
123	119 122	syl5ibrcom	$⊢ (φ \land m \in (0 \dots K - 1)) \to (x = A + W + m D \to (x \in (1 \dots 2 W) \land F (x) = C))$
124	123	rexlimdva	$⊢ φ \to (\exists m \in (0 \dots K - 1) x = A + W + m D \to (x \in (1 \dots 2 W) \land F (x) = C))$
125		vdwapval	$⊢ (K \in ℕ_{0} \land A + W \in ℕ \land D \in ℕ) \to (x \in ((A + W) AP (K) D) \leftrightarrow \exists m \in (0 \dots K - 1) x = A + W + m D)$
126	86 70 7 125	syl3anc	$⊢ φ \to (x \in ((A + W) AP (K) D) \leftrightarrow \exists m \in (0 \dots K - 1) x = A + W + m D)$
127		ffn	$⊢ F : (1 \dots 2 W) ⟶ R \to F Fn (1 \dots 2 W)$
128		fniniseg	$⊢ F Fn (1 \dots 2 W) \to (x \in F^{-1} [\{C\}] \leftrightarrow (x \in (1 \dots 2 W) \land F (x) = C))$
129	4 127 128	3syl	$⊢ φ \to (x \in F^{-1} [\{C\}] \leftrightarrow (x \in (1 \dots 2 W) \land F (x) = C))$
130	124 126 129	3imtr4d	$⊢ φ \to (x \in ((A + W) AP (K) D) \to x \in F^{-1} [\{C\}])$
131	130	ssrdv	$⊢ φ \to (A + W) AP (K) D \subseteq F^{-1} [\{C\}]$
132		fvsng	$⊢ (1 \in ℕ \land D \in ℕ) \to \{⟨1, D⟩\} (1) = D$
133	54 7 132	sylancr	$⊢ φ \to \{⟨1, D⟩\} (1) = D$
134	133	oveq2d	$⊢ φ \to A + (W - D) + \{⟨1, D⟩\} (1) = A + (W - D) + D$
135	10 18 11	addassd	$⊢ φ \to A + (W - D) + D = A + (W - D) + D$
136	14 11	npcand	$⊢ φ \to W - D + D = W$
137	136	oveq2d	$⊢ φ \to A + (W - D) + D = A + W$
138	134 135 137	3eqtrd	$⊢ φ \to A + (W - D) + \{⟨1, D⟩\} (1) = A + W$
139	138 133	oveq12d	$⊢ φ \to (A + (W - D) + \{⟨1, D⟩\} (1)) AP (K) \{⟨1, D⟩\} (1) = (A + W) AP (K) D$
140	138	fveq2d	$⊢ φ \to F (A + (W - D) + \{⟨1, D⟩\} (1)) = F (A + W)$
141		vdwapid1	$⊢ (K \in ℕ \land A \in ℕ \land D \in ℕ) \to A \in (A AP (K) D)$
142	35 6 7 141	syl3anc	$⊢ φ \to A \in (A AP (K) D)$
143	8 142	sseldd	$⊢ φ \to A \in G^{-1} [\{C\}]$
144		fniniseg	$⊢ G Fn (1 \dots W) \to (A \in G^{-1} [\{C\}] \leftrightarrow (A \in (1 \dots W) \land G (A) = C))$
145	92 144	ax-mp	$⊢ A \in G^{-1} [\{C\}] \leftrightarrow (A \in (1 \dots W) \land G (A) = C)$
146	143 145	sylib	$⊢ φ \to (A \in (1 \dots W) \land G (A) = C)$
147	146	simpld	$⊢ φ \to A \in (1 \dots W)$
148		fvoveq1	$⊢ x = A \to F (x + W) = F (A + W)$
149		fvex	$⊢ F (A + W) \in V$
150	148 9 149	fvmpt	$⊢ A \in (1 \dots W) \to G (A) = F (A + W)$
151	147 150	syl	$⊢ φ \to G (A) = F (A + W)$
152	146	simprd	$⊢ φ \to G (A) = C$
153	140 151 152	3eqtr2d	$⊢ φ \to F (A + (W - D) + \{⟨1, D⟩\} (1)) = C$
154	153	sneqd	$⊢ φ \to \{F (A + (W - D) + \{⟨1, D⟩\} (1))\} = \{C\}$
155	154	imaeq2d	$⊢ φ \to F^{-1} [\{F (A + (W - D) + \{⟨1, D⟩\} (1))\}] = F^{-1} [\{C\}]$
156	131 139 155	3sstr4d	$⊢ φ \to (A + (W - D) + \{⟨1, D⟩\} (1)) AP (K) \{⟨1, D⟩\} (1) \subseteq F^{-1} [\{F (A + (W - D) + \{⟨1, D⟩\} (1))\}]$
157	156	ralrimivw	$⊢ φ \to \forall i \in (1 \dots 1) (A + (W - D) + \{⟨1, D⟩\} (1)) AP (K) \{⟨1, D⟩\} (1) \subseteq F^{-1} [\{F (A + (W - D) + \{⟨1, D⟩\} (1))\}]$
158	153	mpteq2dv	$⊢ φ \to (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1))) = (i \in (1 \dots 1) ⟼ C)$
159		fconstmpt	$⊢ (1 \dots 1) \times \{C\} = (i \in (1 \dots 1) ⟼ C)$
160	158 159	eqtr4di	$⊢ φ \to (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1))) = (1 \dots 1) \times \{C\}$
161	160	rneqd	$⊢ φ \to ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1))) = ran ((1 \dots 1) \times \{C\})$
162		elfz3	$⊢ 1 \in ℤ \to 1 \in (1 \dots 1)$
163		ne0i	$⊢ 1 \in (1 \dots 1) \to (1 \dots 1) \neq \emptyset$
164	61 162 163	mp2b	$⊢ (1 \dots 1) \neq \emptyset$
165		rnxp	$⊢ (1 \dots 1) \neq \emptyset \to ran ((1 \dots 1) \times \{C\}) = \{C\}$
166	164 165	ax-mp	$⊢ ran ((1 \dots 1) \times \{C\}) = \{C\}$
167	161 166	eqtrdi	$⊢ φ \to ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1))) = \{C\}$
168	167	fveq2d	$⊢ φ \to \|ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1)))\| = \|\{C\}\|$
169		hashsng	$⊢ C \in V \to \|\{C\}\| = 1$
170	5 169	ax-mp	$⊢ \|\{C\}\| = 1$
171	168 170	eqtrdi	$⊢ φ \to \|ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1)))\| = 1$
172		oveq1	$⊢ a = A + W - D \to a + d (i) = A + (W - D) + d (i)$
173	172	oveq1d	$⊢ a = A + W - D \to (a + d (i)) AP (K) d (i) = (A + (W - D) + d (i)) AP (K) d (i)$
174		fvoveq1	$⊢ a = A + W - D \to F (a + d (i)) = F (A + (W - D) + d (i))$
175	174	sneqd	$⊢ a = A + W - D \to \{F (a + d (i))\} = \{F (A + (W - D) + d (i))\}$
176	175	imaeq2d	$⊢ a = A + W - D \to F^{-1} [\{F (a + d (i))\}] = F^{-1} [\{F (A + (W - D) + d (i))\}]$
177	173 176	sseq12d	$⊢ a = A + W - D \to ((a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \leftrightarrow (A + (W - D) + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (A + (W - D) + d (i))\}])$
178	177	ralbidv	$⊢ a = A + W - D \to (\forall i \in (1 \dots 1) (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \leftrightarrow \forall i \in (1 \dots 1) (A + (W - D) + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (A + (W - D) + d (i))\}])$
179	174	mpteq2dv	$⊢ a = A + W - D \to (i \in (1 \dots 1) ⟼ F (a + d (i))) = (i \in (1 \dots 1) ⟼ F (A + (W - D) + d (i)))$
180	179	rneqd	$⊢ a = A + W - D \to ran (i \in (1 \dots 1) ⟼ F (a + d (i))) = ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + d (i)))$
181	180	fveqeq2d	$⊢ a = A + W - D \to (\|ran (i \in (1 \dots 1) ⟼ F (a + d (i)))\| = 1 \leftrightarrow \|ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + d (i)))\| = 1)$
182	178 181	anbi12d	$⊢ a = A + W - D \to ((\forall i \in (1 \dots 1) (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in (1 \dots 1) ⟼ F (a + d (i)))\| = 1) \leftrightarrow (\forall i \in (1 \dots 1) (A + (W - D) + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (A + (W - D) + d (i))\}] \land \|ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + d (i)))\| = 1))$
183		fveq1	$⊢ d = \{⟨1, D⟩\} \to d (i) = \{⟨1, D⟩\} (i)$
184		elfz1eq	$⊢ i \in (1 \dots 1) \to i = 1$
185	184	fveq2d	$⊢ i \in (1 \dots 1) \to \{⟨1, D⟩\} (i) = \{⟨1, D⟩\} (1)$
186	183 185	sylan9eq	$⊢ (d = \{⟨1, D⟩\} \land i \in (1 \dots 1)) \to d (i) = \{⟨1, D⟩\} (1)$
187	186	oveq2d	$⊢ (d = \{⟨1, D⟩\} \land i \in (1 \dots 1)) \to A + (W - D) + d (i) = A + (W - D) + \{⟨1, D⟩\} (1)$
188	187 186	oveq12d	$⊢ (d = \{⟨1, D⟩\} \land i \in (1 \dots 1)) \to (A + (W - D) + d (i)) AP (K) d (i) = (A + (W - D) + \{⟨1, D⟩\} (1)) AP (K) \{⟨1, D⟩\} (1)$
189	187	fveq2d	$⊢ (d = \{⟨1, D⟩\} \land i \in (1 \dots 1)) \to F (A + (W - D) + d (i)) = F (A + (W - D) + \{⟨1, D⟩\} (1))$
190	189	sneqd	$⊢ (d = \{⟨1, D⟩\} \land i \in (1 \dots 1)) \to \{F (A + (W - D) + d (i))\} = \{F (A + (W - D) + \{⟨1, D⟩\} (1))\}$
191	190	imaeq2d	$⊢ (d = \{⟨1, D⟩\} \land i \in (1 \dots 1)) \to F^{-1} [\{F (A + (W - D) + d (i))\}] = F^{-1} [\{F (A + (W - D) + \{⟨1, D⟩\} (1))\}]$
192	188 191	sseq12d	$⊢ (d = \{⟨1, D⟩\} \land i \in (1 \dots 1)) \to ((A + (W - D) + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (A + (W - D) + d (i))\}] \leftrightarrow (A + (W - D) + \{⟨1, D⟩\} (1)) AP (K) \{⟨1, D⟩\} (1) \subseteq F^{-1} [\{F (A + (W - D) + \{⟨1, D⟩\} (1))\}])$
193	192	ralbidva	$⊢ d = \{⟨1, D⟩\} \to (\forall i \in (1 \dots 1) (A + (W - D) + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (A + (W - D) + d (i))\}] \leftrightarrow \forall i \in (1 \dots 1) (A + (W - D) + \{⟨1, D⟩\} (1)) AP (K) \{⟨1, D⟩\} (1) \subseteq F^{-1} [\{F (A + (W - D) + \{⟨1, D⟩\} (1))\}])$
194	189	mpteq2dva	$⊢ d = \{⟨1, D⟩\} \to (i \in (1 \dots 1) ⟼ F (A + (W - D) + d (i))) = (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1)))$
195	194	rneqd	$⊢ d = \{⟨1, D⟩\} \to ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + d (i))) = ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1)))$
196	195	fveqeq2d	$⊢ d = \{⟨1, D⟩\} \to (\|ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + d (i)))\| = 1 \leftrightarrow \|ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1)))\| = 1)$
197	193 196	anbi12d	$⊢ d = \{⟨1, D⟩\} \to ((\forall i \in (1 \dots 1) (A + (W - D) + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (A + (W - D) + d (i))\}] \land \|ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + d (i)))\| = 1) \leftrightarrow (\forall i \in (1 \dots 1) (A + (W - D) + \{⟨1, D⟩\} (1)) AP (K) \{⟨1, D⟩\} (1) \subseteq F^{-1} [\{F (A + (W - D) + \{⟨1, D⟩\} (1))\}] \land \|ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1)))\| = 1))$
198	182 197	rspc2ev	$⊢ (A + W - D \in ℕ \land \{⟨1, D⟩\} \in (ℕ^{(1 \dots 1)}) \land (\forall i \in (1 \dots 1) (A + (W - D) + \{⟨1, D⟩\} (1)) AP (K) \{⟨1, D⟩\} (1) \subseteq F^{-1} [\{F (A + (W - D) + \{⟨1, D⟩\} (1))\}] \land \|ran (i \in (1 \dots 1) ⟼ F (A + (W - D) + \{⟨1, D⟩\} (1)))\| = 1)) \to \exists a \in ℕ \exists d \in (ℕ^{(1 \dots 1)}) (\forall i \in (1 \dots 1) (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in (1 \dots 1) ⟼ F (a + d (i)))\| = 1)$
199	53 69 157 171 198	syl112anc	$⊢ φ \to \exists a \in ℕ \exists d \in (ℕ^{(1 \dots 1)}) (\forall i \in (1 \dots 1) (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in (1 \dots 1) ⟼ F (a + d (i)))\| = 1)$
200		ovex	$⊢ (1 \dots 2 W) \in V$
201	54	a1i	$⊢ φ \to 1 \in ℕ$
202		eqid	$⊢ (1 \dots 1) = (1 \dots 1)$
203	200 86 4 201 202	vdwpc	$⊢ φ \to (⟨1, K⟩ PolyAP F \leftrightarrow \exists a \in ℕ \exists d \in (ℕ^{(1 \dots 1)}) (\forall i \in (1 \dots 1) (a + d (i)) AP (K) d (i) \subseteq F^{-1} [\{F (a + d (i))\}] \land \|ran (i \in (1 \dots 1) ⟼ F (a + d (i)))\| = 1))$
204	199 203	mpbird	$⊢ φ \to ⟨1, K⟩ PolyAP F$

Metamath Proof Explorer

Theorem vdwlem8

Proof