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 40489

Description: Lemma for mzpcompact2 40490. (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 1543	. . 3 ⊢ ⊤
2		0fin 8916	. . . . . 6 ⊢ ∅ ∈ Fin
3		0ex 5226	. . . . . . . 8 ⊢ ∅ ∈ V
4		mzpconst 40473	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑_m ∅) × {𝑓}) ∈ (mzPoly‘∅))
5	3, 4	mpan 686	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_m ∅) × {𝑓}) ∈ (mzPoly‘∅))
6		0ss 4327	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
7	6	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8		fconstmpt 5640	. . . . . . . 8 ⊢ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ 𝑓)
9		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → 𝑑 ∈ (ℤ ↑_m 𝐵))
10		elmapssres 8613	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑_m ∅))
11	9, 6, 10	sylancl 585	. . . . . . . . . 10 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑_m ∅))
12		vex 3426	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
13	12	fvconst2 7061	. . . . . . . . . 10 ⊢ ((𝑑 ↾ ∅) ∈ (ℤ ↑_m ∅) → (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
14	11, 13	syl 17	. . . . . . . . 9 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
15	14	mpteq2dva 5170	. . . . . . . 8 ⊢ (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ 𝑓))
16	8, 15	eqtr4id 2798	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17		fveq1 6755	. . . . . . . . . . 11 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)))
18	17	mpteq2dv 5172	. . . . . . . . . 10 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
19	18	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → (((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
20	19	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
21	20	rspcev 3552	. . . . . . 7 ⊢ ((((ℤ ↑_m ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
22	5, 7, 16, 21	syl12anc 833	. . . . . 6 ⊢ (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23		fveq2 6756	. . . . . . . 8 ⊢ (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24		sseq1 3942	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵))
25		reseq2 5875	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ∅))
26	25	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
27	26	mpteq2dv 5172	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
28	27	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
29	24, 28	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
30	23, 29	rexeqbidv 3328	. . . . . . 7 ⊢ (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
31	30	rspcev 3552	. . . . . 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 8788	. . . . . 6 ⊢ {𝑓} ∈ Fin
35		snex 5349	. . . . . . . . 9 ⊢ {𝑓} ∈ V
36		vsnid 4595	. . . . . . . . 9 ⊢ 𝑓 ∈ {𝑓}
37		mzpproj 40475	. . . . . . . . 9 ⊢ (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
38	35, 36, 37	mp2an 688	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓})
39	38	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
40		snssi 4738	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → {𝑓} ⊆ 𝐵)
41		fveq1 6755	. . . . . . . . 9 ⊢ (𝑔 = 𝑑 → (𝑔‘𝑓) = (𝑑‘𝑓))
42	41	cbvmptv 5183	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑑‘𝑓))
43		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → 𝑑 ∈ (ℤ ↑_m 𝐵))
44		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → 𝑓 ∈ 𝐵)
45	44	snssd 4739	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → {𝑓} ⊆ 𝐵)
46		elmapssres 8613	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_m {𝑓}))
47	43, 45, 46	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_m {𝑓}))
48		fveq1 6755	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔‘𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49		eqid 2738	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))
50		fvex 6769	. . . . . . . . . . . 12 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
51	48, 49, 50	fvmpt 6857	. . . . . . . . . . 11 ⊢ ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑_m {𝑓}) → ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
52	47, 51	syl 17	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53		fvres 6775	. . . . . . . . . . 11 ⊢ (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓))
54	36, 53	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓)
55	52, 54	eqtr2di 2796	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑‘𝑓) = ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
56	55	mpteq2dva 5170	. . . . . . . 8 ⊢ (𝑓 ∈ 𝐵 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑑‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
57	42, 56	syl5eq 2791	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
58		fveq1 6755	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
59	58	mpteq2dv 5172	. . . . . . . . . 10 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
60	59	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → ((𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))))
61	60	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))))
62	61	rspcev 3552	. . . . . . 7 ⊢ (((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
63	39, 40, 57, 62	syl12anc 833	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64		fveq2 6756	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65		sseq1 3942	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → (𝑎 ⊆ 𝐵 ↔ {𝑓} ⊆ 𝐵))
66		reseq2 5875	. . . . . . . . . . . 12 ⊢ (𝑎 = {𝑓} → (𝑑 ↾ 𝑎) = (𝑑 ↾ {𝑓}))
67	66	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑎 = {𝑓} → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
68	67	mpteq2dv 5172	. . . . . . . . . 10 ⊢ (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
69	68	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
70	65, 69	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → ((𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
71	64, 70	rexeqbidv 3328	. . . . . . 7 ⊢ (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
72	71	rspcev 3552	. . . . . 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 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ∈ Fin)
76		simprll 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ∈ Fin)
77		unfi 8917	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ ∈ Fin ∧ 𝑗 ∈ Fin) → (ℎ ∪ 𝑗) ∈ Fin)
78	75, 76, 77	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ Fin)
79		vex 3426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℎ ∈ V
80		vex 3426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑗 ∈ V
81	79, 80	unex 7574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ∪ 𝑗) ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ V)
83		ssun1 4102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℎ ⊆ (ℎ ∪ 𝑗)
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ (ℎ ∪ 𝑗))
85		simpllr 772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑖 ∈ (mzPoly‘ℎ))
86		mzpresrename 40488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ ℎ ⊆ (ℎ ∪ 𝑗) ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
87	82, 84, 85, 86	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
88		ssun2 4103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑗 ⊆ (ℎ ∪ 𝑗)
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ (ℎ ∪ 𝑗))
90		simprlr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91		mzpresrename 40488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ 𝑗 ⊆ (ℎ ∪ 𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
92	82, 89, 90, 91	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
93		mzpaddmpt 40479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
94	87, 92, 93	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
95		simplr 765	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ 𝐵)
96		simprr 769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ 𝐵)
97	95, 96	unssd 4116	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ⊆ 𝐵)
98		ovex 7288	. . . . . . . . . . . . . . . . . . . . 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 40488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ ℎ ⊆ 𝐵 ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
103	101, 95, 85, 102	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
104		mzpf 40474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_m 𝐵)⟶ℤ)
105		ffn 6584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵))
106	103, 104, 105	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵))
107		mzpresrename 40488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ 𝑗 ⊆ 𝐵 ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
108	101, 96, 90, 107	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
109		mzpf 40474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_m 𝐵)⟶ℤ)
110		ffn 6584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵))
111	108, 109, 110	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵))
112		ofmpteq 7533	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵) ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
113	99, 106, 111, 112	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
114		elmapi 8595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℤ ↑_m 𝐵) → 𝑑:𝐵⟶ℤ)
115		fssres 6624	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑑:𝐵⟶ℤ ∧ (ℎ ∪ 𝑗) ⊆ 𝐵) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
116	114, 97, 115	syl2anr 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
117		zex 12258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℤ ∈ V
118	117, 81	elmap 8617	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↔ (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
119	116, 118	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)))
120		reseq1 5874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ ℎ) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ))
121	120	fveq2d 6760	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑖‘(𝑙 ↾ ℎ)) = (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)))
122		reseq1 5874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ 𝑗) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))
123	122	fveq2d 6760	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑘‘(𝑙 ↾ 𝑗)) = (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)))
124	121, 123	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
125		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))
126		ovex 7288	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
127	124, 125, 126	fvmpt 6857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
128	119, 127	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
129		resabs1 5910	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ))
130	83, 129	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ)
131	130	fveq2i 6759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ))
132		resabs1 5910	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗))
133	88, 132	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗)
134	133	fveq2i 6759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗))
135	131, 134	oveq12i 7267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))
136	128, 135	eqtr2di 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
137	136	mpteq2dva 5170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
138	113, 137	eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
139		fveq1 6755	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
140	139	mpteq2dv 5172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
141	140	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . 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 3552	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
144	94, 97, 138, 143	syl12anc 833	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
145		mzpmulmpt 40480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
146	87, 92, 145	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
147		ofmpteq 7533	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵) ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
148	99, 106, 111, 147	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
149	121, 123	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
150		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))
151		ovex 7288	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
152	149, 150, 151	fvmpt 6857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
153	119, 152	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
154	131, 134	oveq12i 7267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))
155	153, 154	eqtr2di 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
156	155	mpteq2dva 5170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
157	148, 156	eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
158		fveq1 6755	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
159	158	mpteq2dv 5172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
160	159	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . 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 3552	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
163	146, 97, 157, 162	syl12anc 833	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
164		fveq2 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (mzPoly‘𝑎) = (mzPoly‘(ℎ ∪ 𝑗)))
165		sseq1 3942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑎 ⊆ 𝐵 ↔ (ℎ ∪ 𝑗) ⊆ 𝐵))
166		reseq2 5875	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ↾ 𝑎) = (𝑑 ↾ (ℎ ∪ 𝑗)))
167	166	fveq2d 6760	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))
168	167	mpteq2dv 5172	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
169	168	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . 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 3328	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
172	168	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . 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 3328	. . . . . . . . . . . . . . . . . . 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 3552	. . . . . . . . . . . . . . . . 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 833	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
178	177	adantlrr 717	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
179	178	adantrrr 721	. . . . . . . . . . . . . 14 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
180		simplrr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
181		simprrr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
182	180, 181	oveq12d 7273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_f + 𝑔) = ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
183	182	eqeq1d 2740	. . . . . . . . . . . . . . . . . 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 3225	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
186	180, 181	oveq12d 7273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_f · 𝑔) = ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
187	186	eqeq1d 2740	. . . . . . . . . . . . . . . . . 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 3225	. . . . . . . . . . . . . . . 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 3225	. . . . . . . . . . . . . 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 256	. . . . . . . . . . . . 13 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
193		r19.40 3272	. . . . . . . . . . . . 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 3221	. . . . . . . . . 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 3220	. . . . . . . 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 742	. . . . . 6 ⊢ (((𝑓:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
201	200	3adant1 1128	. . . . 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 2742	. . . . . 6 ⊢ (𝑒 = ((ℤ ↑_m 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
205	204	anbi2d 628	. . . . 5 ⊢ (𝑒 = ((ℤ ↑_m 𝐵) × {𝑓}) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
206	205	2rexbidv 3228	. . . 4 ⊢ (𝑒 = ((ℤ ↑_m 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
207		eqeq1 2742	. . . . . 6 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
208	207	anbi2d 628	. . . . 5 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
209	208	2rexbidv 3228	. . . 4 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
210		eqeq1 2742	. . . . . . 7 ⊢ (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
211	210	anbi2d 628	. . . . . 6 ⊢ (𝑒 = 𝑓 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
212	211	2rexbidv 3228	. . . . 5 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
213		fveq2 6756	. . . . . . . 8 ⊢ (𝑎 = ℎ → (mzPoly‘𝑎) = (mzPoly‘ℎ))
214		sseq1 3942	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑎 ⊆ 𝐵 ↔ ℎ ⊆ 𝐵))
215		reseq2 5875	. . . . . . . . . . . 12 ⊢ (𝑎 = ℎ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ℎ))
216	215	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑎 = ℎ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ℎ)))
217	216	mpteq2dv 5172	. . . . . . . . . 10 ⊢ (𝑎 = ℎ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))
218	217	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))))
219	214, 218	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = ℎ → ((𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
220	213, 219	rexeqbidv 3328	. . . . . . 7 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
221		fveq1 6755	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑖 → (𝑏‘(𝑑 ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ)))
222	221	mpteq2dv 5172	. . . . . . . . . 10 ⊢ (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
223	222	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
224	223	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = 𝑖 → ((ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
225	224	cbvrexvw 3373	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
226	220, 225	bitrdi 286	. . . . . 6 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
227	226	cbvrexvw 3373	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
228	212, 227	bitrdi 286	. . . 4 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
229		eqeq1 2742	. . . . . . 7 ⊢ (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
230	229	anbi2d 628	. . . . . 6 ⊢ (𝑒 = 𝑔 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
231	230	2rexbidv 3228	. . . . 5 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
232		fveq2 6756	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233		sseq1 3942	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑎 ⊆ 𝐵 ↔ 𝑗 ⊆ 𝐵))
234		reseq2 5875	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑗 → (𝑑 ↾ 𝑎) = (𝑑 ↾ 𝑗))
235	234	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑗 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ 𝑗)))
236	235	mpteq2dv 5172	. . . . . . . . . 10 ⊢ (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))
237	236	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))))
238	233, 237	anbi12d 630	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → ((𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
239	232, 238	rexeqbidv 3328	. . . . . . 7 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
240		fveq1 6755	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑘 → (𝑏‘(𝑑 ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗)))
241	240	mpteq2dv 5172	. . . . . . . . . 10 ⊢ (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
242	241	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
243	242	anbi2d 628	. . . . . . . 8 ⊢ (𝑏 = 𝑘 → ((𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
244	243	cbvrexvw 3373	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
245	239, 244	bitrdi 286	. . . . . 6 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
246	245	cbvrexvw 3373	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
247	231, 246	bitrdi 286	. . . 4 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
248		eqeq1 2742	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_f + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
249	248	anbi2d 628	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_f + 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
250	249	2rexbidv 3228	. . . 4 ⊢ (𝑒 = (𝑓 ∘_f + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
251		eqeq1 2742	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_f · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
252	251	anbi2d 628	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_f · 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
253	252	2rexbidv 3228	. . . 4 ⊢ (𝑒 = (𝑓 ∘_f · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
254		eqeq1 2742	. . . . . 6 ⊢ (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
255	254	anbi2d 628	. . . . 5 ⊢ (𝑒 = 𝐴 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
256	255	2rexbidv 3228	. . . 4 ⊢ (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
257	33, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256	mzpindd 40484	. . 3 ⊢ ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
258	1, 257	mpan 686	. 2 ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
259		reseq1 5874	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑑 ↾ 𝑎) = (𝑐 ↾ 𝑎))
260	259	fveq2d 6760	. . . . . 6 ⊢ (𝑑 = 𝑐 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑐 ↾ 𝑎)))
261	260	cbvmptv 5183	. . . . 5 ⊢ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))
262	261	eqeq2i 2751	. . . 4 ⊢ (𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎))))
263	262	anbi2i 622	. . 3 ⊢ ((𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
264	263	2rexbii 3178	. 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 1085 = wceq 1539 ⊤wtru 1540 ∈ wcel 2108 ∃wrex 3064 Vcvv 3422 ∪ cun 3881 ⊆ wss 3883 ∅c0 4253 {csn 4558 ↦ cmpt 5153 × cxp 5578 ↾ cres 5582 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ∘_f cof 7509 ↑_m cmap 8573 Fincfn 8691 + caddc 10805 · cmul 10807 ℤcz 12249 mzPolycmzp 40460

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-n0 12164 df-z 12250 df-mzpcl 40461 df-mzp 40462

This theorem is referenced by: mzpcompact2 40490

W3C validator