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 41060

Description: Lemma for mzpcompact2 41061. (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 1545	. . 3 ⊢ ⊤
2		0fin 9115	. . . . . 6 ⊢ ∅ ∈ Fin
3		0ex 5264	. . . . . . . 8 ⊢ ∅ ∈ V
4		mzpconst 41044	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑_m ∅) × {𝑓}) ∈ (mzPoly‘∅))
5	3, 4	mpan 688	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_m ∅) × {𝑓}) ∈ (mzPoly‘∅))
6		0ss 4356	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
7	6	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8		fconstmpt 5694	. . . . . . . 8 ⊢ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ 𝑓)
9		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → 𝑑 ∈ (ℤ ↑_m 𝐵))
10		elmapssres 8805	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑_m ∅))
11	9, 6, 10	sylancl 586	. . . . . . . . . 10 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑_m ∅))
12		vex 3449	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
13	12	fvconst2 7153	. . . . . . . . . 10 ⊢ ((𝑑 ↾ ∅) ∈ (ℤ ↑_m ∅) → (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
14	11, 13	syl 17	. . . . . . . . 9 ⊢ ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
15	14	mpteq2dva 5205	. . . . . . . 8 ⊢ (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ 𝑓))
16	8, 15	eqtr4id 2795	. . . . . . 7 ⊢ (𝑓 ∈ ℤ → ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17		fveq1 6841	. . . . . . . . . . 11 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)))
18	17	mpteq2dv 5207	. . . . . . . . . 10 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
19	18	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → (((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
20	19	anbi2d 629	. . . . . . . 8 ⊢ (𝑏 = ((ℤ ↑_m ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
21	20	rspcev 3581	. . . . . . 7 ⊢ ((((ℤ ↑_m ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (((ℤ ↑_m ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
22	5, 7, 16, 21	syl12anc 835	. . . . . 6 ⊢ (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23		fveq2 6842	. . . . . . . 8 ⊢ (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24		sseq1 3969	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵))
25		reseq2 5932	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ∅))
26	25	fveq2d 6846	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
27	26	mpteq2dv 5207	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
28	27	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
29	24, 28	anbi12d 631	. . . . . . . 8 ⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
30	23, 29	rexeqbidv 3320	. . . . . . 7 ⊢ (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
31	30	rspcev 3581	. . . . . 6 ⊢ ((∅ ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
32	2, 22, 31	sylancr 587	. . . . 5 ⊢ (𝑓 ∈ ℤ → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
33	32	adantl 482	. . . 4 ⊢ ((⊤ ∧ 𝑓 ∈ ℤ) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
34		snfi 8988	. . . . . 6 ⊢ {𝑓} ∈ Fin
35		vsnex 5386	. . . . . . . . 9 ⊢ {𝑓} ∈ V
36		vsnid 4623	. . . . . . . . 9 ⊢ 𝑓 ∈ {𝑓}
37		mzpproj 41046	. . . . . . . . 9 ⊢ (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
38	35, 36, 37	mp2an 690	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓})
39	38	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}))
40		snssi 4768	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → {𝑓} ⊆ 𝐵)
41		fveq1 6841	. . . . . . . . 9 ⊢ (𝑔 = 𝑑 → (𝑔‘𝑓) = (𝑑‘𝑓))
42	41	cbvmptv 5218	. . . . . . . 8 ⊢ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑑‘𝑓))
43		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → 𝑑 ∈ (ℤ ↑_m 𝐵))
44		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → 𝑓 ∈ 𝐵)
45	44	snssd 4769	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → {𝑓} ⊆ 𝐵)
46		elmapssres 8805	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_m {𝑓}))
47	43, 45, 46	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑_m {𝑓}))
48		fveq1 6841	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔‘𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))
50		fvex 6855	. . . . . . . . . . . 12 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
51	48, 49, 50	fvmpt 6948	. . . . . . . . . . 11 ⊢ ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑_m {𝑓}) → ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
52	47, 51	syl 17	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53		fvres 6861	. . . . . . . . . . 11 ⊢ (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓))
54	36, 53	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑‘𝑓)
55	52, 54	eqtr2di 2793	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑‘𝑓) = ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
56	55	mpteq2dva 5205	. . . . . . . 8 ⊢ (𝑓 ∈ 𝐵 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑑‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
57	42, 56	eqtrid 2788	. . . . . . 7 ⊢ (𝑓 ∈ 𝐵 → (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
58		fveq1 6841	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))
59	58	mpteq2dv 5207	. . . . . . . . . 10 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))
60	59	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → ((𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓})))))
61	60	anbi2d 629	. . . . . . . 8 ⊢ (𝑏 = (𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))))
62	61	rspcev 3581	. . . . . . 7 ⊢ (((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑_m {𝑓}) ↦ (𝑔‘𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
63	39, 40, 57, 62	syl12anc 835	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64		fveq2 6842	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65		sseq1 3969	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → (𝑎 ⊆ 𝐵 ↔ {𝑓} ⊆ 𝐵))
66		reseq2 5932	. . . . . . . . . . . 12 ⊢ (𝑎 = {𝑓} → (𝑑 ↾ 𝑎) = (𝑑 ↾ {𝑓}))
67	66	fveq2d 6846	. . . . . . . . . . 11 ⊢ (𝑎 = {𝑓} → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
68	67	mpteq2dv 5207	. . . . . . . . . 10 ⊢ (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
69	68	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
70	65, 69	anbi12d 631	. . . . . . . 8 ⊢ (𝑎 = {𝑓} → ((𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
71	64, 70	rexeqbidv 3320	. . . . . . 7 ⊢ (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
72	71	rspcev 3581	. . . . . 6 ⊢ (({𝑓} ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
73	34, 63, 72	sylancr 587	. . . . 5 ⊢ (𝑓 ∈ 𝐵 → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
74	73	adantl 482	. . . 4 ⊢ ((⊤ ∧ 𝑓 ∈ 𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
75		simplll 773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ∈ Fin)
76		simprll 777	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ∈ Fin)
77		unfi 9116	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ ∈ Fin ∧ 𝑗 ∈ Fin) → (ℎ ∪ 𝑗) ∈ Fin)
78	75, 76, 77	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ Fin)
79		vex 3449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℎ ∈ V
80		vex 3449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑗 ∈ V
81	79, 80	unex 7680	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ∪ 𝑗) ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ∈ V)
83		ssun1 4132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℎ ⊆ (ℎ ∪ 𝑗)
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ (ℎ ∪ 𝑗))
85		simpllr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑖 ∈ (mzPoly‘ℎ))
86		mzpresrename 41059	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ ℎ ⊆ (ℎ ∪ 𝑗) ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
87	82, 84, 85, 86	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
88		ssun2 4133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑗 ⊆ (ℎ ∪ 𝑗)
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ (ℎ ∪ 𝑗))
90		simprlr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91		mzpresrename 41059	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∪ 𝑗) ∈ V ∧ 𝑗 ⊆ (ℎ ∪ 𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
92	82, 89, 90, 91	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
93		mzpaddmpt 41050	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
94	87, 92, 93	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
95		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ℎ ⊆ 𝐵)
96		simprr 771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → 𝑗 ⊆ 𝐵)
97	95, 96	unssd 4146	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (ℎ ∪ 𝑗) ⊆ 𝐵)
98		ovex 7390	. . . . . . . . . . . . . . . . . . . . 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 41059	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ ℎ ⊆ 𝐵 ∧ 𝑖 ∈ (mzPoly‘ℎ)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
103	101, 95, 85, 102	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵))
104		mzpf 41045	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_m 𝐵)⟶ℤ)
105		ffn 6668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))):(ℤ ↑_m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵))
106	103, 104, 105	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵))
107		mzpresrename 41059	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ V ∧ 𝑗 ⊆ 𝐵 ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
108	101, 96, 90, 107	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵))
109		mzpf 41045	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_m 𝐵)⟶ℤ)
110		ffn 6668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))):(ℤ ↑_m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵))
111	108, 109, 110	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵))
112		ofmpteq 7639	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵) ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
113	99, 106, 111, 112	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))))
114		elmapi 8787	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℤ ↑_m 𝐵) → 𝑑:𝐵⟶ℤ)
115		fssres 6708	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑑:𝐵⟶ℤ ∧ (ℎ ∪ 𝑗) ⊆ 𝐵) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
116	114, 97, 115	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
117		zex 12508	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℤ ∈ V
118	117, 81	elmap 8809	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↔ (𝑑 ↾ (ℎ ∪ 𝑗)):(ℎ ∪ 𝑗)⟶ℤ)
119	116, 118	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → (𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)))
120		reseq1 5931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ ℎ) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ))
121	120	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑖‘(𝑙 ↾ ℎ)) = (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)))
122		reseq1 5931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑙 ↾ 𝑗) = ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))
123	122	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → (𝑘‘(𝑙 ↾ 𝑗)) = (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)))
124	121, 123	oveq12d 7375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
125		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))
126		ovex 7390	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
127	124, 125, 126	fvmpt 6948	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
128	119, 127	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
129		resabs1 5967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ))
130	83, 129	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ) = (𝑑 ↾ ℎ)
131	130	fveq2i 6845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ))
132		resabs1 5967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ⊆ (ℎ ∪ 𝑗) → ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗))
133	88, 132	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗) = (𝑑 ↾ 𝑗)
134	133	fveq2i 6845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗))
135	131, 134	oveq12i 7369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) + (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))
136	128, 135	eqtr2di 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
137	136	mpteq2dva 5205	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) + (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
138	113, 137	eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
139		fveq1 6841	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
140	139	mpteq2dv 5207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
141	140	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
142	141	anbi2d 629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) → (((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
143	142	rspcev 3581	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) + (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
144	94, 97, 138, 143	syl12anc 835	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
145		mzpmulmpt 41051	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑖‘(𝑙 ↾ ℎ))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ (𝑘‘(𝑙 ↾ 𝑗))) ∈ (mzPoly‘(ℎ ∪ 𝑗))) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
146	87, 92, 145	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)))
147		ofmpteq 7639	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℤ ↑_m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) Fn (ℤ ↑_m 𝐵) ∧ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))) Fn (ℤ ↑_m 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
148	99, 106, 111, 147	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))))
149	121, 123	oveq12d 7375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 = (𝑑 ↾ (ℎ ∪ 𝑗)) → ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
150		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))
151		ovex 7390	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) ∈ V
152	149, 150, 151	fvmpt 6948	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑑 ↾ (ℎ ∪ 𝑗)) ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
153	119, 152	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))))
154	131, 134	oveq12i 7369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ ℎ)) · (𝑘‘((𝑑 ↾ (ℎ ∪ 𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))
155	153, 154	eqtr2di 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) ∧ 𝑑 ∈ (ℤ ↑_m 𝐵)) → ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
156	155	mpteq2dva 5205	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑖‘(𝑑 ↾ ℎ)) · (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
157	148, 156	eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
158		fveq1 6841	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))) = ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))
159	158	mpteq2dv 5207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
160	159	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
161	160	anbi2d 629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) → (((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
162	161	rspcev 3581	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗)))) ∈ (mzPoly‘(ℎ ∪ 𝑗)) ∧ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑_m (ℎ ∪ 𝑗)) ↦ ((𝑖‘(𝑙 ↾ ℎ)) · (𝑘‘(𝑙 ↾ 𝑗))))‘(𝑑 ↾ (ℎ ∪ 𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
163	146, 97, 157, 162	syl12anc 835	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
164		fveq2 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (mzPoly‘𝑎) = (mzPoly‘(ℎ ∪ 𝑗)))
165		sseq1 3969	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑎 ⊆ 𝐵 ↔ (ℎ ∪ 𝑗) ⊆ 𝐵))
166		reseq2 5932	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ↾ 𝑎) = (𝑑 ↾ (ℎ ∪ 𝑗)))
167	166	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))
168	167	mpteq2dv 5207	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))
169	168	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
170	165, 169	anbi12d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
171	164, 170	rexeqbidv 3320	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
172	168	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))
173	165, 172	anbi12d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
174	164, 173	rexeqbidv 3320	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (ℎ ∪ 𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗)))))))
175	171, 174	anbi12d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (ℎ ∪ 𝑗) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(ℎ ∪ 𝑗))((ℎ ∪ 𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ (ℎ ∪ 𝑗))))))))
176	175	rspcev 3581	. . . . . . . . . . . . . . . . 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 835	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ ℎ ⊆ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
178	177	adantlrr 719	. . . . . . . . . . . . . . 15 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗 ⊆ 𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
179	178	adantrrr 723	. . . . . . . . . . . . . 14 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
180		simplrr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
181		simprrr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
182	180, 181	oveq12d 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_f + 𝑔) = ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
183	182	eqeq1d 2738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
184	183	anbi2d 629	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
185	184	rexbidv 3175	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f + (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
186	180, 181	oveq12d 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (𝑓 ∘_f · 𝑔) = ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
187	186	eqeq1d 2738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
188	187	anbi2d 629	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ((𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
189	188	rexbidv 3175	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))) ∘_f · (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
190	185, 189	anbi12d 631	. . . . . . . . . . . . . . 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 3175	. . . . . . . . . . . . . 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 3122	. . . . . . . . . . . . 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 421	. . . . . . . . . . 11 ⊢ (((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) → ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) → ((𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))))
196	195	rexlimdvv 3204	. . . . . . . . . 10 ⊢ (((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) ∧ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
197	196	ex 413	. . . . . . . . 9 ⊢ ((ℎ ∈ Fin ∧ 𝑖 ∈ (mzPoly‘ℎ)) → ((ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))))
198	197	rexlimivv 3196	. . . . . . . 8 ⊢ (∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))))
199	198	imp 407	. . . . . . 7 ⊢ ((∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))) ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
200	199	ad2ant2l 744	. . . . . 6 ⊢ (((𝑓:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
201	200	3adant1 1130	. . . . 5 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
202	201	simpld 495	. . . 4 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
203	201	simprd 496	. . . 4 ⊢ ((⊤ ∧ (𝑓:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))) ∧ (𝑔:(ℤ ↑_m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
204		eqeq1 2740	. . . . . 6 ⊢ (𝑒 = ((ℤ ↑_m 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
205	204	anbi2d 629	. . . . 5 ⊢ (𝑒 = ((ℤ ↑_m 𝐵) × {𝑓}) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
206	205	2rexbidv 3213	. . . 4 ⊢ (𝑒 = ((ℤ ↑_m 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ ((ℤ ↑_m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
207		eqeq1 2740	. . . . . 6 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
208	207	anbi2d 629	. . . . 5 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
209	208	2rexbidv 3213	. . . 4 ⊢ (𝑒 = (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑_m 𝐵) ↦ (𝑔‘𝑓)) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
210		eqeq1 2740	. . . . . . 7 ⊢ (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
211	210	anbi2d 629	. . . . . 6 ⊢ (𝑒 = 𝑓 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
212	211	2rexbidv 3213	. . . . 5 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
213		fveq2 6842	. . . . . . . 8 ⊢ (𝑎 = ℎ → (mzPoly‘𝑎) = (mzPoly‘ℎ))
214		sseq1 3969	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑎 ⊆ 𝐵 ↔ ℎ ⊆ 𝐵))
215		reseq2 5932	. . . . . . . . . . . 12 ⊢ (𝑎 = ℎ → (𝑑 ↾ 𝑎) = (𝑑 ↾ ℎ))
216	215	fveq2d 6846	. . . . . . . . . . 11 ⊢ (𝑎 = ℎ → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ ℎ)))
217	216	mpteq2dv 5207	. . . . . . . . . 10 ⊢ (𝑎 = ℎ → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))
218	217	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑎 = ℎ → (𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))))
219	214, 218	anbi12d 631	. . . . . . . 8 ⊢ (𝑎 = ℎ → ((𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
220	213, 219	rexeqbidv 3320	. . . . . . 7 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))))))
221		fveq1 6841	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑖 → (𝑏‘(𝑑 ↾ ℎ)) = (𝑖‘(𝑑 ↾ ℎ)))
222	221	mpteq2dv 5207	. . . . . . . . . 10 ⊢ (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))
223	222	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
224	223	anbi2d 629	. . . . . . . 8 ⊢ (𝑏 = 𝑖 → ((ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ (ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
225	224	cbvrexvw 3226	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ ℎ)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
226	220, 225	bitrdi 286	. . . . . 6 ⊢ (𝑎 = ℎ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
227	226	cbvrexvw 3226	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ)))))
228	212, 227	bitrdi 286	. . . 4 ⊢ (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃ℎ ∈ Fin ∃𝑖 ∈ (mzPoly‘ℎ)(ℎ ⊆ 𝐵 ∧ 𝑓 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑖‘(𝑑 ↾ ℎ))))))
229		eqeq1 2740	. . . . . . 7 ⊢ (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
230	229	anbi2d 629	. . . . . 6 ⊢ (𝑒 = 𝑔 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
231	230	2rexbidv 3213	. . . . 5 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
232		fveq2 6842	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233		sseq1 3969	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑎 ⊆ 𝐵 ↔ 𝑗 ⊆ 𝐵))
234		reseq2 5932	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑗 → (𝑑 ↾ 𝑎) = (𝑑 ↾ 𝑗))
235	234	fveq2d 6846	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑗 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑑 ↾ 𝑗)))
236	235	mpteq2dv 5207	. . . . . . . . . 10 ⊢ (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))
237	236	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))))
238	233, 237	anbi12d 631	. . . . . . . 8 ⊢ (𝑎 = 𝑗 → ((𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
239	232, 238	rexeqbidv 3320	. . . . . . 7 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))))))
240		fveq1 6841	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑘 → (𝑏‘(𝑑 ↾ 𝑗)) = (𝑘‘(𝑑 ↾ 𝑗)))
241	240	mpteq2dv 5207	. . . . . . . . . 10 ⊢ (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))
242	241	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
243	242	anbi2d 629	. . . . . . . 8 ⊢ (𝑏 = 𝑘 → ((𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ (𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
244	243	cbvrexvw 3226	. . . . . . 7 ⊢ (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
245	239, 244	bitrdi 286	. . . . . 6 ⊢ (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
246	245	cbvrexvw 3226	. . . . 5 ⊢ (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗)))))
247	231, 246	bitrdi 286	. . . 4 ⊢ (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗 ⊆ 𝐵 ∧ 𝑔 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑘‘(𝑑 ↾ 𝑗))))))
248		eqeq1 2740	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_f + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
249	248	anbi2d 629	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_f + 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
250	249	2rexbidv 3213	. . . 4 ⊢ (𝑒 = (𝑓 ∘_f + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f + 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
251		eqeq1 2740	. . . . . 6 ⊢ (𝑒 = (𝑓 ∘_f · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
252	251	anbi2d 629	. . . . 5 ⊢ (𝑒 = (𝑓 ∘_f · 𝑔) → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
253	252	2rexbidv 3213	. . . 4 ⊢ (𝑒 = (𝑓 ∘_f · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ (𝑓 ∘_f · 𝑔) = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
254		eqeq1 2740	. . . . . 6 ⊢ (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
255	254	anbi2d 629	. . . . 5 ⊢ (𝑒 = 𝐴 → ((𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
256	255	2rexbidv 3213	. . . 4 ⊢ (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝑒 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))))))
257	33, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256	mzpindd 41055	. . 3 ⊢ ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
258	1, 257	mpan 688	. 2 ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))))
259		reseq1 5931	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑑 ↾ 𝑎) = (𝑐 ↾ 𝑎))
260	259	fveq2d 6846	. . . . . 6 ⊢ (𝑑 = 𝑐 → (𝑏‘(𝑑 ↾ 𝑎)) = (𝑏‘(𝑐 ↾ 𝑎)))
261	260	cbvmptv 5218	. . . . 5 ⊢ (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))
262	261	eqeq2i 2749	. . . 4 ⊢ (𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎))))
263	262	anbi2i 623	. . 3 ⊢ ((𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑑 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑑 ↾ 𝑎)))) ↔ (𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑_m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
264	263	2rexbii 3128	. 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 396 ∧ w3a 1087 = wceq 1541 ⊤wtru 1542 ∈ wcel 2106 ∃wrex 3073 Vcvv 3445 ∪ cun 3908 ⊆ wss 3910 ∅c0 4282 {csn 4586 ↦ cmpt 5188 × cxp 5631 ↾ cres 5635 Fn wfn 6491 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 ∘_f cof 7615 ↑_m cmap 8765 Fincfn 8883 + caddc 11054 · cmul 11056 ℤcz 12499 mzPolycmzp 41031

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-nn 12154 df-n0 12414 df-z 12500 df-mzpcl 41032 df-mzp 41033

This theorem is referenced by: mzpcompact2 41061

W3C validator