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 41978

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

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

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

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 1537	. . 3 ⊢ ⊤
2		0fin 9167	. . . . . 6 ⊢ ∅ ∈ Fin
3		0ex 5297	. . . . . . . 8 ⊢ ∅ ∈ V
4		mzpconst 41962	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑_m ∅) × {𝑓}) ∈ (mzPoly‘∅))
5	3, 4	mpan 687	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_m ∅) × {𝑓}) ∈ (mzPoly‘∅))
6		0ss 4388	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
7	6	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8		fconstmpt 5728	. . . . . . . 8 ⊢ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ 𝑓)
9		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → 𝑑 ∈ (ℤ ↑_m 𝐵))
10		elmapssres 8857	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑_m ∅))
11	9, 6, 10	sylancl 585	. . . . . . . . . 10 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑_m ∅))
12		vex 3470	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
13	12	fvconst2 7197	. . . . . . . . . 10 ⊢ ((𝑑 ↾ ∅) ∈ (ℤ ↑_m ∅) → (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
14	11, 13	syl 17	. . . . . . . . 9 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
15	14	mpteq2dva 5238	. . . . . . . 8 ⊢ (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ 𝑓))
16	8, 15	eqtr4id 2783	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)))
18	17	mpteq2dv 5240	. . . . . . . . . 10 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
19	18	eqeq2d 2735	. . . . . . . . 9 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → (((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
20	19	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
21	20	rspcev 3604	. . . . . . 7 ⊢ ((((ℤ ↑_m ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
22	5, 7, 16, 21	syl12anc 834	. . . . . 6 ⊢ (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23		fveq2 6881	. . . . . . . 8 ⊢ (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24		sseq1 3999	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵))
25		reseq2 5966	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ∅))
26	25	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
27	26	mpteq2dv 5240	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
28	27	eqeq2d 2735	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
29	24, 28	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
30	23, 29	rexeqbidv 3335	. . . . . . 7 ⊢ (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
31	30	rspcev 3604	. . . . . 6 ⊢ ((∅ ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
32	2, 22, 31	sylancr 586	. . . . 5 ⊢ (𝑓 ∈ ℤ → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
33	32	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑓 ∈ ℤ) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
34		snfi 9040	. . . . . 6 ⊢ {𝑓} ∈ Fin
35		vsnex 5419	. . . . . . . . 9 ⊢ {𝑓} ∈ V
36		vsnid 4657	. . . . . . . . 9 ⊢ 𝑓 ∈ {𝑓}
37		mzpproj 41964	. . . . . . . . 9 ⊢ (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
38	35, 36, 37	mp2an 689	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓})
39	38	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
40		snssi 4803	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → {𝑓} ⊆ 𝐵)
41		fveq1 6880	. . . . . . . . 9 ⊢ (𝑔 = 𝑑 → (𝑔‘𝑓) = (𝑑‘𝑓))
42	41	cbvmptv 5251	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑑‘𝑓))
43		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → 𝑑 ∈ (ℤ ↑_m 𝐵))
44		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → 𝑓 ∈ 𝐵)
45	44	snssd 4804	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → {𝑓} ⊆ 𝐵)
46		elmapssres 8857	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_m {𝑓}))
47	43, 45, 46	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_m {𝑓}))
48		fveq1 6880	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔‘𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49		eqid 2724	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))
50		fvex 6894	. . . . . . . . . . . 12 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
51	48, 49, 50	fvmpt 6988	. . . . . . . . . . 11 ⊢ ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑_m {𝑓}) → ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
52	47, 51	syl 17	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53		fvres 6900	. . . . . . . . . . 11 ⊢ (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓))
54	36, 53	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓)
55	52, 54	eqtr2di 2781	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑‘𝑓) = ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
56	55	mpteq2dva 5238	. . . . . . . 8 ⊢ (𝑓 ∈ 𝐵 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑑‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
57	42, 56	eqtrid 2776	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
58		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
59	58	mpteq2dv 5240	. . . . . . . . . 10 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
60	59	eqeq2d 2735	. . . . . . . . 9 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → ((𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))))
61	60	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))))
62	61	rspcev 3604	. . . . . . 7 ⊢ (((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
63	39, 40, 57, 62	syl12anc 834	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64		fveq2 6881	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65		sseq1 3999	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → (𝑎 ⊆ 𝐵 ↔ {𝑓} ⊆ 𝐵))
66		reseq2 5966	. . . . . . . . . . . 12 ⊢ (𝑎 = {𝑓} → (𝑑 ↾ 𝑎) = (𝑑 ↾ {𝑓}))
67	66	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑎 = {𝑓} → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
68	67	mpteq2dv 5240	. . . . . . . . . 10 ⊢ (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
69	68	eqeq2d 2735	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
70	65, 69	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → ((𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
71	64, 70	rexeqbidv 3335	. . . . . . 7 ⊢ (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
72	71	rspcev 3604	. . . . . 6 ⊢ (({𝑓} ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
73	34, 63, 72	sylancr 586	. . . . 5 ⊢ (𝑓 ∈ 𝐵 → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
74	73	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑓 ∈ 𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
75		simplll 772	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ∈ Fin)
76		simprll 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ∈ Fin)
77		unfi 9168	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ ∈ Fin ∧ 𝑗 ∈ Fin) → (ℎ ∪ 𝑗) ∈ Fin)
78	75, 76, 77	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ Fin)
79		vex 3470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℎ ∈ V
80		vex 3470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑗 ∈ V
81	79, 80	unex 7726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ∪ 𝑗) ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ V)
83		ssun1 4164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℎ ⊆ (ℎ ∪ 𝑗)
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ (ℎ ∪ 𝑗))
85		simpllr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑖 ∈ (mzPoly‘ℎ))
86		mzpresrename 41977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ ℎ ⊆ (ℎ ∪ 𝑗) ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
87	82, 84, 85, 86	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
88		ssun2 4165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑗 ⊆ (ℎ ∪ 𝑗)
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ (ℎ ∪ 𝑗))
90		simprlr 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91		mzpresrename 41977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ 𝑗 ⊆ (ℎ ∪ 𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
92	82, 89, 90, 91	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
93		mzpaddmpt 41968	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
94	87, 92, 93	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
95		simplr 766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ 𝐵)
96		simprr 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ 𝐵)
97	95, 96	unssd 4178	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ⊆ 𝐵)
98		ovex 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℤ ↑_m 𝐵) ∈ V
99	98	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℤ ↑_m 𝐵) ∈ V)
100		mzpcompact2lem.i	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐵 ∈ V
101	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝐵 ∈ V)
102		mzpresrename 41977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ ℎ ⊆ 𝐵 ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
103	101, 95, 85, 102	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
104		mzpf 41963	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_m 𝐵)⟶ℤ)
105		ffn 6707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵))
106	103, 104, 105	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵))
107		mzpresrename 41977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ 𝑗 ⊆ 𝐵 ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
108	101, 96, 90, 107	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
109		mzpf 41963	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_m 𝐵)⟶ℤ)
110		ffn 6707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵))
111	108, 109, 110	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵))
112		ofmpteq 7685	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵) ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
113	99, 106, 111, 112	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
114		elmapi 8839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℤ ↑_m 𝐵) → 𝑑:𝐵⟶ℤ)
115		fssres 6747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑑:𝐵⟶ℤ ∧ (ℎ ∪ 𝑗) ⊆ 𝐵) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
116	114, 97, 115	syl2anr 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
117		zex 12564	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℤ ∈ V
118	117, 81	elmap 8861	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↔ (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
119	116, 118	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)))
120		reseq1 5965	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ ℎ) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ))
121	120	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑖‘(𝑙 ↾ ℎ)) = (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)))
122		reseq1 5965	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ 𝑗) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))
123	122	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑘‘(𝑙 ↾ 𝑗)) = (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)))
124	121, 123	oveq12d 7419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
125		eqid 2724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))
126		ovex 7434	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
127	124, 125, 126	fvmpt 6988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
128	119, 127	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
129		resabs1 6001	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ))
130	83, 129	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ)
131	130	fveq2i 6884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ))
132		resabs1 6001	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗))
133	88, 132	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗)
134	133	fveq2i 6884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗))
135	131, 134	oveq12i 7413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))
136	128, 135	eqtr2di 2781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
137	136	mpteq2dva 5238	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
138	113, 137	eqtrd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
139		fveq1 6880	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
140	139	mpteq2dv 5240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
141	140	eqeq2d 2735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
142	141	anbi2d 628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
143	142	rspcev 3604	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
144	94, 97, 138, 143	syl12anc 834	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
145		mzpmulmpt 41969	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
146	87, 92, 145	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
147		ofmpteq 7685	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵) ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
148	99, 106, 111, 147	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
149	121, 123	oveq12d 7419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
150		eqid 2724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))
151		ovex 7434	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
152	149, 150, 151	fvmpt 6988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
153	119, 152	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
154	131, 134	oveq12i 7413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))
155	153, 154	eqtr2di 2781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
156	155	mpteq2dva 5238	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
157	148, 156	eqtrd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
158		fveq1 6880	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
159	158	mpteq2dv 5240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
160	159	eqeq2d 2735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
161	160	anbi2d 628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
162	161	rspcev 3604	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
163	146, 97, 157, 162	syl12anc 834	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
164		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (mzPoly‘𝑎) = (mzPoly‘(ℎ ∪ 𝑗)))
165		sseq1 3999	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑎 ⊆ 𝐵 ↔ (ℎ ∪ 𝑗) ⊆ 𝐵))
166		reseq2 5966	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ↾ 𝑎) = (𝑑 ↾ (ℎ ∪ 𝑗)))
167	166	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))
168	167	mpteq2dv 5240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
169	168	eqeq2d 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
170	165, 169	anbi12d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
171	164, 170	rexeqbidv 3335	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
172	168	eqeq2d 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
173	165, 172	anbi12d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
174	164, 173	rexeqbidv 3335	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
175	171, 174	anbi12d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))))
176	175	rspcev 3604	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ ∪ 𝑗) ∈ Fin ∧ (∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
177	78, 144, 163, 176	syl12anc 834	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
178	177	adantlrr 718	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
179	178	adantrrr 722	. . . . . . . . . . . . . 14 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
180		simplrr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
181		simprrr 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
182	180, 181	oveq12d 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_f + 𝑔) = ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
183	182	eqeq1d 2726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
184	183	anbi2d 628	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
185	184	rexbidv 3170	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
186	180, 181	oveq12d 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_f · 𝑔) = ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
187	186	eqeq1d 2726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
188	187	anbi2d 628	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
189	188	rexbidv 3170	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
190	185, 189	anbi12d 630	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
191	190	rexbidv 3170	. . . . . . . . . . . . . 14 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
192	179, 191	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
193		r19.40 3111	. . . . . . . . . . . . 13 ⊢ (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
194	192, 193	syl 17	. . . . . . . . . . . 12 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
195	194	exp32 420	. . . . . . . . . . 11 ⊢ (((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) → ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) → ((𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))))
196	195	rexlimdvv 3202	. . . . . . . . . 10 ⊢ (((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
197	196	ex 412	. . . . . . . . 9 ⊢ ((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) → ((ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))))
198	197	rexlimivv 3191	. . . . . . . 8 ⊢ (∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
199	198	imp 406	. . . . . . 7 ⊢ ((∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
200	199	ad2ant2l 743	. . . . . 6 ⊢ (((𝑓:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
201	200	3adant1 1127	. . . . 5 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
202	201	simpld 494	. . . 4 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
203	201	simprd 495	. . . 4 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
204		eqeq1 2728	. . . . . 6 ⊢ (𝑒 = ((ℤ ↑_m 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
205	204	anbi2d 628	. . . . 5 ⊢ (𝑒 = ((ℤ ↑_m 𝐵) × {𝑓}) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
206	205	2rexbidv 3211	. . . 4 ⊢ (𝑒 = ((ℤ ↑_m 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
207		eqeq1 2728	. . . . . 6 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
208	207	anbi2d 628	. . . . 5 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
209	208	2rexbidv 3211	. . . 4 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
210		eqeq1 2728	. . . . . . 7 ⊢ (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
211	210	anbi2d 628	. . . . . 6 ⊢ (𝑒 = 𝑓 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
212	211	2rexbidv 3211	. . . . 5 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
213		fveq2 6881	. . . . . . . 8 ⊢ (𝑎 = ℎ → (mzPoly‘𝑎) = (mzPoly‘ℎ))
214		sseq1 3999	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑎 ⊆ 𝐵 ↔ ℎ ⊆ 𝐵))
215		reseq2 5966	. . . . . . . . . . . 12 ⊢ (𝑎 = ℎ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ℎ))
216	215	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑎 = ℎ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ℎ)))
217	216	mpteq2dv 5240	. . . . . . . . . 10 ⊢ (𝑎 = ℎ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))
218	217	eqeq2d 2735	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))))
219	214, 218	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = ℎ → ((𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
220	213, 219	rexeqbidv 3335	. . . . . . 7 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
221		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑖 → (𝑏‘(𝑑 ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ)))
222	221	mpteq2dv 5240	. . . . . . . . . 10 ⊢ (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
223	222	eqeq2d 2735	. . . . . . . . 9 ⊢ (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
224	223	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = 𝑖 → ((ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
225	224	cbvrexvw 3227	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
226	220, 225	bitrdi 287	. . . . . 6 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
227	226	cbvrexvw 3227	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
228	212, 227	bitrdi 287	. . . 4 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
229		eqeq1 2728	. . . . . . 7 ⊢ (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
230	229	anbi2d 628	. . . . . 6 ⊢ (𝑒 = 𝑔 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
231	230	2rexbidv 3211	. . . . 5 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
232		fveq2 6881	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233		sseq1 3999	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑎 ⊆ 𝐵 ↔ 𝑗 ⊆ 𝐵))
234		reseq2 5966	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑗 → (𝑑 ↾ 𝑎) = (𝑑 ↾ 𝑗))
235	234	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑗 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ 𝑗)))
236	235	mpteq2dv 5240	. . . . . . . . . 10 ⊢ (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))
237	236	eqeq2d 2735	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))))
238	233, 237	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → ((𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
239	232, 238	rexeqbidv 3335	. . . . . . 7 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
240		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑘 → (𝑏‘(𝑑 ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗)))
241	240	mpteq2dv 5240	. . . . . . . . . 10 ⊢ (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
242	241	eqeq2d 2735	. . . . . . . . 9 ⊢ (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
243	242	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = 𝑘 → ((𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
244	243	cbvrexvw 3227	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
245	239, 244	bitrdi 287	. . . . . 6 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
246	245	cbvrexvw 3227	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
247	231, 246	bitrdi 287	. . . 4 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
248		eqeq1 2728	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_f + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
249	248	anbi2d 628	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_f + 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
250	249	2rexbidv 3211	. . . 4 ⊢ (𝑒 = (𝑓 ∘_f + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
251		eqeq1 2728	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_f · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
252	251	anbi2d 628	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_f · 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
253	252	2rexbidv 3211	. . . 4 ⊢ (𝑒 = (𝑓 ∘_f · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
254		eqeq1 2728	. . . . . 6 ⊢ (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
255	254	anbi2d 628	. . . . 5 ⊢ (𝑒 = 𝐴 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
256	255	2rexbidv 3211	. . . 4 ⊢ (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
257	33, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256	mzpindd 41973	. . 3 ⊢ ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
258	1, 257	mpan 687	. 2 ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
259		reseq1 5965	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑑 ↾ 𝑎) = (𝑐 ↾ 𝑎))
260	259	fveq2d 6885	. . . . . 6 ⊢ (𝑑 = 𝑐 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑐 ↾ 𝑎)))
261	260	cbvmptv 5251	. . . . 5 ⊢ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))
262	261	eqeq2i 2737	. . . 4 ⊢ (𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎))))
263	262	anbi2i 622	. . 3 ⊢ ((𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
264	263	2rexbii 3121	. 2 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
265	258, 264	sylib 217	1 ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ⊤wtru 1534 ∈ wcel 2098 ∃wrex 3062 Vcvv 3466 ∪ cun 3938 ⊆ wss 3940 ∅c0 4314 {csn 4620 ↦ cmpt 5221 × cxp 5664 ↾ cres 5668 Fn wfn 6528 ⟶wf 6529 ‘cfv 6533 (class class class)co 7401 ∘_f cof 7661 ↑_m cmap 8816 Fincfn 8935 + caddc 11109 · cmul 11111 ℤcz 12555 mzPolycmzp 41949

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-int 4941 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-of 7663 df-om 7849 df-1st 7968 df-2nd 7969 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-er 8699 df-map 8818 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-nn 12210 df-n0 12470 df-z 12556 df-mzpcl 41950 df-mzp 41951

This theorem is referenced by: mzpcompact2 41979

W3C validator