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 37314

Description: Lemma for mzpcompact2 37315. (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 1487	. . 3 ⊢ ⊤
2		0fin 8188	. . . . . 6 ⊢ ∅ ∈ Fin
3		0ex 4790	. . . . . . . 8 ⊢ ∅ ∈ V
4		mzpconst 37298	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑_𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅))
5	3, 4	mpan 706	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅))
6		0ss 3972	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
7	6	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8		simpr 477	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → 𝑑 ∈ (ℤ ↑_𝑚 𝐵))
9		elmapssres 7882	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑_𝑚 ∅))
10	8, 6, 9	sylancl 694	. . . . . . . . . 10 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑_𝑚 ∅))
11		vex 3203	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
12	11	fvconst2 6469	. . . . . . . . . 10 ⊢ ((𝑑 ↾ ∅) ∈ (ℤ ↑_𝑚 ∅) → (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
13	10, 12	syl 17	. . . . . . . . 9 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
14	13	mpteq2dva 4744	. . . . . . . 8 ⊢ (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ 𝑓))
15		fconstmpt 5163	. . . . . . . 8 ⊢ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ 𝑓)
16	14, 15	syl6reqr 2675	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17		fveq1 6190	. . . . . . . . . . 11 ⊢ (𝑏 = ((ℤ ↑_𝑚 ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)))
18	17	mpteq2dv 4745	. . . . . . . . . 10 ⊢ (𝑏 = ((ℤ ↑_𝑚 ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))
19	18	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑏 = ((ℤ ↑_𝑚 ∅) × {𝑓}) → (((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
20	19	anbi2d 740	. . . . . . . 8 ⊢ (𝑏 = ((ℤ ↑_𝑚 ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
21	20	rspcev 3309	. . . . . . 7 ⊢ ((((ℤ ↑_𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (((ℤ ↑_𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
22	5, 7, 16, 21	syl12anc 1324	. . . . . 6 ⊢ (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23		fveq2 6191	. . . . . . . 8 ⊢ (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24		sseq1 3626	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵))
25		reseq2 5391	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ∅))
26	25	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
27	26	mpteq2dv 4745	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
28	27	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
29	24, 28	anbi12d 747	. . . . . . . 8 ⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
30	23, 29	rexeqbidv 3153	. . . . . . 7 ⊢ (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
31	30	rspcev 3309	. . . . . 6 ⊢ ((∅ ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
32	2, 22, 31	sylancr 695	. . . . 5 ⊢ (𝑓 ∈ ℤ → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
33	32	adantl 482	. . . 4 ⊢ ((⊤ ∧ 𝑓 ∈ ℤ) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
34		snfi 8038	. . . . . 6 ⊢ {𝑓} ∈ Fin
35		snex 4908	. . . . . . . . 9 ⊢ {𝑓} ∈ V
36		vsnid 4209	. . . . . . . . 9 ⊢ 𝑓 ∈ {𝑓}
37		mzpproj 37300	. . . . . . . . 9 ⊢ (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
38	35, 36, 37	mp2an 708	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓})
39	38	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
40		snssi 4339	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → {𝑓} ⊆ 𝐵)
41		fveq1 6190	. . . . . . . . 9 ⊢ (𝑔 = 𝑑 → (𝑔‘𝑓) = (𝑑‘𝑓))
42	41	cbvmptv 4750	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑑‘𝑓))
43		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → 𝑑 ∈ (ℤ ↑_𝑚 𝐵))
44		simpl 473	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → 𝑓 ∈ 𝐵)
45	44	snssd 4340	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → {𝑓} ⊆ 𝐵)
46		elmapssres 7882	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_𝑚 {𝑓}))
47	43, 45, 46	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_𝑚 {𝑓}))
48		fveq1 6190	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔‘𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49		eqid 2622	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))
50		fvex 6201	. . . . . . . . . . . 12 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
51	48, 49, 50	fvmpt 6282	. . . . . . . . . . 11 ⊢ ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑_𝑚 {𝑓}) → ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
52	47, 51	syl 17	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53		fvres 6207	. . . . . . . . . . 11 ⊢ (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓))
54	36, 53	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓)
55	52, 54	syl6req 2673	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑‘𝑓) = ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
56	55	mpteq2dva 4744	. . . . . . . 8 ⊢ (𝑓 ∈ 𝐵 → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑑‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
57	42, 56	syl5eq 2668	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
58		fveq1 6190	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
59	58	mpteq2dv 4745	. . . . . . . . . 10 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
60	59	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) → ((𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))))
61	60	anbi2d 740	. . . . . . . 8 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))))
62	61	rspcev 3309	. . . . . . 7 ⊢ (((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_𝑚 {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
63	39, 40, 57, 62	syl12anc 1324	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64		fveq2 6191	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65		sseq1 3626	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → (𝑎 ⊆ 𝐵 ↔ {𝑓} ⊆ 𝐵))
66		reseq2 5391	. . . . . . . . . . . 12 ⊢ (𝑎 = {𝑓} → (𝑑 ↾ 𝑎) = (𝑑 ↾ {𝑓}))
67	66	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑎 = {𝑓} → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
68	67	mpteq2dv 4745	. . . . . . . . . 10 ⊢ (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
69	68	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
70	65, 69	anbi12d 747	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → ((𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
71	64, 70	rexeqbidv 3153	. . . . . . 7 ⊢ (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
72	71	rspcev 3309	. . . . . 6 ⊢ (({𝑓} ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
73	34, 63, 72	sylancr 695	. . . . 5 ⊢ (𝑓 ∈ 𝐵 → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
74	73	adantl 482	. . . 4 ⊢ ((⊤ ∧ 𝑓 ∈ 𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
75		simplll 798	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ∈ Fin)
76		simprll 802	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ∈ Fin)
77		unfi 8227	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ ∈ Fin ∧ 𝑗 ∈ Fin) → (ℎ ∪ 𝑗) ∈ Fin)
78	75, 76, 77	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ Fin)
79		vex 3203	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℎ ∈ V
80		vex 3203	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑗 ∈ V
81	79, 80	unex 6956	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ∪ 𝑗) ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ V)
83		ssun1 3776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℎ ⊆ (ℎ ∪ 𝑗)
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ (ℎ ∪ 𝑗))
85		simpllr 799	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑖 ∈ (mzPoly‘ℎ))
86		mzpresrename 37313	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ ℎ ⊆ (ℎ ∪ 𝑗) ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
87	82, 84, 85, 86	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
88		ssun2 3777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑗 ⊆ (ℎ ∪ 𝑗)
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ (ℎ ∪ 𝑗))
90		simprlr 803	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91		mzpresrename 37313	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ 𝑗 ⊆ (ℎ ∪ 𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
92	82, 89, 90, 91	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
93		mzpaddmpt 37304	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
94	87, 92, 93	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
95		simplr 792	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ 𝐵)
96		simprr 796	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ 𝐵)
97	95, 96	unssd 3789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ⊆ 𝐵)
98		ovex 6678	. . . . . . . . . . . . . . . . . . . . 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 37313	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ ℎ ⊆ 𝐵 ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
103	101, 95, 85, 102	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
104		mzpf 37299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_𝑚 𝐵)⟶ℤ)
105		ffn 6045	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_𝑚 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_𝑚 𝐵))
106	103, 104, 105	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_𝑚 𝐵))
107		mzpresrename 37313	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ 𝑗 ⊆ 𝐵 ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
108	101, 96, 90, 107	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
109		mzpf 37299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_𝑚 𝐵)⟶ℤ)
110		ffn 6045	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_𝑚 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_𝑚 𝐵))
111	108, 109, 110	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_𝑚 𝐵))
112		ofmpteq 6916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_𝑚 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_𝑚 𝐵) ∧ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_𝑚 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
113	99, 106, 111, 112	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
114		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) → 𝑑:𝐵⟶ℤ)
115		fssres 6070	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑑:𝐵⟶ℤ ∧ (ℎ ∪ 𝑗) ⊆ 𝐵) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
116	114, 97, 115	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
117		zex 11386	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℤ ∈ V
118	117, 81	elmap 7886	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↔ (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
119	116, 118	sylibr 224	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)))
120		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ ℎ) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ))
121	120	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑖‘(𝑙 ↾ ℎ)) = (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)))
122		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ 𝑗) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))
123	122	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑘‘(𝑙 ↾ 𝑗)) = (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)))
124	121, 123	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
125		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))
126		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
127	124, 125, 126	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
128	119, 127	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
129		resabs1 5427	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ))
130	83, 129	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ)
131	130	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ))
132		resabs1 5427	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗))
133	88, 132	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗)
134	133	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗))
135	131, 134	oveq12i 6662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))
136	128, 135	syl6req 2673	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
137	136	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
138	113, 137	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
139		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
140	139	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
141	140	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
142	141	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
143	142	rspcev 3309	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
144	94, 97, 138, 143	syl12anc 1324	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
145		mzpmulmpt 37305	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
146	87, 92, 145	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
147		ofmpteq 6916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_𝑚 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_𝑚 𝐵) ∧ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_𝑚 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
148	99, 106, 111, 147	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
149	121, 123	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
150		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))
151		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
152	149, 150, 151	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
153	119, 152	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
154	131, 134	oveq12i 6662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))
155	153, 154	syl6req 2673	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_𝑚 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
156	155	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
157	148, 156	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
158		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
159	158	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
160	159	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
161	160	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
162	161	rspcev 3309	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_𝑚 (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
163	146, 97, 157, 162	syl12anc 1324	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
164		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (mzPoly‘𝑎) = (mzPoly‘(ℎ ∪ 𝑗)))
165		sseq1 3626	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑎 ⊆ 𝐵 ↔ (ℎ ∪ 𝑗) ⊆ 𝐵))
166		reseq2 5391	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ↾ 𝑎) = (𝑑 ↾ (ℎ ∪ 𝑗)))
167	166	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))
168	167	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
169	168	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
170	165, 169	anbi12d 747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
171	164, 170	rexeqbidv 3153	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
172	168	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
173	165, 172	anbi12d 747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
174	164, 173	rexeqbidv 3153	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
175	171, 174	anbi12d 747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))))
176	175	rspcev 3309	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ ∪ 𝑗) ∈ Fin ∧ (∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
177	78, 144, 163, 176	syl12anc 1324	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
178	177	adantlrr 757	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
179	178	adantrrr 761	. . . . . . . . . . . . . 14 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
180		simplrr 801	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
181		simprrr 805	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
182	180, 181	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_𝑓 + 𝑔) = ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
183	182	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
184	183	anbi2d 740	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
185	184	rexbidv 3052	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
186	180, 181	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_𝑓 · 𝑔) = ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
187	186	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
188	187	anbi2d 740	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
189	188	rexbidv 3052	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
190	185, 189	anbi12d 747	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
191	190	rexbidv 3052	. . . . . . . . . . . . . 14 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 + (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_𝑓 · (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
192	179, 191	mpbird 247	. . . . . . . . . . . . 13 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
193		r19.40 3088	. . . . . . . . . . . . 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 631	. . . . . . . . . . 11 ⊢ (((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) → ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) → ((𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))))
196	195	rexlimdvv 3037	. . . . . . . . . 10 ⊢ (((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
197	196	ex 450	. . . . . . . . 9 ⊢ ((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) → ((ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))))
198	197	rexlimivv 3036	. . . . . . . 8 ⊢ (∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
199	198	imp 445	. . . . . . 7 ⊢ ((∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
200	199	ad2ant2l 782	. . . . . 6 ⊢ (((𝑓:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
201	200	3adant1 1079	. . . . 5 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
202	201	simpld 475	. . . 4 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
203	201	simprd 479	. . . 4 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
204		eqeq1 2626	. . . . . 6 ⊢ (𝑒 = ((ℤ ↑_𝑚 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
205	204	anbi2d 740	. . . . 5 ⊢ (𝑒 = ((ℤ ↑_𝑚 𝐵) × {𝑓}) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
206	205	2rexbidv 3057	. . . 4 ⊢ (𝑒 = ((ℤ ↑_𝑚 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
207		eqeq1 2626	. . . . . 6 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
208	207	anbi2d 740	. . . . 5 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
209	208	2rexbidv 3057	. . . 4 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
210		eqeq1 2626	. . . . . . 7 ⊢ (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
211	210	anbi2d 740	. . . . . 6 ⊢ (𝑒 = 𝑓 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
212	211	2rexbidv 3057	. . . . 5 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
213		fveq2 6191	. . . . . . . 8 ⊢ (𝑎 = ℎ → (mzPoly‘𝑎) = (mzPoly‘ℎ))
214		sseq1 3626	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑎 ⊆ 𝐵 ↔ ℎ ⊆ 𝐵))
215		reseq2 5391	. . . . . . . . . . . 12 ⊢ (𝑎 = ℎ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ℎ))
216	215	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑎 = ℎ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ℎ)))
217	216	mpteq2dv 4745	. . . . . . . . . 10 ⊢ (𝑎 = ℎ → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))
218	217	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))))
219	214, 218	anbi12d 747	. . . . . . . 8 ⊢ (𝑎 = ℎ → ((𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
220	213, 219	rexeqbidv 3153	. . . . . . 7 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
221		fveq1 6190	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑖 → (𝑏‘(𝑑 ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ)))
222	221	mpteq2dv 4745	. . . . . . . . . 10 ⊢ (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
223	222	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
224	223	anbi2d 740	. . . . . . . 8 ⊢ (𝑏 = 𝑖 → ((ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
225	224	cbvrexv 3172	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
226	220, 225	syl6bb 276	. . . . . 6 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
227	226	cbvrexv 3172	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
228	212, 227	syl6bb 276	. . . 4 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
229		eqeq1 2626	. . . . . . 7 ⊢ (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
230	229	anbi2d 740	. . . . . 6 ⊢ (𝑒 = 𝑔 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
231	230	2rexbidv 3057	. . . . 5 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
232		fveq2 6191	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233		sseq1 3626	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑎 ⊆ 𝐵 ↔ 𝑗 ⊆ 𝐵))
234		reseq2 5391	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑗 → (𝑑 ↾ 𝑎) = (𝑑 ↾ 𝑗))
235	234	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑗 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ 𝑗)))
236	235	mpteq2dv 4745	. . . . . . . . . 10 ⊢ (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))
237	236	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))))
238	233, 237	anbi12d 747	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → ((𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
239	232, 238	rexeqbidv 3153	. . . . . . 7 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
240		fveq1 6190	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑘 → (𝑏‘(𝑑 ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗)))
241	240	mpteq2dv 4745	. . . . . . . . . 10 ⊢ (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
242	241	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
243	242	anbi2d 740	. . . . . . . 8 ⊢ (𝑏 = 𝑘 → ((𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
244	243	cbvrexv 3172	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
245	239, 244	syl6bb 276	. . . . . 6 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
246	245	cbvrexv 3172	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
247	231, 246	syl6bb 276	. . . 4 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
248		eqeq1 2626	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_𝑓 + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
249	248	anbi2d 740	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_𝑓 + 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
250	249	2rexbidv 3057	. . . 4 ⊢ (𝑒 = (𝑓 ∘_𝑓 + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
251		eqeq1 2626	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_𝑓 · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
252	251	anbi2d 740	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_𝑓 · 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
253	252	2rexbidv 3057	. . . 4 ⊢ (𝑒 = (𝑓 ∘_𝑓 · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
254		eqeq1 2626	. . . . . 6 ⊢ (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
255	254	anbi2d 740	. . . . 5 ⊢ (𝑒 = 𝐴 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
256	255	2rexbidv 3057	. . . 4 ⊢ (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
257	33, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256	mzpindd 37309	. . 3 ⊢ ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
258	1, 257	mpan 706	. 2 ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
259		reseq1 5390	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑑 ↾ 𝑎) = (𝑐 ↾ 𝑎))
260	259	fveq2d 6195	. . . . . 6 ⊢ (𝑑 = 𝑐 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑐 ↾ 𝑎)))
261	260	cbvmptv 4750	. . . . 5 ⊢ (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))
262	261	eqeq2i 2634	. . . 4 ⊢ (𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎))))
263	262	anbi2i 730	. . 3 ⊢ ((𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
264	263	2rexbii 3042	. 2 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
265	258, 264	sylib 208	1 ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ⊤wtru 1484 ∈ wcel 1990 ∃wrex 2913 Vcvv 3200 ∪ cun 3572 ⊆ wss 3574 ∅c0 3915 {csn 4177 ↦ cmpt 4729 × cxp 5112 ↾ cres 5116 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ∘_𝑓 cof 6895 ↑_𝑚 cmap 7857 Fincfn 7955 + caddc 9939 · cmul 9941 ℤcz 11377 mzPolycmzp 37285

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-mzpcl 37286 df-mzp 37287

This theorem is referenced by: mzpcompact2 37315

W3C validator