mzpcompact2lem

		Ref	Expression
	Hypothesis	mzpcompact2lem.i	$⊢ B \in V$
	Assertion	mzpcompact2lem	$⊢ A \in mzPoly (B) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land A = (c \in (ℤ^{B}) ⟼ b ({c ↾}_{a})))$

Proof

Step	Hyp	Ref	Expression
1		mzpcompact2lem.i	$⊢ B \in V$
2		tru	$⊢ ⊤$
3		0fin	$⊢ \emptyset \in Fin$
4		0ex	$⊢ \emptyset \in V$
5		mzpconst	$⊢ (\emptyset \in V \land f \in ℤ) \to (ℤ^{\emptyset}) \times \{f\} \in mzPoly (\emptyset)$
6	4 5	mpan	$⊢ f \in ℤ \to (ℤ^{\emptyset}) \times \{f\} \in mzPoly (\emptyset)$
7		0ss	$⊢ \emptyset \subseteq B$
8	7	a1i	$⊢ f \in ℤ \to \emptyset \subseteq B$
9		fconstmpt	$⊢ (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ f)$
10		simpr	$⊢ (f \in ℤ \land d \in (ℤ^{B})) \to d \in (ℤ^{B})$
11		elmapssres	$⊢ (d \in (ℤ^{B}) \land \emptyset \subseteq B) \to {d ↾}_{\emptyset} \in (ℤ^{\emptyset})$
12	10 7 11	sylancl	$⊢ (f \in ℤ \land d \in (ℤ^{B})) \to {d ↾}_{\emptyset} \in (ℤ^{\emptyset})$
13		vex	$⊢ f \in V$
14	13	fvconst2	$⊢ {d ↾}_{\emptyset} \in (ℤ^{\emptyset}) \to ((ℤ^{\emptyset}) \times \{f\}) ({d ↾}_{\emptyset}) = f$
15	12 14	syl	$⊢ (f \in ℤ \land d \in (ℤ^{B})) \to ((ℤ^{\emptyset}) \times \{f\}) ({d ↾}_{\emptyset}) = f$
16	15	mpteq2dva	$⊢ f \in ℤ \to (d \in (ℤ^{B}) ⟼ ((ℤ^{\emptyset}) \times \{f\}) ({d ↾}_{\emptyset})) = (d \in (ℤ^{B}) ⟼ f)$
17	9 16	eqtr4id	$⊢ f \in ℤ \to (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ ((ℤ^{\emptyset}) \times \{f\}) ({d ↾}_{\emptyset}))$
18		fveq1	$⊢ b = (ℤ^{\emptyset}) \times \{f\} \to b ({d ↾}_{\emptyset}) = ((ℤ^{\emptyset}) \times \{f\}) ({d ↾}_{\emptyset})$
19	18	mpteq2dv	$⊢ b = (ℤ^{\emptyset}) \times \{f\} \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset})) = (d \in (ℤ^{B}) ⟼ ((ℤ^{\emptyset}) \times \{f\}) ({d ↾}_{\emptyset}))$
20	19	eqeq2d	$⊢ b = (ℤ^{\emptyset}) \times \{f\} \to ((ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset})) \leftrightarrow (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ ((ℤ^{\emptyset}) \times \{f\}) ({d ↾}_{\emptyset})))$
21	20	anbi2d	$⊢ b = (ℤ^{\emptyset}) \times \{f\} \to ((\emptyset \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset}))) \leftrightarrow (\emptyset \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ ((ℤ^{\emptyset}) \times \{f\}) ({d ↾}_{\emptyset}))))$
22	21	rspcev	$⊢ ((ℤ^{\emptyset}) \times \{f\} \in mzPoly (\emptyset) \land (\emptyset \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ ((ℤ^{\emptyset}) \times \{f\}) ({d ↾}_{\emptyset})))) \to \exists b \in mzPoly (\emptyset) (\emptyset \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset})))$
23	6 8 17 22	syl12anc	$⊢ f \in ℤ \to \exists b \in mzPoly (\emptyset) (\emptyset \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset})))$
24		fveq2	$⊢ a = \emptyset \to mzPoly (a) = mzPoly (\emptyset)$
25		sseq1	$⊢ a = \emptyset \to (a \subseteq B \leftrightarrow \emptyset \subseteq B)$
26		reseq2	$⊢ a = \emptyset \to {d ↾}_{a} = {d ↾}_{\emptyset}$
27	26	fveq2d	$⊢ a = \emptyset \to b ({d ↾}_{a}) = b ({d ↾}_{\emptyset})$
28	27	mpteq2dv	$⊢ a = \emptyset \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset}))$
29	28	eqeq2d	$⊢ a = \emptyset \to ((ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset})))$
30	25 29	anbi12d	$⊢ a = \emptyset \to ((a \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (\emptyset \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset}))))$
31	24 30	rexeqbidv	$⊢ a = \emptyset \to (\exists b \in mzPoly (a) (a \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists b \in mzPoly (\emptyset) (\emptyset \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset}))))$
32	31	rspcev	$⊢ (\emptyset \in Fin \land \exists b \in mzPoly (\emptyset) (\emptyset \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\emptyset})))) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
33	3 23 32	sylancr	$⊢ f \in ℤ \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
34	33	adantl	$⊢ (⊤ \land f \in ℤ) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
35		snfi	$⊢ \{f\} \in Fin$
36		vsnex	$⊢ \{f\} \in V$
37		vsnid	$⊢ f \in \{f\}$
38		mzpproj	$⊢ (\{f\} \in V \land f \in \{f\}) \to (g \in (ℤ^{\{f\}}) ⟼ g (f)) \in mzPoly (\{f\})$
39	36 37 38	mp2an	$⊢ (g \in (ℤ^{\{f\}}) ⟼ g (f)) \in mzPoly (\{f\})$
40	39	a1i	$⊢ f \in B \to (g \in (ℤ^{\{f\}}) ⟼ g (f)) \in mzPoly (\{f\})$
41		snssi	$⊢ f \in B \to \{f\} \subseteq B$
42		fveq1	$⊢ g = d \to g (f) = d (f)$
43	42	cbvmptv	$⊢ (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ d (f))$
44		simpr	$⊢ (f \in B \land d \in (ℤ^{B})) \to d \in (ℤ^{B})$
45		simpl	$⊢ (f \in B \land d \in (ℤ^{B})) \to f \in B$
46	45	snssd	$⊢ (f \in B \land d \in (ℤ^{B})) \to \{f\} \subseteq B$
47		elmapssres	$⊢ (d \in (ℤ^{B}) \land \{f\} \subseteq B) \to {d ↾}_{\{f\}} \in (ℤ^{\{f\}})$
48	44 46 47	syl2anc	$⊢ (f \in B \land d \in (ℤ^{B})) \to {d ↾}_{\{f\}} \in (ℤ^{\{f\}})$
49		fveq1	$⊢ g = {d ↾}_{\{f\}} \to g (f) = ({d ↾}_{\{f\}}) (f)$
50		eqid	$⊢ (g \in (ℤ^{\{f\}}) ⟼ g (f)) = (g \in (ℤ^{\{f\}}) ⟼ g (f))$
51		fvex	$⊢ ({d ↾}_{\{f\}}) (f) \in V$
52	49 50 51	fvmpt	$⊢ {d ↾}_{\{f\}} \in (ℤ^{\{f\}}) \to (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}}) = ({d ↾}_{\{f\}}) (f)$
53	48 52	syl	$⊢ (f \in B \land d \in (ℤ^{B})) \to (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}}) = ({d ↾}_{\{f\}}) (f)$
54		fvres	$⊢ f \in \{f\} \to ({d ↾}_{\{f\}}) (f) = d (f)$
55	37 54	ax-mp	$⊢ ({d ↾}_{\{f\}}) (f) = d (f)$
56	53 55	eqtr2di	$⊢ (f \in B \land d \in (ℤ^{B})) \to d (f) = (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}})$
57	56	mpteq2dva	$⊢ f \in B \to (d \in (ℤ^{B}) ⟼ d (f)) = (d \in (ℤ^{B}) ⟼ (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}}))$
58	43 57	eqtrid	$⊢ f \in B \to (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}}))$
59		fveq1	$⊢ b = (g \in (ℤ^{\{f\}}) ⟼ g (f)) \to b ({d ↾}_{\{f\}}) = (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}})$
60	59	mpteq2dv	$⊢ b = (g \in (ℤ^{\{f\}}) ⟼ g (f)) \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}})) = (d \in (ℤ^{B}) ⟼ (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}}))$
61	60	eqeq2d	$⊢ b = (g \in (ℤ^{\{f\}}) ⟼ g (f)) \to ((g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}})) \leftrightarrow (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}})))$
62	61	anbi2d	$⊢ b = (g \in (ℤ^{\{f\}}) ⟼ g (f)) \to ((\{f\} \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}}))) \leftrightarrow (\{f\} \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}}))))$
63	62	rspcev	$⊢ ((g \in (ℤ^{\{f\}}) ⟼ g (f)) \in mzPoly (\{f\}) \land (\{f\} \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ (g \in (ℤ^{\{f\}}) ⟼ g (f)) ({d ↾}_{\{f\}})))) \to \exists b \in mzPoly (\{f\}) (\{f\} \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}})))$
64	40 41 58 63	syl12anc	$⊢ f \in B \to \exists b \in mzPoly (\{f\}) (\{f\} \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}})))$
65		fveq2	$⊢ a = \{f\} \to mzPoly (a) = mzPoly (\{f\})$
66		sseq1	$⊢ a = \{f\} \to (a \subseteq B \leftrightarrow \{f\} \subseteq B)$
67		reseq2	$⊢ a = \{f\} \to {d ↾}_{a} = {d ↾}_{\{f\}}$
68	67	fveq2d	$⊢ a = \{f\} \to b ({d ↾}_{a}) = b ({d ↾}_{\{f\}})$
69	68	mpteq2dv	$⊢ a = \{f\} \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}}))$
70	69	eqeq2d	$⊢ a = \{f\} \to ((g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}})))$
71	66 70	anbi12d	$⊢ a = \{f\} \to ((a \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (\{f\} \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}}))))$
72	65 71	rexeqbidv	$⊢ a = \{f\} \to (\exists b \in mzPoly (a) (a \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists b \in mzPoly (\{f\}) (\{f\} \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}}))))$
73	72	rspcev	$⊢ (\{f\} \in Fin \land \exists b \in mzPoly (\{f\}) (\{f\} \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{\{f\}})))) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
74	35 64 73	sylancr	$⊢ f \in B \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
75	74	adantl	$⊢ (⊤ \land f \in B) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
76		simplll	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to h \in Fin$
77		simprll	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to j \in Fin$
78		unfi	$⊢ (h \in Fin \land j \in Fin) \to h \cup j \in Fin$
79	76 77 78	syl2anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to h \cup j \in Fin$
80		vex	$⊢ h \in V$
81		vex	$⊢ j \in V$
82	80 81	unex	$⊢ h \cup j \in V$
83	82	a1i	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to h \cup j \in V$
84		ssun1	$⊢ h \subseteq h \cup j$
85	84	a1i	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to h \subseteq h \cup j$
86		simpllr	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to i \in mzPoly (h)$
87		mzpresrename	$⊢ (h \cup j \in V \land h \subseteq h \cup j \land i \in mzPoly (h)) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h})) \in mzPoly (h \cup j)$
88	83 85 86 87	syl3anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h})) \in mzPoly (h \cup j)$
89		ssun2	$⊢ j \subseteq h \cup j$
90	89	a1i	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to j \subseteq h \cup j$
91		simprlr	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to k \in mzPoly (j)$
92		mzpresrename	$⊢ (h \cup j \in V \land j \subseteq h \cup j \land k \in mzPoly (j)) \to (l \in (ℤ^{(h \cup j)}) ⟼ k ({l ↾}_{j})) \in mzPoly (h \cup j)$
93	83 90 91 92	syl3anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (l \in (ℤ^{(h \cup j)}) ⟼ k ({l ↾}_{j})) \in mzPoly (h \cup j)$
94		mzpaddmpt	$⊢ ((l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h})) \in mzPoly (h \cup j) \land (l \in (ℤ^{(h \cup j)}) ⟼ k ({l ↾}_{j})) \in mzPoly (h \cup j)) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) \in mzPoly (h \cup j)$
95	88 93 94	syl2anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) \in mzPoly (h \cup j)$
96		simplr	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to h \subseteq B$
97		simprr	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to j \subseteq B$
98	96 97	unssd	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to h \cup j \subseteq B$
99		ovex	$⊢ ℤ^{B} \in V$
100	99	a1i	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to ℤ^{B} \in V$
101	1	a1i	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to B \in V$
102		mzpresrename	$⊢ (B \in V \land h \subseteq B \land i \in mzPoly (h)) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \in mzPoly (B)$
103	101 96 86 102	syl3anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \in mzPoly (B)$
104		mzpf	$⊢ (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \in mzPoly (B) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) : ℤ^{B} ⟶ ℤ$
105		ffn	$⊢ (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) : ℤ^{B} ⟶ ℤ \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) Fn (ℤ^{B})$
106	103 104 105	3syl	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) Fn (ℤ^{B})$
107		mzpresrename	$⊢ (B \in V \land j \subseteq B \land k \in mzPoly (j)) \to (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) \in mzPoly (B)$
108	101 97 91 107	syl3anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) \in mzPoly (B)$
109		mzpf	$⊢ (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) \in mzPoly (B) \to (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) : ℤ^{B} ⟶ ℤ$
110		ffn	$⊢ (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) : ℤ^{B} ⟶ ℤ \to (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) Fn (ℤ^{B})$
111	108 109 110	3syl	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) Fn (ℤ^{B})$
112		ofmpteq	$⊢ (ℤ^{B} \in V \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) Fn (ℤ^{B}) \land (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) Fn (ℤ^{B})) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}) + k ({d ↾}_{j}))$
113	100 106 111 112	syl3anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}) + k ({d ↾}_{j}))$
114		elmapi	$⊢ d \in (ℤ^{B}) \to d : B ⟶ ℤ$
115		fssres	$⊢ (d : B ⟶ ℤ \land h \cup j \subseteq B) \to ({d ↾}_{(h \cup j)}) : h \cup j ⟶ ℤ$
116	114 98 115	syl2anr	$⊢ ((((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \land d \in (ℤ^{B})) \to ({d ↾}_{(h \cup j)}) : h \cup j ⟶ ℤ$
117		zex	$⊢ ℤ \in V$
118	117 82	elmap	$⊢ {d ↾}_{(h \cup j)} \in (ℤ^{(h \cup j)}) \leftrightarrow ({d ↾}_{(h \cup j)}) : h \cup j ⟶ ℤ$
119	116 118	sylibr	$⊢ ((((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \land d \in (ℤ^{B})) \to {d ↾}_{(h \cup j)} \in (ℤ^{(h \cup j)})$
120		reseq1	$⊢ l = {d ↾}_{(h \cup j)} \to {l ↾}_{h} = {({d ↾}_{(h \cup j)}) ↾}_{h}$
121	120	fveq2d	$⊢ l = {d ↾}_{(h \cup j)} \to i ({l ↾}_{h}) = i ({({d ↾}_{(h \cup j)}) ↾}_{h})$
122		reseq1	$⊢ l = {d ↾}_{(h \cup j)} \to {l ↾}_{j} = {({d ↾}_{(h \cup j)}) ↾}_{j}$
123	122	fveq2d	$⊢ l = {d ↾}_{(h \cup j)} \to k ({l ↾}_{j}) = k ({({d ↾}_{(h \cup j)}) ↾}_{j})$
124	121 123	oveq12d	$⊢ l = {d ↾}_{(h \cup j)} \to i ({l ↾}_{h}) + k ({l ↾}_{j}) = i ({({d ↾}_{(h \cup j)}) ↾}_{h}) + k ({({d ↾}_{(h \cup j)}) ↾}_{j})$
125		eqid	$⊢ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j}))$
126		ovex	$⊢ i ({({d ↾}_{(h \cup j)}) ↾}_{h}) + k ({({d ↾}_{(h \cup j)}) ↾}_{j}) \in V$
127	124 125 126	fvmpt	$⊢ {d ↾}_{(h \cup j)} \in (ℤ^{(h \cup j)}) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}) = i ({({d ↾}_{(h \cup j)}) ↾}_{h}) + k ({({d ↾}_{(h \cup j)}) ↾}_{j})$
128	119 127	syl	$⊢ ((((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \land d \in (ℤ^{B})) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}) = i ({({d ↾}_{(h \cup j)}) ↾}_{h}) + k ({({d ↾}_{(h \cup j)}) ↾}_{j})$
129		resabs1	$⊢ h \subseteq h \cup j \to {({d ↾}_{(h \cup j)}) ↾}_{h} = {d ↾}_{h}$
130	84 129	ax-mp	$⊢ {({d ↾}_{(h \cup j)}) ↾}_{h} = {d ↾}_{h}$
131	130	fveq2i	$⊢ i ({({d ↾}_{(h \cup j)}) ↾}_{h}) = i ({d ↾}_{h})$
132		resabs1	$⊢ j \subseteq h \cup j \to {({d ↾}_{(h \cup j)}) ↾}_{j} = {d ↾}_{j}$
133	89 132	ax-mp	$⊢ {({d ↾}_{(h \cup j)}) ↾}_{j} = {d ↾}_{j}$
134	133	fveq2i	$⊢ k ({({d ↾}_{(h \cup j)}) ↾}_{j}) = k ({d ↾}_{j})$
135	131 134	oveq12i	$⊢ i ({({d ↾}_{(h \cup j)}) ↾}_{h}) + k ({({d ↾}_{(h \cup j)}) ↾}_{j}) = i ({d ↾}_{h}) + k ({d ↾}_{j})$
136	128 135	eqtr2di	$⊢ ((((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \land d \in (ℤ^{B})) \to i ({d ↾}_{h}) + k ({d ↾}_{j}) = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)})$
137	136	mpteq2dva	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}) + k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}))$
138	113 137	eqtrd	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}))$
139		fveq1	$⊢ b = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) \to b ({d ↾}_{(h \cup j)}) = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)})$
140	139	mpteq2dv	$⊢ b = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}))$
141	140	eqeq2d	$⊢ b = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) \to ((d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})) \leftrightarrow (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)})))$
142	141	anbi2d	$⊢ b = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) \to ((h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))) \leftrightarrow (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}))))$
143	142	rspcev	$⊢ ((l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) \in mzPoly (h \cup j) \land (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) + k ({l ↾}_{j})) ({d ↾}_{(h \cup j)})))) \to \exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})))$
144	95 98 138 143	syl12anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to \exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})))$
145		mzpmulmpt	$⊢ ((l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h})) \in mzPoly (h \cup j) \land (l \in (ℤ^{(h \cup j)}) ⟼ k ({l ↾}_{j})) \in mzPoly (h \cup j)) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) \in mzPoly (h \cup j)$
146	88 93 145	syl2anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) \in mzPoly (h \cup j)$
147		ofmpteq	$⊢ (ℤ^{B} \in V \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) Fn (ℤ^{B}) \land (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) Fn (ℤ^{B})) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}) k ({d ↾}_{j}))$
148	100 106 111 147	syl3anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}) k ({d ↾}_{j}))$
149	121 123	oveq12d	$⊢ l = {d ↾}_{(h \cup j)} \to i ({l ↾}_{h}) k ({l ↾}_{j}) = i ({({d ↾}_{(h \cup j)}) ↾}_{h}) k ({({d ↾}_{(h \cup j)}) ↾}_{j})$
150		eqid	$⊢ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j}))$
151		ovex	$⊢ i ({({d ↾}_{(h \cup j)}) ↾}_{h}) k ({({d ↾}_{(h \cup j)}) ↾}_{j}) \in V$
152	149 150 151	fvmpt	$⊢ {d ↾}_{(h \cup j)} \in (ℤ^{(h \cup j)}) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}) = i ({({d ↾}_{(h \cup j)}) ↾}_{h}) k ({({d ↾}_{(h \cup j)}) ↾}_{j})$
153	119 152	syl	$⊢ ((((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \land d \in (ℤ^{B})) \to (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}) = i ({({d ↾}_{(h \cup j)}) ↾}_{h}) k ({({d ↾}_{(h \cup j)}) ↾}_{j})$
154	131 134	oveq12i	$⊢ i ({({d ↾}_{(h \cup j)}) ↾}_{h}) k ({({d ↾}_{(h \cup j)}) ↾}_{j}) = i ({d ↾}_{h}) k ({d ↾}_{j})$
155	153 154	eqtr2di	$⊢ ((((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \land d \in (ℤ^{B})) \to i ({d ↾}_{h}) k ({d ↾}_{j}) = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)})$
156	155	mpteq2dva	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}) k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}))$
157	148 156	eqtrd	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}))$
158		fveq1	$⊢ b = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) \to b ({d ↾}_{(h \cup j)}) = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)})$
159	158	mpteq2dv	$⊢ b = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}))$
160	159	eqeq2d	$⊢ b = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) \to ((d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})) \leftrightarrow (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)})))$
161	160	anbi2d	$⊢ b = (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) \to ((h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))) \leftrightarrow (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)}))))$
162	161	rspcev	$⊢ ((l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) \in mzPoly (h \cup j) \land (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ (l \in (ℤ^{(h \cup j)}) ⟼ i ({l ↾}_{h}) k ({l ↾}_{j})) ({d ↾}_{(h \cup j)})))) \to \exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})))$
163	146 98 157 162	syl12anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to \exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})))$
164		fveq2	$⊢ a = h \cup j \to mzPoly (a) = mzPoly (h \cup j)$
165		sseq1	$⊢ a = h \cup j \to (a \subseteq B \leftrightarrow h \cup j \subseteq B)$
166		reseq2	$⊢ a = h \cup j \to {d ↾}_{a} = {d ↾}_{(h \cup j)}$
167	166	fveq2d	$⊢ a = h \cup j \to b ({d ↾}_{a}) = b ({d ↾}_{(h \cup j)})$
168	167	mpteq2dv	$⊢ a = h \cup j \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))$
169	168	eqeq2d	$⊢ a = h \cup j \to ((d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})))$
170	165 169	anbi12d	$⊢ a = h \cup j \to ((a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))))$
171	164 170	rexeqbidv	$⊢ a = h \cup j \to (\exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))))$
172	168	eqeq2d	$⊢ a = h \cup j \to ((d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})))$
173	165 172	anbi12d	$⊢ a = h \cup j \to ((a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))))$
174	164 173	rexeqbidv	$⊢ a = h \cup j \to (\exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))))$
175	171 174	anbi12d	$⊢ a = h \cup j \to ((\exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))) \leftrightarrow (\exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))) \land \exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)})))))$
176	175	rspcev	$⊢ (h \cup j \in Fin \land (\exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))) \land \exists b \in mzPoly (h \cup j) (h \cup j \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{(h \cup j)}))))) \to \exists a \in Fin (\exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
177	79 144 163 176	syl12anc	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land h \subseteq B) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to \exists a \in Fin (\exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
178	177	adantlrr	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land j \subseteq B)) \to \exists a \in Fin (\exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
179	178	adantrrr	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to \exists a \in Fin (\exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
180		simplrr	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}))$
181		simprrr	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))$
182	180 181	oveq12d	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to f +_{f} g = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))$
183	182	eqeq1d	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to (f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
184	183	anbi2d	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to ((a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
185	184	rexbidv	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to (\exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
186	180 181	oveq12d	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to f \times_{f} g = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))$
187	186	eqeq1d	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to (f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
188	187	anbi2d	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to ((a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
189	188	rexbidv	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to (\exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
190	185 189	anbi12d	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to ((\exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))) \leftrightarrow (\exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))))$
191	190	rexbidv	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to (\exists a \in Fin (\exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))) \leftrightarrow \exists a \in Fin (\exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) +_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})) \times_{f} (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))))$
192	179 191	mpbird	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to \exists a \in Fin (\exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
193		r19.40	$⊢ \exists a \in Fin (\exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
194	192 193	syl	$⊢ (((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land ((j \in Fin \land k \in mzPoly (j)) \land (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
195	194	exp32	$⊢ ((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \to ((j \in Fin \land k \in mzPoly (j)) \to ((j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))))$
196	195	rexlimdvv	$⊢ ((h \in Fin \land i \in mzPoly (h)) \land (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \to (\exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))))$
197	196	ex	$⊢ (h \in Fin \land i \in mzPoly (h)) \to ((h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}))) \to (\exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))))$
198	197	rexlimivv	$⊢ \exists h \in Fin \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}))) \to (\exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))))$
199	198	imp	$⊢ (\exists h \in Fin \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}))) \land \exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})))) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
200	199	ad2ant2l	$⊢ ((f : ℤ^{B} ⟶ ℤ \land \exists h \in Fin \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land (g : ℤ^{B} ⟶ ℤ \land \exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
201	200	3adant1	$⊢ (⊤ \land (f : ℤ^{B} ⟶ ℤ \land \exists h \in Fin \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land (g : ℤ^{B} ⟶ ℤ \land \exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \land \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
202	201	simpld	$⊢ (⊤ \land (f : ℤ^{B} ⟶ ℤ \land \exists h \in Fin \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land (g : ℤ^{B} ⟶ ℤ \land \exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
203	201	simprd	$⊢ (⊤ \land (f : ℤ^{B} ⟶ ℤ \land \exists h \in Fin \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))) \land (g : ℤ^{B} ⟶ ℤ \land \exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
204		eqeq1	$⊢ e = (ℤ^{B}) \times \{f\} \to (e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
205	204	anbi2d	$⊢ e = (ℤ^{B}) \times \{f\} \to ((a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
206	205	2rexbidv	$⊢ e = (ℤ^{B}) \times \{f\} \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land (ℤ^{B}) \times \{f\} = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
207		eqeq1	$⊢ e = (g \in (ℤ^{B}) ⟼ g (f)) \to (e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
208	207	anbi2d	$⊢ e = (g \in (ℤ^{B}) ⟼ g (f)) \to ((a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
209	208	2rexbidv	$⊢ e = (g \in (ℤ^{B}) ⟼ g (f)) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land (g \in (ℤ^{B}) ⟼ g (f)) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
210		eqeq1	$⊢ e = f \to (e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
211	210	anbi2d	$⊢ e = f \to ((a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
212	211	2rexbidv	$⊢ e = f \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
213		fveq2	$⊢ a = h \to mzPoly (a) = mzPoly (h)$
214		sseq1	$⊢ a = h \to (a \subseteq B \leftrightarrow h \subseteq B)$
215		reseq2	$⊢ a = h \to {d ↾}_{a} = {d ↾}_{h}$
216	215	fveq2d	$⊢ a = h \to b ({d ↾}_{a}) = b ({d ↾}_{h})$
217	216	mpteq2dv	$⊢ a = h \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{h}))$
218	217	eqeq2d	$⊢ a = h \to (f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{h})))$
219	214 218	anbi12d	$⊢ a = h \to ((a \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{h}))))$
220	213 219	rexeqbidv	$⊢ a = h \to (\exists b \in mzPoly (a) (a \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists b \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{h}))))$
221		fveq1	$⊢ b = i \to b ({d ↾}_{h}) = i ({d ↾}_{h})$
222	221	mpteq2dv	$⊢ b = i \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{h})) = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}))$
223	222	eqeq2d	$⊢ b = i \to (f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{h})) \leftrightarrow f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))$
224	223	anbi2d	$⊢ b = i \to ((h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{h}))) \leftrightarrow (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}))))$
225	224	cbvrexvw	$⊢ \exists b \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{h}))) \leftrightarrow \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))$
226	220 225	bitrdi	$⊢ a = h \to (\exists b \in mzPoly (a) (a \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}))))$
227	226	cbvrexvw	$⊢ \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists h \in Fin \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h})))$
228	212 227	bitrdi	$⊢ e = f \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists h \in Fin \exists i \in mzPoly (h) (h \subseteq B \land f = (d \in (ℤ^{B}) ⟼ i ({d ↾}_{h}))))$
229		eqeq1	$⊢ e = g \to (e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
230	229	anbi2d	$⊢ e = g \to ((a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
231	230	2rexbidv	$⊢ e = g \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
232		fveq2	$⊢ a = j \to mzPoly (a) = mzPoly (j)$
233		sseq1	$⊢ a = j \to (a \subseteq B \leftrightarrow j \subseteq B)$
234		reseq2	$⊢ a = j \to {d ↾}_{a} = {d ↾}_{j}$
235	234	fveq2d	$⊢ a = j \to b ({d ↾}_{a}) = b ({d ↾}_{j})$
236	235	mpteq2dv	$⊢ a = j \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{j}))$
237	236	eqeq2d	$⊢ a = j \to (g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{j})))$
238	233 237	anbi12d	$⊢ a = j \to ((a \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{j}))))$
239	232 238	rexeqbidv	$⊢ a = j \to (\exists b \in mzPoly (a) (a \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists b \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{j}))))$
240		fveq1	$⊢ b = k \to b ({d ↾}_{j}) = k ({d ↾}_{j})$
241	240	mpteq2dv	$⊢ b = k \to (d \in (ℤ^{B}) ⟼ b ({d ↾}_{j})) = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))$
242	241	eqeq2d	$⊢ b = k \to (g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{j})) \leftrightarrow g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})))$
243	242	anbi2d	$⊢ b = k \to ((j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{j}))) \leftrightarrow (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))$
244	243	cbvrexvw	$⊢ \exists b \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{j}))) \leftrightarrow \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})))$
245	239 244	bitrdi	$⊢ a = j \to (\exists b \in mzPoly (a) (a \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))$
246	245	cbvrexvw	$⊢ \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j})))$
247	231 246	bitrdi	$⊢ e = g \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists j \in Fin \exists k \in mzPoly (j) (j \subseteq B \land g = (d \in (ℤ^{B}) ⟼ k ({d ↾}_{j}))))$
248		eqeq1	$⊢ e = f +_{f} g \to (e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
249	248	anbi2d	$⊢ e = f +_{f} g \to ((a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
250	249	2rexbidv	$⊢ e = f +_{f} g \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f +_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
251		eqeq1	$⊢ e = f \times_{f} g \to (e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
252	251	anbi2d	$⊢ e = f \times_{f} g \to ((a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
253	252	2rexbidv	$⊢ e = f \times_{f} g \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land f \times_{f} g = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
254		eqeq1	$⊢ e = A \to (e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow A = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
255	254	anbi2d	$⊢ e = A \to ((a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land A = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
256	255	2rexbidv	$⊢ e = A \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land e = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land A = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))))$
257	34 75 202 203 206 209 228 247 250 253 256	mzpindd	$⊢ (⊤ \land A \in mzPoly (B)) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land A = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
258	2 257	mpan	$⊢ A \in mzPoly (B) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land A = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})))$
259		reseq1	$⊢ d = c \to {d ↾}_{a} = {c ↾}_{a}$
260	259	fveq2d	$⊢ d = c \to b ({d ↾}_{a}) = b ({c ↾}_{a})$
261	260	cbvmptv	$⊢ (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) = (c \in (ℤ^{B}) ⟼ b ({c ↾}_{a}))$
262	261	eqeq2i	$⊢ A = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a})) \leftrightarrow A = (c \in (ℤ^{B}) ⟼ b ({c ↾}_{a}))$
263	262	anbi2i	$⊢ (a \subseteq B \land A = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow (a \subseteq B \land A = (c \in (ℤ^{B}) ⟼ b ({c ↾}_{a})))$
264	263	2rexbii	$⊢ \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land A = (d \in (ℤ^{B}) ⟼ b ({d ↾}_{a}))) \leftrightarrow \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land A = (c \in (ℤ^{B}) ⟼ b ({c ↾}_{a})))$
265	258 264	sylib	$⊢ A \in mzPoly (B) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq B \land A = (c \in (ℤ^{B}) ⟼ b ({c ↾}_{a})))$

Metamath Proof Explorer

Theorem mzpcompact2lem

Proof