mzpcompact2lem - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mzpcompact2lem		Structured version Visualization version GIF version

Theorem mzpcompact2lem 38833

Description: Lemma for mzpcompact2 38834. (Contributed by Stefan O'Rear, 9-Oct-2014.)

**Hypothesis**
Ref	Expression
mzpcompact2lem.i	⊢ 𝐵 ∈ V

**Assertion**
Ref	Expression
mzpcompact2lem	⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))

Distinct variable groups: 𝐴,𝑎,𝑏 𝐵,𝑎,𝑏,𝑐 Allowed substitution hint: 𝐴(𝑐)

Proof of Theorem mzpcompact2lem Dummy variables 𝑑 𝑒 𝑓 𝑔 ℎ 𝑖 𝑗 𝑘 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tru 1526	. . 3 ⊢ ⊤
2		0fin 8592	. . . . . 6 ⊢ ∅ ∈ Fin
3		0ex 5102	. . . . . . . 8 ⊢ ∅ ∈ V
4		mzpconst 38817	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑_𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅))
5	3, 4	mpan 686	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅))
6		0ss 4270	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
7	6	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → 𝑑 ∈ (ℤ ↑_𝑚 𝐵))
9		elmapssres 8281	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑_𝑚 ∅))
10	8, 6, 9	sylancl 586	. . . . . . . . . 10 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑_𝑚 ∅))
11		vex 3440	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
12	11	fvconst2 6833	. . . . . . . . . 10 ⊢ ((𝑑 ↾ ∅) ∈ (ℤ ↑_𝑚 ∅) → (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
13	10, 12	syl 17	. . . . . . . . 9 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
14	13	mpteq2dva 5055	. . . . . . . 8 ⊢ (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ 𝑓))
15		fconstmpt 5500	. . . . . . . 8 ⊢ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ 𝑓)
16	14, 15	syl6reqr 2850	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17		fveq1 6537	. . . . . . . . . . 11 ⊢ (𝑏 = ((ℤ ↑_𝑚 ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)))
18	17	mpteq2dv 5056	. . . . . . . . . 10 ⊢ (𝑏 = ((ℤ ↑_𝑚 ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))
19	18	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑏 = ((ℤ ↑_𝑚 ∅) × {𝑓}) → (((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
20	19	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = ((ℤ ↑_𝑚 ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
21	20	rspcev 3559	. . . . . . 7 ⊢ ((((ℤ ↑_𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
22	5, 7, 16, 21	syl12anc 833	. . . . . 6 ⊢ (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23		fveq2 6538	. . . . . . . 8 ⊢ (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24		sseq1 3913	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵))
25		reseq2 5729	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ∅))
26	25	fveq2d 6542	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
27	26	mpteq2dv 5056	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
28	27	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
29	24, 28	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
30	23, 29	rexeqbidv 3362	. . . . . . 7 ⊢ (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
31	30	rspcev 3559	. . . . . 6 ⊢ ((∅ ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
32	2, 22, 31	sylancr 587	. . . . 5 ⊢ (𝑓 ∈ ℤ → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
33	32	adantl 482	. . . 4 ⊢ ((⊤ ∧ 𝑓 ∈ ℤ) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
34		snfi 8442	. . . . . 6 ⊢ {𝑓} ∈ Fin
35		snex 5223	. . . . . . . . 9 ⊢ {𝑓} ∈ V
36		vsnid 4507	. . . . . . . . 9 ⊢ 𝑓 ∈ {𝑓}
37		mzpproj 38819	. . . . . . . . 9 ⊢ (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
38	35, 36, 37	mp2an 688	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓})
39	38	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
40		snssi 4648	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → {𝑓} ⊆ 𝐵)
41		fveq1 6537	. . . . . . . . 9 ⊢ (𝑔 = 𝑑 → (𝑔‘𝑓) = (𝑑‘𝑓))
42	41	cbvmptv 5061	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑑‘𝑓))
43		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → 𝑑 ∈ (ℤ ↑_𝑚 𝐵))
44		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → 𝑓 ∈ 𝐵)
45	44	snssd 4649	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → {𝑓} ⊆ 𝐵)
46		elmapssres 8281	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_𝑚 {𝑓}))
47	43, 45, 46	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_𝑚 {𝑓}))
48		fveq1 6537	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔‘𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49		eqid 2795	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))
50		fvex 6551	. . . . . . . . . . . 12 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
51	48, 49, 50	fvmpt 6635	. . . . . . . . . . 11 ⊢ ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑_𝑚 {𝑓}) → ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
52	47, 51	syl 17	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53		fvres 6557	. . . . . . . . . . 11 ⊢ (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓))
54	36, 53	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓)
55	52, 54	syl6req 2848	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑‘𝑓) = ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
56	55	mpteq2dva 5055	. . . . . . . 8 ⊢ (𝑓 ∈ 𝐵 → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑑‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
57	42, 56	syl5eq 2843	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
58		fveq1 6537	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
59	58	mpteq2dv 5056	. . . . . . . . . 10 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
60	59	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) → ((𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))))
61	60	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))))
62	61	rspcev 3559	. . . . . . 7 ⊢ (((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
63	39, 40, 57, 62	syl12anc 833	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64		fveq2 6538	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65		sseq1 3913	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → (𝑎 ⊆ 𝐵 ↔ {𝑓} ⊆ 𝐵))
66		reseq2 5729	. . . . . . . . . . . 12 ⊢ (𝑎 = {𝑓} → (𝑑 ↾ 𝑎) = (𝑑 ↾ {𝑓}))
67	66	fveq2d 6542	. . . . . . . . . . 11 ⊢ (𝑎 = {𝑓} → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
68	67	mpteq2dv 5056	. . . . . . . . . 10 ⊢ (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
69	68	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
70	65, 69	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → ((𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
71	64, 70	rexeqbidv 3362	. . . . . . 7 ⊢ (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
72	71	rspcev 3559	. . . . . 6 ⊢ (({𝑓} ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
73	34, 63, 72	sylancr 587	. . . . 5 ⊢ (𝑓 ∈ 𝐵 → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
74	73	adantl 482	. . . 4 ⊢ ((⊤ ∧ 𝑓 ∈ 𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
75		simplll 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ∈ Fin)
76		simprll 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ∈ Fin)
77		unfi 8631	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ ∈ Fin ∧ 𝑗 ∈ Fin) → (ℎ ∪ 𝑗) ∈ Fin)
78	75, 76, 77	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ Fin)
79		vex 3440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℎ ∈ V
80		vex 3440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑗 ∈ V
81	79, 80	unex 7326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ∪ 𝑗) ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ V)
83		ssun1 4069	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℎ ⊆ (ℎ ∪ 𝑗)
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ (ℎ ∪ 𝑗))
85		simpllr 772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑖 ∈ (mzPoly‘ℎ))
86		mzpresrename 38832	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ ℎ ⊆ (ℎ ∪ 𝑗) ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
87	82, 84, 85, 86	syl3anc 1364	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
88		ssun2 4070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑗 ⊆ (ℎ ∪ 𝑗)
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ (ℎ ∪ 𝑗))
90		simprlr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91		mzpresrename 38832	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ 𝑗 ⊆ (ℎ ∪ 𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
92	82, 89, 90, 91	syl3anc 1364	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
93		mzpaddmpt 38823	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
94	87, 92, 93	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
95		simplr 765	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ 𝐵)
96		simprr 769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ 𝐵)
97	95, 96	unssd 4083	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ⊆ 𝐵)
98		ovex 7048	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℤ ↑_𝑚 𝐵) ∈ V
99	98	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℤ ↑_𝑚 𝐵) ∈ V)
100		mzpcompact2lem.i	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 ∈ V
101	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝐵 ∈ V)
102		mzpresrename 38832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ ℎ ⊆ 𝐵 ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
103	101, 95, 85, 102	syl3anc 1364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
104		mzpf 38818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_𝑚 𝐵)⟶ℤ)
105		ffn 6382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_𝑚 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_𝑚 𝐵))
106	103, 104, 105	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_𝑚 𝐵))
107		mzpresrename 38832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ 𝑗 ⊆ 𝐵 ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
108	101, 96, 90, 107	syl3anc 1364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
109		mzpf 38818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_𝑚 𝐵)⟶ℤ)
110		ffn 6382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_𝑚 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_𝑚 𝐵))
111	108, 109, 110	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_𝑚 𝐵))
112		ofmpteq 7286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_𝑚 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_𝑚 𝐵) ∧ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_𝑚 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
113	99, 106, 111, 112	syl3anc 1364	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
114		elmapi 8278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) → 𝑑:𝐵⟶ℤ)
115		fssres 6412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑑:𝐵⟶ℤ ∧ (ℎ ∪ 𝑗) ⊆ 𝐵) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
116	114, 97, 115	syl2anr 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
117		zex 11838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℤ ∈ V
118	117, 81	elmap 8285	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↔ (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
119	116, 118	sylibr 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)))
120		reseq1 5728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ ℎ) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ))
121	120	fveq2d 6542	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑖‘(𝑙 ↾ ℎ)) = (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)))
122		reseq1 5728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ 𝑗) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))
123	122	fveq2d 6542	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑘‘(𝑙 ↾ 𝑗)) = (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)))
124	121, 123	oveq12d 7034	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
125		eqid 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))
126		ovex 7048	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
127	124, 125, 126	fvmpt 6635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
128	119, 127	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
129		resabs1 5764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ))
130	83, 129	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ)
131	130	fveq2i 6541	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ))
132		resabs1 5764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗))
133	88, 132	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗)
134	133	fveq2i 6541	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗))
135	131, 134	oveq12i 7028	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))
136	128, 135	syl6req 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
137	136	mpteq2dva 5055	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
138	113, 137	eqtrd 2831	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
139		fveq1 6537	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
140	139	mpteq2dv 5056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
141	140	eqeq2d 2805	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
142	141	anbi2d 628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
143	142	rspcev 3559	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
144	94, 97, 138, 143	syl12anc 833	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
145		mzpmulmpt 38824	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
146	87, 92, 145	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
147		ofmpteq 7286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_𝑚 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_𝑚 𝐵) ∧ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_𝑚 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
148	99, 106, 111, 147	syl3anc 1364	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
149	121, 123	oveq12d 7034	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
150		eqid 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))
151		ovex 7048	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
152	149, 150, 151	fvmpt 6635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
153	119, 152	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
154	131, 134	oveq12i 7028	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))
155	153, 154	syl6req 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
156	155	mpteq2dva 5055	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
157	148, 156	eqtrd 2831	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
158		fveq1 6537	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
159	158	mpteq2dv 5056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
160	159	eqeq2d 2805	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
161	160	anbi2d 628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
162	161	rspcev 3559	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
163	146, 97, 157, 162	syl12anc 833	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
164		fveq2 6538	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (mzPoly‘𝑎) = (mzPoly‘(ℎ ∪ 𝑗)))
165		sseq1 3913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑎 ⊆ 𝐵 ↔ (ℎ ∪ 𝑗) ⊆ 𝐵))
166		reseq2 5729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ↾ 𝑎) = (𝑑 ↾ (ℎ ∪ 𝑗)))
167	166	fveq2d 6542	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))
168	167	mpteq2dv 5056	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
169	168	eqeq2d 2805	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
170	165, 169	anbi12d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
171	164, 170	rexeqbidv 3362	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
172	168	eqeq2d 2805	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
173	165, 172	anbi12d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
174	164, 173	rexeqbidv 3362	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
175	171, 174	anbi12d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))))
176	175	rspcev 3559	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ ∪ 𝑗) ∈ Fin ∧ (∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
177	78, 144, 163, 176	syl12anc 833	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
178	177	adantlrr 717	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
179	178	adantrrr 721	. . . . . . . . . . . . . 14 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
180		simplrr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
181		simprrr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
182	180, 181	oveq12d 7034	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_𝑓 + 𝑔) = ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
183	182	eqeq1d 2797	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
184	183	anbi2d 628	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
185	184	rexbidv 3260	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
186	180, 181	oveq12d 7034	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_𝑓 · 𝑔) = ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
187	186	eqeq1d 2797	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
188	187	anbi2d 628	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
189	188	rexbidv 3260	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
190	185, 189	anbi12d 630	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
191	190	rexbidv 3260	. . . . . . . . . . . . . 14 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
192	179, 191	mpbird 258	. . . . . . . . . . . . 13 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
193		r19.40 3307	. . . . . . . . . . . . 13 ⊢ (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
194	192, 193	syl 17	. . . . . . . . . . . 12 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
195	194	exp32 421	. . . . . . . . . . 11 ⊢ (((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) → ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) → ((𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))))
196	195	rexlimdvv 3256	. . . . . . . . . 10 ⊢ (((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
197	196	ex 413	. . . . . . . . 9 ⊢ ((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) → ((ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))))
198	197	rexlimivv 3255	. . . . . . . 8 ⊢ (∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
199	198	imp 407	. . . . . . 7 ⊢ ((∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
200	199	ad2ant2l 742	. . . . . 6 ⊢ (((𝑓:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
201	200	3adant1 1123	. . . . 5 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
202	201	simpld 495	. . . 4 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
203	201	simprd 496	. . . 4 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
204		eqeq1 2799	. . . . . 6 ⊢ (𝑒 = ((ℤ ↑_𝑚 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
205	204	anbi2d 628	. . . . 5 ⊢ (𝑒 = ((ℤ ↑_𝑚 𝐵) × {𝑓}) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
206	205	2rexbidv 3263	. . . 4 ⊢ (𝑒 = ((ℤ ↑_𝑚 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
207		eqeq1 2799	. . . . . 6 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
208	207	anbi2d 628	. . . . 5 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
209	208	2rexbidv 3263	. . . 4 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
210		eqeq1 2799	. . . . . . 7 ⊢ (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
211	210	anbi2d 628	. . . . . 6 ⊢ (𝑒 = 𝑓 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
212	211	2rexbidv 3263	. . . . 5 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
213		fveq2 6538	. . . . . . . 8 ⊢ (𝑎 = ℎ → (mzPoly‘𝑎) = (mzPoly‘ℎ))
214		sseq1 3913	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑎 ⊆ 𝐵 ↔ ℎ ⊆ 𝐵))
215		reseq2 5729	. . . . . . . . . . . 12 ⊢ (𝑎 = ℎ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ℎ))
216	215	fveq2d 6542	. . . . . . . . . . 11 ⊢ (𝑎 = ℎ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ℎ)))
217	216	mpteq2dv 5056	. . . . . . . . . 10 ⊢ (𝑎 = ℎ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))
218	217	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))))
219	214, 218	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = ℎ → ((𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
220	213, 219	rexeqbidv 3362	. . . . . . 7 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
221		fveq1 6537	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑖 → (𝑏‘(𝑑 ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ)))
222	221	mpteq2dv 5056	. . . . . . . . . 10 ⊢ (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
223	222	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
224	223	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = 𝑖 → ((ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
225	224	cbvrexv 3404	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
226	220, 225	syl6bb 288	. . . . . 6 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
227	226	cbvrexv 3404	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
228	212, 227	syl6bb 288	. . . 4 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
229		eqeq1 2799	. . . . . . 7 ⊢ (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
230	229	anbi2d 628	. . . . . 6 ⊢ (𝑒 = 𝑔 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
231	230	2rexbidv 3263	. . . . 5 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
232		fveq2 6538	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233		sseq1 3913	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑎 ⊆ 𝐵 ↔ 𝑗 ⊆ 𝐵))
234		reseq2 5729	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑗 → (𝑑 ↾ 𝑎) = (𝑑 ↾ 𝑗))
235	234	fveq2d 6542	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑗 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ 𝑗)))
236	235	mpteq2dv 5056	. . . . . . . . . 10 ⊢ (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))
237	236	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))))
238	233, 237	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → ((𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
239	232, 238	rexeqbidv 3362	. . . . . . 7 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
240		fveq1 6537	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑘 → (𝑏‘(𝑑 ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗)))
241	240	mpteq2dv 5056	. . . . . . . . . 10 ⊢ (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
242	241	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
243	242	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = 𝑘 → ((𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
244	243	cbvrexv 3404	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
245	239, 244	syl6bb 288	. . . . . 6 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
246	245	cbvrexv 3404	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
247	231, 246	syl6bb 288	. . . 4 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
248		eqeq1 2799	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_𝑓 + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
249	248	anbi2d 628	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_𝑓 + 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
250	249	2rexbidv 3263	. . . 4 ⊢ (𝑒 = (𝑓 ∘_𝑓 + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
251		eqeq1 2799	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_𝑓 · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
252	251	anbi2d 628	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_𝑓 · 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
253	252	2rexbidv 3263	. . . 4 ⊢ (𝑒 = (𝑓 ∘_𝑓 · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
254		eqeq1 2799	. . . . . 6 ⊢ (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
255	254	anbi2d 628	. . . . 5 ⊢ (𝑒 = 𝐴 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
256	255	2rexbidv 3263	. . . 4 ⊢ (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
257	33, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256	mzpindd 38828	. . 3 ⊢ ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
258	1, 257	mpan 686	. 2 ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
259		reseq1 5728	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑑 ↾ 𝑎) = (𝑐 ↾ 𝑎))
260	259	fveq2d 6542	. . . . . 6 ⊢ (𝑑 = 𝑐 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑐 ↾ 𝑎)))
261	260	cbvmptv 5061	. . . . 5 ⊢ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))
262	261	eqeq2i 2807	. . . 4 ⊢ (𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎))))
263	262	anbi2i 622	. . 3 ⊢ ((𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
264	263	2rexbii 3212	. 2 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
265	258, 264	sylib 219	1 ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 = wceq 1522 ⊤wtru 1523 ∈ wcel 2081 ∃wrex 3106 Vcvv 3437 ∪ cun 3857 ⊆ wss 3859 ∅c0 4211 {csn 4472 ↦ cmpt 5041 × cxp 5441 ↾ cres 5445 Fn wfn 6220 ⟶wf 6221 ‘cfv 6225 (class class class)co 7016 ∘_𝑓 cof 7265 ↑_𝑚 cmap 8256 Fincfn 8357 + caddc 10386 · cmul 10388 ℤcz 11829 mzPolycmzp 38804

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-cnex 10439 ax-resscn 10440 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-mulcom 10447 ax-addass 10448 ax-mulass 10449 ax-distr 10450 ax-i2m1 10451 ax-1ne0 10452 ax-1rid 10453 ax-rnegex 10454 ax-rrecex 10455 ax-cnre 10456 ax-pre-lttri 10457 ax-pre-lttrn 10458 ax-pre-ltadd 10459 ax-pre-mulgt0 10460

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-int 4783 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-riota 6977 df-ov 7019 df-oprab 7020 df-mpo 7021 df-of 7267 df-om 7437 df-1st 7545 df-2nd 7546 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-1o 7953 df-oadd 7957 df-er 8139 df-map 8258 df-en 8358 df-dom 8359 df-sdom 8360 df-fin 8361 df-pnf 10523 df-mnf 10524 df-xr 10525 df-ltxr 10526 df-le 10527 df-sub 10719 df-neg 10720 df-nn 11487 df-n0 11746 df-z 11830 df-mzpcl 38805 df-mzp 38806

This theorem is referenced by: mzpcompact2 38834

W3C validator