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 36829
 Description: Lemma for mzpcompact2 36830. (Contributed by Stefan O'Rear, 9-Oct-2014.)
Hypothesis
Ref Expression
mzpcompact2lem.i 𝐵 ∈ V
Assertion
Ref Expression
mzpcompact2lem (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
Distinct variable groups:   𝐴,𝑎,𝑏   𝐵,𝑎,𝑏,𝑐
Allowed substitution hint:   𝐴(𝑐)

Proof of Theorem mzpcompact2lem
Dummy variables 𝑑 𝑒 𝑓 𝑔 𝑖 𝑗 𝑘 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tru 1484 . . 3
2 0fin 8140 . . . . . 6 ∅ ∈ Fin
3 0ex 4755 . . . . . . . 8 ∅ ∈ V
4 mzpconst 36813 . . . . . . . 8 ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅))
53, 4mpan 705 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅))
6 0ss 3949 . . . . . . . 8 ∅ ⊆ 𝐵
76a1i 11 . . . . . . 7 (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8 simpr 477 . . . . . . . . . . 11 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → 𝑑 ∈ (ℤ ↑𝑚 𝐵))
9 elmapssres 7834 . . . . . . . . . . 11 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑𝑚 ∅))
108, 6, 9sylancl 693 . . . . . . . . . 10 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑𝑚 ∅))
11 vex 3192 . . . . . . . . . . 11 𝑓 ∈ V
1211fvconst2 6429 . . . . . . . . . 10 ((𝑑 ↾ ∅) ∈ (ℤ ↑𝑚 ∅) → (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1310, 12syl 17 . . . . . . . . 9 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1413mpteq2dva 4709 . . . . . . . 8 (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ 𝑓))
15 fconstmpt 5128 . . . . . . . 8 ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ 𝑓)
1614, 15syl6reqr 2674 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17 fveq1 6152 . . . . . . . . . . 11 (𝑏 = ((ℤ ↑𝑚 ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)))
1817mpteq2dv 4710 . . . . . . . . . 10 (𝑏 = ((ℤ ↑𝑚 ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))
1918eqeq2d 2631 . . . . . . . . 9 (𝑏 = ((ℤ ↑𝑚 ∅) × {𝑓}) → (((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
2019anbi2d 739 . . . . . . . 8 (𝑏 = ((ℤ ↑𝑚 ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
2120rspcev 3298 . . . . . . 7 ((((ℤ ↑𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
225, 7, 16, 21syl12anc 1321 . . . . . 6 (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23 fveq2 6153 . . . . . . . 8 (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24 sseq1 3610 . . . . . . . . 9 (𝑎 = ∅ → (𝑎𝐵 ↔ ∅ ⊆ 𝐵))
25 reseq2 5356 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑑𝑎) = (𝑑 ↾ ∅))
2625fveq2d 6157 . . . . . . . . . . 11 (𝑎 = ∅ → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
2726mpteq2dv 4710 . . . . . . . . . 10 (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
2827eqeq2d 2631 . . . . . . . . 9 (𝑎 = ∅ → (((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
2924, 28anbi12d 746 . . . . . . . 8 (𝑎 = ∅ → ((𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3023, 29rexeqbidv 3145 . . . . . . 7 (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3130rspcev 3298 . . . . . 6 ((∅ ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
322, 22, 31sylancr 694 . . . . 5 (𝑓 ∈ ℤ → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
3332adantl 482 . . . 4 ((⊤ ∧ 𝑓 ∈ ℤ) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
34 snfi 7990 . . . . . 6 {𝑓} ∈ Fin
35 snex 4874 . . . . . . . . 9 {𝑓} ∈ V
36 vsnid 4185 . . . . . . . . 9 𝑓 ∈ {𝑓}
37 mzpproj 36815 . . . . . . . . 9 (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
3835, 36, 37mp2an 707 . . . . . . . 8 (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓})
3938a1i 11 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
40 snssi 4313 . . . . . . 7 (𝑓𝐵 → {𝑓} ⊆ 𝐵)
41 fveq1 6152 . . . . . . . . 9 (𝑔 = 𝑑 → (𝑔𝑓) = (𝑑𝑓))
4241cbvmptv 4715 . . . . . . . 8 (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑑𝑓))
43 simpr 477 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → 𝑑 ∈ (ℤ ↑𝑚 𝐵))
44 simpl 473 . . . . . . . . . . . . 13 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → 𝑓𝐵)
4544snssd 4314 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → {𝑓} ⊆ 𝐵)
46 elmapssres 7834 . . . . . . . . . . . 12 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑𝑚 {𝑓}))
4743, 45, 46syl2anc 692 . . . . . . . . . . 11 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑𝑚 {𝑓}))
48 fveq1 6152 . . . . . . . . . . . 12 (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49 eqid 2621 . . . . . . . . . . . 12 (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))
50 fvex 6163 . . . . . . . . . . . 12 ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
5148, 49, 50fvmpt 6244 . . . . . . . . . . 11 ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑𝑚 {𝑓}) → ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
5247, 51syl 17 . . . . . . . . . 10 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53 fvres 6169 . . . . . . . . . . 11 (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓))
5436, 53ax-mp 5 . . . . . . . . . 10 ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓)
5552, 54syl6req 2672 . . . . . . . . 9 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑𝑓) = ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5655mpteq2dva 4709 . . . . . . . 8 (𝑓𝐵 → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑑𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
5742, 56syl5eq 2667 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
58 fveq1 6152 . . . . . . . . . . 11 (𝑏 = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5958mpteq2dv 4710 . . . . . . . . . 10 (𝑏 = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
6059eqeq2d 2631 . . . . . . . . 9 (𝑏 = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) → ((𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))))
6160anbi2d 739 . . . . . . . 8 (𝑏 = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))))
6261rspcev 3298 . . . . . . 7 (((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
6339, 40, 57, 62syl12anc 1321 . . . . . 6 (𝑓𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64 fveq2 6153 . . . . . . . 8 (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65 sseq1 3610 . . . . . . . . 9 (𝑎 = {𝑓} → (𝑎𝐵 ↔ {𝑓} ⊆ 𝐵))
66 reseq2 5356 . . . . . . . . . . . 12 (𝑎 = {𝑓} → (𝑑𝑎) = (𝑑 ↾ {𝑓}))
6766fveq2d 6157 . . . . . . . . . . 11 (𝑎 = {𝑓} → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
6867mpteq2dv 4710 . . . . . . . . . 10 (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
6968eqeq2d 2631 . . . . . . . . 9 (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
7065, 69anbi12d 746 . . . . . . . 8 (𝑎 = {𝑓} → ((𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7164, 70rexeqbidv 3145 . . . . . . 7 (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7271rspcev 3298 . . . . . 6 (({𝑓} ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7334, 63, 72sylancr 694 . . . . 5 (𝑓𝐵 → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7473adantl 482 . . . 4 ((⊤ ∧ 𝑓𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
75 simplll 797 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∈ Fin)
76 simprll 801 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗 ∈ Fin)
77 unfi 8179 . . . . . . . . . . . . . . . . . 18 (( ∈ Fin ∧ 𝑗 ∈ Fin) → (𝑗) ∈ Fin)
7875, 76, 77syl2anc 692 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ Fin)
79 vex 3192 . . . . . . . . . . . . . . . . . . . . . 22 ∈ V
80 vex 3192 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ V
8179, 80unex 6916 . . . . . . . . . . . . . . . . . . . . 21 (𝑗) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ V)
83 ssun1 3759 . . . . . . . . . . . . . . . . . . . . 21 ⊆ (𝑗)
8483a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ⊆ (𝑗))
85 simpllr 798 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑖 ∈ (mzPoly‘))
86 mzpresrename 36828 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ ⊆ (𝑗) ∧ 𝑖 ∈ (mzPoly‘)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
8782, 84, 85, 86syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
88 ssun2 3760 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ⊆ (𝑗)
8988a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗 ⊆ (𝑗))
90 simprlr 802 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91 mzpresrename 36828 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ 𝑗 ⊆ (𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
9282, 89, 90, 91syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
93 mzpaddmpt 36819 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
9487, 92, 93syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
95 simplr 791 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝐵)
96 simprr 795 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗𝐵)
9795, 96unssd 3772 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ⊆ 𝐵)
98 ovex 6638 . . . . . . . . . . . . . . . . . . . . 21 (ℤ ↑𝑚 𝐵) ∈ V
9998a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (ℤ ↑𝑚 𝐵) ∈ V)
100 mzpcompact2lem.i . . . . . . . . . . . . . . . . . . . . . . 23 𝐵 ∈ V
101100a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝐵 ∈ V)
102 mzpresrename 36828 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝐵𝑖 ∈ (mzPoly‘)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
103101, 95, 85, 102syl3anc 1323 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
104 mzpf 36814 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑𝑚 𝐵)⟶ℤ)
105 ffn 6007 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑𝑚 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑𝑚 𝐵))
106103, 104, 1053syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑𝑚 𝐵))
107 mzpresrename 36828 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝑗𝐵𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
108101, 96, 90, 107syl3anc 1323 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
109 mzpf 36814 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑𝑚 𝐵)⟶ℤ)
110 ffn 6007 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑𝑚 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑𝑚 𝐵))
111108, 109, 1103syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑𝑚 𝐵))
112 ofmpteq 6876 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑𝑚 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑𝑚 𝐵) ∧ (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑𝑚 𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
11399, 106, 111, 112syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
114 elmapi 7831 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 ∈ (ℤ ↑𝑚 𝐵) → 𝑑:𝐵⟶ℤ)
115 fssres 6032 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑑:𝐵⟶ℤ ∧ (𝑗) ⊆ 𝐵) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
116114, 97, 115syl2anr 495 . . . . . . . . . . . . . . . . . . . . . . 23 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
117 zex 11338 . . . . . . . . . . . . . . . . . . . . . . . 24 ℤ ∈ V
118117, 81elmap 7838 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑𝑚 (𝑗)) ↔ (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
119116, 118sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑 ↾ (𝑗)) ∈ (ℤ ↑𝑚 (𝑗)))
120 reseq1 5355 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙) = ((𝑑 ↾ (𝑗)) ↾ ))
121120fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑖‘(𝑙)) = (𝑖‘((𝑑 ↾ (𝑗)) ↾ )))
122 reseq1 5355 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙𝑗) = ((𝑑 ↾ (𝑗)) ↾ 𝑗))
123122fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑘‘(𝑙𝑗)) = (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)))
124121, 123oveq12d 6628 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
125 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))
126 ovex 6638 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
127124, 125, 126fvmpt 6244 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑𝑚 (𝑗)) → ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
128119, 127syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
129 resabs1 5391 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑))
13083, 129ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑)
131130fveq2i 6156 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖‘((𝑑 ↾ (𝑗)) ↾ )) = (𝑖‘(𝑑))
132 resabs1 5391 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗))
13388, 132ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗)
134133fveq2i 6156 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑𝑗))
135131, 134oveq12i 6622 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))
136128, 135syl6req 2672 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
137136mpteq2dva 4709 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
138113, 137eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
139 fveq1 6152 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
140139mpteq2dv 4710 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
141140eqeq2d 2631 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
142141anbi2d 739 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
143142rspcev 3298 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
14494, 97, 138, 143syl12anc 1321 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
145 mzpmulmpt 36820 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
14687, 92, 145syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
147 ofmpteq 6876 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑𝑚 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑𝑚 𝐵) ∧ (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑𝑚 𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
14899, 106, 111, 147syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
149121, 123oveq12d 6628 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
150 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))
151 ovex 6638 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
152149, 150, 151fvmpt 6244 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑𝑚 (𝑗)) → ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
153119, 152syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
154131, 134oveq12i 6622 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))
155153, 154syl6req 2672 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
156155mpteq2dva 4709 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
157148, 156eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
158 fveq1 6152 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
159158mpteq2dv 4710 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
160159eqeq2d 2631 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
161160anbi2d 739 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
162161rspcev 3298 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
163146, 97, 157, 162syl12anc 1321 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
164 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → (mzPoly‘𝑎) = (mzPoly‘(𝑗)))
165 sseq1 3610 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (𝑎𝐵 ↔ (𝑗) ⊆ 𝐵))
166 reseq2 5356 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑗) → (𝑑𝑎) = (𝑑 ↾ (𝑗)))
167166fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑗) → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ (𝑗))))
168167mpteq2dv 4710 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑗) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))
169168eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
170165, 169anbi12d 746 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
171164, 170rexeqbidv 3145 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
172168eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
173165, 172anbi12d 746 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
174164, 173rexeqbidv 3145 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
175171, 174anbi12d 746 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑗) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))))
176175rspcev 3298 . . . . . . . . . . . . . . . . 17 (((𝑗) ∈ Fin ∧ (∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
17778, 144, 163, 176syl12anc 1321 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
178177adantlrr 756 . . . . . . . . . . . . . . 15 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
179178adantrrr 760 . . . . . . . . . . . . . 14 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
180 simplrr 800 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → 𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))
181 simprrr 804 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → 𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))
182180, 181oveq12d 6628 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓𝑓 + 𝑔) = ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
183182eqeq1d 2623 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
184183anbi2d 739 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
185184rexbidv 3046 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
186180, 181oveq12d 6628 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓𝑓 · 𝑔) = ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
187186eqeq1d 2623 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
188187anbi2d 739 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
189188rexbidv 3046 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
190185, 189anbi12d 746 . . . . . . . . . . . . . . 15 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
191190rexbidv 3046 . . . . . . . . . . . . . 14 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
192179, 191mpbird 247 . . . . . . . . . . . . 13 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
193 r19.40 3081 . . . . . . . . . . . . 13 (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
194192, 193syl 17 . . . . . . . . . . . 12 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
195194exp32 630 . . . . . . . . . . 11 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) → ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
196195rexlimdvv 3031 . . . . . . . . . 10 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
197196ex 450 . . . . . . . . 9 (( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
198197rexlimivv 3030 . . . . . . . 8 (∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
199198imp 445 . . . . . . 7 ((∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))) ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
200199ad2ant2l 781 . . . . . 6 (((𝑓:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2012003adant1 1077 . . . . 5 ((⊤ ∧ (𝑓:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
202201simpld 475 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
203201simprd 479 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
204 eqeq1 2625 . . . . . 6 (𝑒 = ((ℤ ↑𝑚 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
205204anbi2d 739 . . . . 5 (𝑒 = ((ℤ ↑𝑚 𝐵) × {𝑓}) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2062052rexbidv 3051 . . . 4 (𝑒 = ((ℤ ↑𝑚 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
207 eqeq1 2625 . . . . . 6 (𝑒 = (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
208207anbi2d 739 . . . . 5 (𝑒 = (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2092082rexbidv 3051 . . . 4 (𝑒 = (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
210 eqeq1 2625 . . . . . . 7 (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
211210anbi2d 739 . . . . . 6 (𝑒 = 𝑓 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2122112rexbidv 3051 . . . . 5 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
213 fveq2 6153 . . . . . . . 8 (𝑎 = → (mzPoly‘𝑎) = (mzPoly‘))
214 sseq1 3610 . . . . . . . . 9 (𝑎 = → (𝑎𝐵𝐵))
215 reseq2 5356 . . . . . . . . . . . 12 (𝑎 = → (𝑑𝑎) = (𝑑))
216215fveq2d 6157 . . . . . . . . . . 11 (𝑎 = → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑)))
217216mpteq2dv 4710 . . . . . . . . . 10 (𝑎 = → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))))
218217eqeq2d 2631 . . . . . . . . 9 (𝑎 = → (𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑)))))
219214, 218anbi12d 746 . . . . . . . 8 (𝑎 = → ((𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))))))
220213, 219rexeqbidv 3145 . . . . . . 7 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))))))
221 fveq1 6152 . . . . . . . . . . 11 (𝑏 = 𝑖 → (𝑏‘(𝑑)) = (𝑖‘(𝑑)))
222221mpteq2dv 4710 . . . . . . . . . 10 (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))
223222eqeq2d 2631 . . . . . . . . 9 (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))))
224223anbi2d 739 . . . . . . . 8 (𝑏 = 𝑖 → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))))
225224cbvrexv 3163 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))))
226220, 225syl6bb 276 . . . . . 6 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))))
227226cbvrexv 3163 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))))
228212, 227syl6bb 276 . . . 4 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))))
229 eqeq1 2625 . . . . . . 7 (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
230229anbi2d 739 . . . . . 6 (𝑒 = 𝑔 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2312302rexbidv 3051 . . . . 5 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
232 fveq2 6153 . . . . . . . 8 (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233 sseq1 3610 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑎𝐵𝑗𝐵))
234 reseq2 5356 . . . . . . . . . . . 12 (𝑎 = 𝑗 → (𝑑𝑎) = (𝑑𝑗))
235234fveq2d 6157 . . . . . . . . . . 11 (𝑎 = 𝑗 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑𝑗)))
236235mpteq2dv 4710 . . . . . . . . . 10 (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))))
237236eqeq2d 2631 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗)))))
238233, 237anbi12d 746 . . . . . . . 8 (𝑎 = 𝑗 → ((𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
239232, 238rexeqbidv 3145 . . . . . . 7 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
240 fveq1 6152 . . . . . . . . . . 11 (𝑏 = 𝑘 → (𝑏‘(𝑑𝑗)) = (𝑘‘(𝑑𝑗)))
241240mpteq2dv 4710 . . . . . . . . . 10 (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))
242241eqeq2d 2631 . . . . . . . . 9 (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
243242anbi2d 739 . . . . . . . 8 (𝑏 = 𝑘 → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
244243cbvrexv 3163 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
245239, 244syl6bb 276 . . . . . 6 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
246245cbvrexv 3163 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
247231, 246syl6bb 276 . . . 4 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
248 eqeq1 2625 . . . . . 6 (𝑒 = (𝑓𝑓 + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
249248anbi2d 739 . . . . 5 (𝑒 = (𝑓𝑓 + 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2502492rexbidv 3051 . . . 4 (𝑒 = (𝑓𝑓 + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
251 eqeq1 2625 . . . . . 6 (𝑒 = (𝑓𝑓 · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
252251anbi2d 739 . . . . 5 (𝑒 = (𝑓𝑓 · 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2532522rexbidv 3051 . . . 4 (𝑒 = (𝑓𝑓 · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
254 eqeq1 2625 . . . . . 6 (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
255254anbi2d 739 . . . . 5 (𝑒 = 𝐴 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2562552rexbidv 3051 . . . 4 (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
25733, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256mzpindd 36824 . . 3 ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
2581, 257mpan 705 . 2 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
259 reseq1 5355 . . . . . . 7 (𝑑 = 𝑐 → (𝑑𝑎) = (𝑐𝑎))
260259fveq2d 6157 . . . . . 6 (𝑑 = 𝑐 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑐𝑎)))
261260cbvmptv 4715 . . . . 5 (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎)))
262261eqeq2i 2633 . . . 4 (𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎))))
263262anbi2i 729 . . 3 ((𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
2642632rexbii 3036 . 2 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
265258, 264sylib 208 1 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ⊤wtru 1481   ∈ wcel 1987  ∃wrex 2908  Vcvv 3189   ∪ cun 3557   ⊆ wss 3559  ∅c0 3896  {csn 4153   ↦ cmpt 4678   × cxp 5077   ↾ cres 5081   Fn wfn 5847  ⟶wf 5848  ‘cfv 5852  (class class class)co 6610   ∘𝑓 cof 6855   ↑𝑚 cmap 7809  Fincfn 7907   + caddc 9891   · cmul 9893  ℤcz 11329  mzPolycmzp 36800 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-nn 10973  df-n0 11245  df-z 11330  df-mzpcl 36801  df-mzp 36802 This theorem is referenced by:  mzpcompact2  36830
 Copyright terms: Public domain W3C validator