Theorem mzpcompact2lem

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

	Ref	Expression
Hypothesis	mzpcompact2lem.i	⊢ 𝐵 ∈ V
Assertion	mzpcompact2lem	⊢ ( 𝐴 ∈ ( mzPoly ‘ 𝐵 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mzpcompact2lem.i	⊢ 𝐵 ∈ V
2		tru	⊢ ⊤
3		0fin	⊢ ∅ ∈ Fin
4		0ex	⊢ ∅ ∈ V
5		mzpconst	⊢ ( ( ∅ ∈ V ∧ 𝑓 ∈ ℤ ) → ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ∈ ( mzPoly ‘ ∅ ) )
6	4 5	mpan	⊢ ( 𝑓 ∈ ℤ → ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ∈ ( mzPoly ‘ ∅ ) )
7		0ss	⊢ ∅ ⊆ 𝐵
8	7	a1i	⊢ ( 𝑓 ∈ ℤ → ∅ ⊆ 𝐵 )
9		fconstmpt	⊢ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ 𝑓 )
10		simpr	⊢ ( ( 𝑓 ∈ ℤ ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → 𝑑 ∈ ( ℤ ↑m 𝐵 ) )
11		elmapssres	⊢ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ∧ ∅ ⊆ 𝐵 ) → ( 𝑑 ↾ ∅ ) ∈ ( ℤ ↑m ∅ ) )
12	10 7 11	sylancl	⊢ ( ( 𝑓 ∈ ℤ ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( 𝑑 ↾ ∅ ) ∈ ( ℤ ↑m ∅ ) )
13		vex	⊢ 𝑓 ∈ V
14	13	fvconst2	⊢ ( ( 𝑑 ↾ ∅ ) ∈ ( ℤ ↑m ∅ ) → ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ‘ ( 𝑑 ↾ ∅ ) ) = 𝑓 )
15	12 14	syl	⊢ ( ( 𝑓 ∈ ℤ ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ‘ ( 𝑑 ↾ ∅ ) ) = 𝑓 )
16	15	mpteq2dva	⊢ ( 𝑓 ∈ ℤ → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ‘ ( 𝑑 ↾ ∅ ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ 𝑓 ) )
17	9 16	eqtr4id	⊢ ( 𝑓 ∈ ℤ → ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ‘ ( 𝑑 ↾ ∅ ) ) ) )
18		fveq1	⊢ ( 𝑏 = ( ( ℤ ↑m ∅ ) × { 𝑓 } ) → ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) = ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ‘ ( 𝑑 ↾ ∅ ) ) )
19	18	mpteq2dv	⊢ ( 𝑏 = ( ( ℤ ↑m ∅ ) × { 𝑓 } ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ‘ ( 𝑑 ↾ ∅ ) ) ) )
20	19	eqeq2d	⊢ ( 𝑏 = ( ( ℤ ↑m ∅ ) × { 𝑓 } ) → ( ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) ↔ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ‘ ( 𝑑 ↾ ∅ ) ) ) ) )
21	20	anbi2d	⊢ ( 𝑏 = ( ( ℤ ↑m ∅ ) × { 𝑓 } ) → ( ( ∅ ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) ) ↔ ( ∅ ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ‘ ( 𝑑 ↾ ∅ ) ) ) ) ) )
22	21	rspcev	⊢ ( ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ∈ ( mzPoly ‘ ∅ ) ∧ ( ∅ ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( ( ℤ ↑m ∅ ) × { 𝑓 } ) ‘ ( 𝑑 ↾ ∅ ) ) ) ) ) → ∃ 𝑏 ∈ ( mzPoly ‘ ∅ ) ( ∅ ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) ) )
23	6 8 17 22	syl12anc	⊢ ( 𝑓 ∈ ℤ → ∃ 𝑏 ∈ ( mzPoly ‘ ∅ ) ( ∅ ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) ) )
24		fveq2	⊢ ( 𝑎 = ∅ → ( mzPoly ‘ 𝑎 ) = ( mzPoly ‘ ∅ ) )
25		sseq1	⊢ ( 𝑎 = ∅ → ( 𝑎 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵 ) )
26		reseq2	⊢ ( 𝑎 = ∅ → ( 𝑑 ↾ 𝑎 ) = ( 𝑑 ↾ ∅ ) )
27	26	fveq2d	⊢ ( 𝑎 = ∅ → ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) = ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) )
28	27	mpteq2dv	⊢ ( 𝑎 = ∅ → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) )
29	28	eqeq2d	⊢ ( 𝑎 = ∅ → ( ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) ) )
30	25 29	anbi12d	⊢ ( 𝑎 = ∅ → ( ( 𝑎 ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( ∅ ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) ) ) )
31	24 30	rexeqbidv	⊢ ( 𝑎 = ∅ → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ ∅ ) ( ∅ ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) ) ) )
32	31	rspcev	⊢ ( ( ∅ ∈ Fin ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ∅ ) ( ∅ ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ∅ ) ) ) ) ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
33	3 23 32	sylancr	⊢ ( 𝑓 ∈ ℤ → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
34	33	adantl	⊢ ( ( ⊤ ∧ 𝑓 ∈ ℤ ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
35		snfi	⊢ { 𝑓 } ∈ Fin
36		vsnex	⊢ { 𝑓 } ∈ V
37		vsnid	⊢ 𝑓 ∈ { 𝑓 }
38		mzpproj	⊢ ( ( { 𝑓 } ∈ V ∧ 𝑓 ∈ { 𝑓 } ) → ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( mzPoly ‘ { 𝑓 } ) )
39	36 37 38	mp2an	⊢ ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( mzPoly ‘ { 𝑓 } )
40	39	a1i	⊢ ( 𝑓 ∈ 𝐵 → ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( mzPoly ‘ { 𝑓 } ) )
41		snssi	⊢ ( 𝑓 ∈ 𝐵 → { 𝑓 } ⊆ 𝐵 )
42		fveq1	⊢ ( 𝑔 = 𝑑 → ( 𝑔 ‘ 𝑓 ) = ( 𝑑 ‘ 𝑓 ) )
43	42	cbvmptv	⊢ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑑 ‘ 𝑓 ) )
44		simpr	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → 𝑑 ∈ ( ℤ ↑m 𝐵 ) )
45		simpl	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → 𝑓 ∈ 𝐵 )
46	45	snssd	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → { 𝑓 } ⊆ 𝐵 )
47		elmapssres	⊢ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ∧ { 𝑓 } ⊆ 𝐵 ) → ( 𝑑 ↾ { 𝑓 } ) ∈ ( ℤ ↑m { 𝑓 } ) )
48	44 46 47	syl2anc	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( 𝑑 ↾ { 𝑓 } ) ∈ ( ℤ ↑m { 𝑓 } ) )
49		fveq1	⊢ ( 𝑔 = ( 𝑑 ↾ { 𝑓 } ) → ( 𝑔 ‘ 𝑓 ) = ( ( 𝑑 ↾ { 𝑓 } ) ‘ 𝑓 ) )
50		eqid	⊢ ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) )
51		fvex	⊢ ( ( 𝑑 ↾ { 𝑓 } ) ‘ 𝑓 ) ∈ V
52	49 50 51	fvmpt	⊢ ( ( 𝑑 ↾ { 𝑓 } ) ∈ ( ℤ ↑m { 𝑓 } ) → ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) = ( ( 𝑑 ↾ { 𝑓 } ) ‘ 𝑓 ) )
53	48 52	syl	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) = ( ( 𝑑 ↾ { 𝑓 } ) ‘ 𝑓 ) )
54		fvres	⊢ ( 𝑓 ∈ { 𝑓 } → ( ( 𝑑 ↾ { 𝑓 } ) ‘ 𝑓 ) = ( 𝑑 ‘ 𝑓 ) )
55	37 54	ax-mp	⊢ ( ( 𝑑 ↾ { 𝑓 } ) ‘ 𝑓 ) = ( 𝑑 ‘ 𝑓 )
56	53 55	eqtr2di	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( 𝑑 ‘ 𝑓 ) = ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) )
57	56	mpteq2dva	⊢ ( 𝑓 ∈ 𝐵 → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑑 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) )
58	43 57	eqtrid	⊢ ( 𝑓 ∈ 𝐵 → ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) )
59		fveq1	⊢ ( 𝑏 = ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) → ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) = ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) )
60	59	mpteq2dv	⊢ ( 𝑏 = ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) )
61	60	eqeq2d	⊢ ( 𝑏 = ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) → ( ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ↔ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) )
62	61	anbi2d	⊢ ( 𝑏 = ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) → ( ( { 𝑓 } ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) ↔ ( { 𝑓 } ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) ) )
63	62	rspcev	⊢ ( ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( mzPoly ‘ { 𝑓 } ) ∧ ( { 𝑓 } ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑔 ∈ ( ℤ ↑m { 𝑓 } ) ↦ ( 𝑔 ‘ 𝑓 ) ) ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) ) → ∃ 𝑏 ∈ ( mzPoly ‘ { 𝑓 } ) ( { 𝑓 } ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) )
64	40 41 58 63	syl12anc	⊢ ( 𝑓 ∈ 𝐵 → ∃ 𝑏 ∈ ( mzPoly ‘ { 𝑓 } ) ( { 𝑓 } ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) )
65		fveq2	⊢ ( 𝑎 = { 𝑓 } → ( mzPoly ‘ 𝑎 ) = ( mzPoly ‘ { 𝑓 } ) )
66		sseq1	⊢ ( 𝑎 = { 𝑓 } → ( 𝑎 ⊆ 𝐵 ↔ { 𝑓 } ⊆ 𝐵 ) )
67		reseq2	⊢ ( 𝑎 = { 𝑓 } → ( 𝑑 ↾ 𝑎 ) = ( 𝑑 ↾ { 𝑓 } ) )
68	67	fveq2d	⊢ ( 𝑎 = { 𝑓 } → ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) = ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) )
69	68	mpteq2dv	⊢ ( 𝑎 = { 𝑓 } → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) )
70	69	eqeq2d	⊢ ( 𝑎 = { 𝑓 } → ( ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) )
71	66 70	anbi12d	⊢ ( 𝑎 = { 𝑓 } → ( ( 𝑎 ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( { 𝑓 } ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) ) )
72	65 71	rexeqbidv	⊢ ( 𝑎 = { 𝑓 } → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ { 𝑓 } ) ( { 𝑓 } ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) ) )
73	72	rspcev	⊢ ( ( { 𝑓 } ∈ Fin ∧ ∃ 𝑏 ∈ ( mzPoly ‘ { 𝑓 } ) ( { 𝑓 } ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ { 𝑓 } ) ) ) ) ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
74	35 64 73	sylancr	⊢ ( 𝑓 ∈ 𝐵 → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
75	74	adantl	⊢ ( ( ⊤ ∧ 𝑓 ∈ 𝐵 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
76		simplll	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ℎ ∈ Fin )
77		simprll	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → 𝑗 ∈ Fin )
78		unfi	⊢ ( ( ℎ ∈ Fin ∧ 𝑗 ∈ Fin ) → ( ℎ ∪ 𝑗 ) ∈ Fin )
79	76 77 78	syl2anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( ℎ ∪ 𝑗 ) ∈ Fin )
80		vex	⊢ ℎ ∈ V
81		vex	⊢ 𝑗 ∈ V
82	80 81	unex	⊢ ( ℎ ∪ 𝑗 ) ∈ V
83	82	a1i	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( ℎ ∪ 𝑗 ) ∈ V )
84		ssun1	⊢ ℎ ⊆ ( ℎ ∪ 𝑗 )
85	84	a1i	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ℎ ⊆ ( ℎ ∪ 𝑗 ) )
86		simpllr	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → 𝑖 ∈ ( mzPoly ‘ ℎ ) )
87		mzpresrename	⊢ ( ( ( ℎ ∪ 𝑗 ) ∈ V ∧ ℎ ⊆ ( ℎ ∪ 𝑗 ) ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) → ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) )
88	83 85 86 87	syl3anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) )
89		ssun2	⊢ 𝑗 ⊆ ( ℎ ∪ 𝑗 )
90	89	a1i	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → 𝑗 ⊆ ( ℎ ∪ 𝑗 ) )
91		simprlr	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → 𝑘 ∈ ( mzPoly ‘ 𝑗 ) )
92		mzpresrename	⊢ ( ( ( ℎ ∪ 𝑗 ) ∈ V ∧ 𝑗 ⊆ ( ℎ ∪ 𝑗 ) ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) → ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) )
93	83 90 91 92	syl3anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) )
94		mzpaddmpt	⊢ ( ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ∧ ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ) → ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) )
95	88 93 94	syl2anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) )
96		simplr	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ℎ ⊆ 𝐵 )
97		simprr	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → 𝑗 ⊆ 𝐵 )
98	96 97	unssd	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( ℎ ∪ 𝑗 ) ⊆ 𝐵 )
99		ovex	⊢ ( ℤ ↑m 𝐵 ) ∈ V
100	99	a1i	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( ℤ ↑m 𝐵 ) ∈ V )
101	1	a1i	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → 𝐵 ∈ V )
102		mzpresrename	⊢ ( ( 𝐵 ∈ V ∧ ℎ ⊆ 𝐵 ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∈ ( mzPoly ‘ 𝐵 ) )
103	101 96 86 102	syl3anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∈ ( mzPoly ‘ 𝐵 ) )
104		mzpf	⊢ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∈ ( mzPoly ‘ 𝐵 ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) : ( ℤ ↑m 𝐵 ) ⟶ ℤ )
105		ffn	⊢ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) : ( ℤ ↑m 𝐵 ) ⟶ ℤ → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) Fn ( ℤ ↑m 𝐵 ) )
106	103 104 105	3syl	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) Fn ( ℤ ↑m 𝐵 ) )
107		mzpresrename	⊢ ( ( 𝐵 ∈ V ∧ 𝑗 ⊆ 𝐵 ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ∈ ( mzPoly ‘ 𝐵 ) )
108	101 97 91 107	syl3anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ∈ ( mzPoly ‘ 𝐵 ) )
109		mzpf	⊢ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ∈ ( mzPoly ‘ 𝐵 ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) : ( ℤ ↑m 𝐵 ) ⟶ ℤ )
110		ffn	⊢ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) : ( ℤ ↑m 𝐵 ) ⟶ ℤ → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) Fn ( ℤ ↑m 𝐵 ) )
111	108 109 110	3syl	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) Fn ( ℤ ↑m 𝐵 ) )
112		ofmpteq	⊢ ( ( ( ℤ ↑m 𝐵 ) ∈ V ∧ ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) Fn ( ℤ ↑m 𝐵 ) ∧ ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) Fn ( ℤ ↑m 𝐵 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
113	100 106 111 112	syl3anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
114		elmapi	⊢ ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) → 𝑑 : 𝐵 ⟶ ℤ )
115		fssres	⊢ ( ( 𝑑 : 𝐵 ⟶ ℤ ∧ ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ) → ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) : ( ℎ ∪ 𝑗 ) ⟶ ℤ )
116	114 98 115	syl2anr	⊢ ( ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) : ( ℎ ∪ 𝑗 ) ⟶ ℤ )
117		zex	⊢ ℤ ∈ V
118	117 82	elmap	⊢ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↔ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) : ( ℎ ∪ 𝑗 ) ⟶ ℤ )
119	116 118	sylibr	⊢ ( ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) )
120		reseq1	⊢ ( 𝑙 = ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) → ( 𝑙 ↾ ℎ ) = ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) )
121	120	fveq2d	⊢ ( 𝑙 = ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) → ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) = ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) )
122		reseq1	⊢ ( 𝑙 = ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) → ( 𝑙 ↾ 𝑗 ) = ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) )
123	122	fveq2d	⊢ ( 𝑙 = ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) → ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) = ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) )
124	121 123	oveq12d	⊢ ( 𝑙 = ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) → ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) = ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) + ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) )
125		eqid	⊢ ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) )
126		ovex	⊢ ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) + ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) ∈ V
127	124 125 126	fvmpt	⊢ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) → ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) = ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) + ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) )
128	119 127	syl	⊢ ( ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) = ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) + ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) )
129		resabs1	⊢ ( ℎ ⊆ ( ℎ ∪ 𝑗 ) → ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) = ( 𝑑 ↾ ℎ ) )
130	84 129	ax-mp	⊢ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) = ( 𝑑 ↾ ℎ )
131	130	fveq2i	⊢ ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) = ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) )
132		resabs1	⊢ ( 𝑗 ⊆ ( ℎ ∪ 𝑗 ) → ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) = ( 𝑑 ↾ 𝑗 ) )
133	89 132	ax-mp	⊢ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) = ( 𝑑 ↾ 𝑗 )
134	133	fveq2i	⊢ ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) = ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) )
135	131 134	oveq12i	⊢ ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) + ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) = ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) )
136	128 135	eqtr2di	⊢ ( ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) = ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) )
137	136	mpteq2dva	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) )
138	113 137	eqtrd	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) )
139		fveq1	⊢ ( 𝑏 = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) → ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) = ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) )
140	139	mpteq2dv	⊢ ( 𝑏 = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) )
141	140	eqeq2d	⊢ ( 𝑏 = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) → ( ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) )
142	141	anbi2d	⊢ ( 𝑏 = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) → ( ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ↔ ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) )
143	142	rspcev	⊢ ( ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ∧ ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) + ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) → ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) )
144	95 98 138 143	syl12anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) )
145		mzpmulmpt	⊢ ( ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ∧ ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ) → ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) )
146	88 93 145	syl2anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) )
147		ofmpteq	⊢ ( ( ( ℤ ↑m 𝐵 ) ∈ V ∧ ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) Fn ( ℤ ↑m 𝐵 ) ∧ ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) Fn ( ℤ ↑m 𝐵 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
148	100 106 111 147	syl3anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
149	121 123	oveq12d	⊢ ( 𝑙 = ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) → ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) = ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) · ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) )
150		eqid	⊢ ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) )
151		ovex	⊢ ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) · ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) ∈ V
152	149 150 151	fvmpt	⊢ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) → ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) = ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) · ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) )
153	119 152	syl	⊢ ( ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) = ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) · ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) )
154	131 134	oveq12i	⊢ ( ( 𝑖 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ ℎ ) ) · ( 𝑘 ‘ ( ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ↾ 𝑗 ) ) ) = ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) )
155	153 154	eqtr2di	⊢ ( ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) ∧ 𝑑 ∈ ( ℤ ↑m 𝐵 ) ) → ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) = ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) )
156	155	mpteq2dva	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) )
157	148 156	eqtrd	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) )
158		fveq1	⊢ ( 𝑏 = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) → ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) = ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) )
159	158	mpteq2dv	⊢ ( 𝑏 = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) )
160	159	eqeq2d	⊢ ( 𝑏 = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) → ( ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) )
161	160	anbi2d	⊢ ( 𝑏 = ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) → ( ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ↔ ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) )
162	161	rspcev	⊢ ( ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ∧ ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( ( 𝑙 ∈ ( ℤ ↑m ( ℎ ∪ 𝑗 ) ) ↦ ( ( 𝑖 ‘ ( 𝑙 ↾ ℎ ) ) · ( 𝑘 ‘ ( 𝑙 ↾ 𝑗 ) ) ) ) ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) → ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) )
163	146 98 157 162	syl12anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) )
164		fveq2	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( mzPoly ‘ 𝑎 ) = ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) )
165		sseq1	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( 𝑎 ⊆ 𝐵 ↔ ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ) )
166		reseq2	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( 𝑑 ↾ 𝑎 ) = ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) )
167	166	fveq2d	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) = ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) )
168	167	mpteq2dv	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) )
169	168	eqeq2d	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) )
170	165 169	anbi12d	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) )
171	164 170	rexeqbidv	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) )
172	168	eqeq2d	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) )
173	165 172	anbi12d	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) )
174	164 173	rexeqbidv	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) )
175	171 174	anbi12d	⊢ ( 𝑎 = ( ℎ ∪ 𝑗 ) → ( ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) ↔ ( ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) ) )
176	175	rspcev	⊢ ( ( ( ℎ ∪ 𝑗 ) ∈ Fin ∧ ( ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ( ℎ ∪ 𝑗 ) ) ( ( ℎ ∪ 𝑗 ) ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ( ℎ ∪ 𝑗 ) ) ) ) ) ) ) → ∃ 𝑎 ∈ Fin ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
177	79 144 163 176	syl12anc	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ℎ ⊆ 𝐵 ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ∃ 𝑎 ∈ Fin ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
178	177	adantlrr	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ 𝑗 ⊆ 𝐵 ) ) → ∃ 𝑎 ∈ Fin ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
179	178	adantrrr	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ∃ 𝑎 ∈ Fin ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
180		simplrr	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) )
181		simprrr	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) )
182	180 181	oveq12d	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( 𝑓 ∘f + 𝑔 ) = ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
183	182	eqeq1d	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
184	183	anbi2d	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
185	184	rexbidv	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f + ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
186	180 181	oveq12d	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( 𝑓 ∘f · 𝑔 ) = ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
187	186	eqeq1d	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
188	187	anbi2d	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
189	188	rexbidv	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ∘f · ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
190	185 189	anbi12d	⊢ ( ( ( ( ℎ ∈ 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	⊢ ( ( ( ( ℎ ∈ 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	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ∃ 𝑎 ∈ Fin ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
193		r19.40	⊢ ( ∃ 𝑎 ∈ Fin ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
194	192 193	syl	⊢ ( ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) ∧ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
195	194	exp32	⊢ ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) → ( ( 𝑗 ∈ Fin ∧ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ) → ( ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) ) ) )
196	195	rexlimdvv	⊢ ( ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) ∧ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) → ( ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) ) )
197	196	ex	⊢ ( ( ℎ ∈ Fin ∧ 𝑖 ∈ ( mzPoly ‘ ℎ ) ) → ( ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) → ( ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) ) ) )
198	197	rexlimivv	⊢ ( ∃ ℎ ∈ Fin ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) → ( ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) ) )
199	198	imp	⊢ ( ( ∃ ℎ ∈ Fin ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ∧ ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
200	199	ad2ant2l	⊢ ( ( ( 𝑓 : ( ℤ ↑m 𝐵 ) ⟶ ℤ ∧ ∃ ℎ ∈ Fin ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( 𝑔 : ( ℤ ↑m 𝐵 ) ⟶ ℤ ∧ ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
201	200	3adant1	⊢ ( ( ⊤ ∧ ( 𝑓 : ( ℤ ↑m 𝐵 ) ⟶ ℤ ∧ ∃ ℎ ∈ Fin ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( 𝑔 : ( ℤ ↑m 𝐵 ) ⟶ ℤ ∧ ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ∧ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
202	201	simpld	⊢ ( ( ⊤ ∧ ( 𝑓 : ( ℤ ↑m 𝐵 ) ⟶ ℤ ∧ ∃ ℎ ∈ Fin ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( 𝑔 : ( ℤ ↑m 𝐵 ) ⟶ ℤ ∧ ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
203	201	simprd	⊢ ( ( ⊤ ∧ ( 𝑓 : ( ℤ ↑m 𝐵 ) ⟶ ℤ ∧ ∃ ℎ ∈ Fin ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) ∧ ( 𝑔 : ( ℤ ↑m 𝐵 ) ⟶ ℤ ∧ ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
204		eqeq1	⊢ ( 𝑒 = ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) → ( 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
205	204	anbi2d	⊢ ( 𝑒 = ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) → ( ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
206	205	2rexbidv	⊢ ( 𝑒 = ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( ( ℤ ↑m 𝐵 ) × { 𝑓 } ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
207		eqeq1	⊢ ( 𝑒 = ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) → ( 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
208	207	anbi2d	⊢ ( 𝑒 = ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) → ( ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
209	208	2rexbidv	⊢ ( 𝑒 = ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑔 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
210		eqeq1	⊢ ( 𝑒 = 𝑓 → ( 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
211	210	anbi2d	⊢ ( 𝑒 = 𝑓 → ( ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
212	211	2rexbidv	⊢ ( 𝑒 = 𝑓 → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
213		fveq2	⊢ ( 𝑎 = ℎ → ( mzPoly ‘ 𝑎 ) = ( mzPoly ‘ ℎ ) )
214		sseq1	⊢ ( 𝑎 = ℎ → ( 𝑎 ⊆ 𝐵 ↔ ℎ ⊆ 𝐵 ) )
215		reseq2	⊢ ( 𝑎 = ℎ → ( 𝑑 ↾ 𝑎 ) = ( 𝑑 ↾ ℎ ) )
216	215	fveq2d	⊢ ( 𝑎 = ℎ → ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) = ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) )
217	216	mpteq2dv	⊢ ( 𝑎 = ℎ → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) ) )
218	217	eqeq2d	⊢ ( 𝑎 = ℎ → ( 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) ) ) )
219	214 218	anbi12d	⊢ ( 𝑎 = ℎ → ( ( 𝑎 ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) )
220	213 219	rexeqbidv	⊢ ( 𝑎 = ℎ → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) )
221		fveq1	⊢ ( 𝑏 = 𝑖 → ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) = ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) )
222	221	mpteq2dv	⊢ ( 𝑏 = 𝑖 → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) )
223	222	eqeq2d	⊢ ( 𝑏 = 𝑖 → ( 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) ) ↔ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) )
224	223	anbi2d	⊢ ( 𝑏 = 𝑖 → ( ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ↔ ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) )
225	224	cbvrexvw	⊢ ( ∃ 𝑏 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ↔ ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) )
226	220 225	bitrdi	⊢ ( 𝑎 = ℎ → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) )
227	226	cbvrexvw	⊢ ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ ℎ ∈ Fin ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) )
228	212 227	bitrdi	⊢ ( 𝑒 = 𝑓 → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ ℎ ∈ Fin ∃ 𝑖 ∈ ( mzPoly ‘ ℎ ) ( ℎ ⊆ 𝐵 ∧ 𝑓 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑖 ‘ ( 𝑑 ↾ ℎ ) ) ) ) ) )
229		eqeq1	⊢ ( 𝑒 = 𝑔 → ( 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
230	229	anbi2d	⊢ ( 𝑒 = 𝑔 → ( ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
231	230	2rexbidv	⊢ ( 𝑒 = 𝑔 → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
232		fveq2	⊢ ( 𝑎 = 𝑗 → ( mzPoly ‘ 𝑎 ) = ( mzPoly ‘ 𝑗 ) )
233		sseq1	⊢ ( 𝑎 = 𝑗 → ( 𝑎 ⊆ 𝐵 ↔ 𝑗 ⊆ 𝐵 ) )
234		reseq2	⊢ ( 𝑎 = 𝑗 → ( 𝑑 ↾ 𝑎 ) = ( 𝑑 ↾ 𝑗 ) )
235	234	fveq2d	⊢ ( 𝑎 = 𝑗 → ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) = ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) )
236	235	mpteq2dv	⊢ ( 𝑎 = 𝑗 → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) ) )
237	236	eqeq2d	⊢ ( 𝑎 = 𝑗 → ( 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
238	233 237	anbi12d	⊢ ( 𝑎 = 𝑗 → ( ( 𝑎 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) )
239	232 238	rexeqbidv	⊢ ( 𝑎 = 𝑗 → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) )
240		fveq1	⊢ ( 𝑏 = 𝑘 → ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) = ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) )
241	240	mpteq2dv	⊢ ( 𝑏 = 𝑘 → ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) )
242	241	eqeq2d	⊢ ( 𝑏 = 𝑘 → ( 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ↔ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
243	242	anbi2d	⊢ ( 𝑏 = 𝑘 → ( ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ↔ ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) )
244	243	cbvrexvw	⊢ ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ↔ ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
245	239 244	bitrdi	⊢ ( 𝑎 = 𝑗 → ( ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) )
246	245	cbvrexvw	⊢ ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) )
247	231 246	bitrdi	⊢ ( 𝑒 = 𝑔 → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑗 ∈ Fin ∃ 𝑘 ∈ ( mzPoly ‘ 𝑗 ) ( 𝑗 ⊆ 𝐵 ∧ 𝑔 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑘 ‘ ( 𝑑 ↾ 𝑗 ) ) ) ) ) )
248		eqeq1	⊢ ( 𝑒 = ( 𝑓 ∘f + 𝑔 ) → ( 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
249	248	anbi2d	⊢ ( 𝑒 = ( 𝑓 ∘f + 𝑔 ) → ( ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
250	249	2rexbidv	⊢ ( 𝑒 = ( 𝑓 ∘f + 𝑔 ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f + 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
251		eqeq1	⊢ ( 𝑒 = ( 𝑓 ∘f · 𝑔 ) → ( 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
252	251	anbi2d	⊢ ( 𝑒 = ( 𝑓 ∘f · 𝑔 ) → ( ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
253	252	2rexbidv	⊢ ( 𝑒 = ( 𝑓 ∘f · 𝑔 ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ ( 𝑓 ∘f · 𝑔 ) = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
254		eqeq1	⊢ ( 𝑒 = 𝐴 → ( 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ 𝐴 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
255	254	anbi2d	⊢ ( 𝑒 = 𝐴 → ( ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
256	255	2rexbidv	⊢ ( 𝑒 = 𝐴 → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝑒 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ) )
257	34 75 202 203 206 209 228 247 250 253 256	mzpindd	⊢ ( ( ⊤ ∧ 𝐴 ∈ ( mzPoly ‘ 𝐵 ) ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
258	2 257	mpan	⊢ ( 𝐴 ∈ ( mzPoly ‘ 𝐵 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) )
259		reseq1	⊢ ( 𝑑 = 𝑐 → ( 𝑑 ↾ 𝑎 ) = ( 𝑐 ↾ 𝑎 ) )
260	259	fveq2d	⊢ ( 𝑑 = 𝑐 → ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) = ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) )
261	260	cbvmptv	⊢ ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) )
262	261	eqeq2i	⊢ ( 𝐴 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ↔ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) )
263	262	anbi2i	⊢ ( ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) )
264	263	2rexbii	⊢ ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑑 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑑 ↾ 𝑎 ) ) ) ) ↔ ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) )
265	258 264	sylib	⊢ ( 𝐴 ∈ ( mzPoly ‘ 𝐵 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝐵 ∧ 𝐴 = ( 𝑐 ∈ ( ℤ ↑m 𝐵 ) ↦ ( 𝑏 ‘ ( 𝑐 ↾ 𝑎 ) ) ) ) )