Users' Mathboxes 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 37840
Description: Lemma for mzpcompact2 37841. (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 1635 . . 3
2 0fin 8344 . . . . . 6 ∅ ∈ Fin
3 0ex 4924 . . . . . . . 8 ∅ ∈ V
4 mzpconst 37824 . . . . . . . 8 ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅))
53, 4mpan 662 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅))
6 0ss 4116 . . . . . . . 8 ∅ ⊆ 𝐵
76a1i 11 . . . . . . 7 (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8 simpr 471 . . . . . . . . . . 11 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → 𝑑 ∈ (ℤ ↑𝑚 𝐵))
9 elmapssres 8034 . . . . . . . . . . 11 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑𝑚 ∅))
108, 6, 9sylancl 566 . . . . . . . . . 10 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑𝑚 ∅))
11 vex 3354 . . . . . . . . . . 11 𝑓 ∈ V
1211fvconst2 6613 . . . . . . . . . 10 ((𝑑 ↾ ∅) ∈ (ℤ ↑𝑚 ∅) → (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1310, 12syl 17 . . . . . . . . 9 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1413mpteq2dva 4878 . . . . . . . 8 (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ 𝑓))
15 fconstmpt 5303 . . . . . . . 8 ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ 𝑓)
1614, 15syl6reqr 2824 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17 fveq1 6331 . . . . . . . . . . 11 (𝑏 = ((ℤ ↑𝑚 ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)))
1817mpteq2dv 4879 . . . . . . . . . 10 (𝑏 = ((ℤ ↑𝑚 ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))
1918eqeq2d 2781 . . . . . . . . 9 (𝑏 = ((ℤ ↑𝑚 ∅) × {𝑓}) → (((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
2019anbi2d 606 . . . . . . . 8 (𝑏 = ((ℤ ↑𝑚 ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
2120rspcev 3460 . . . . . . 7 ((((ℤ ↑𝑚 ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (((ℤ ↑𝑚 ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
225, 7, 16, 21syl12anc 1474 . . . . . 6 (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23 fveq2 6332 . . . . . . . 8 (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24 sseq1 3775 . . . . . . . . 9 (𝑎 = ∅ → (𝑎𝐵 ↔ ∅ ⊆ 𝐵))
25 reseq2 5529 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑑𝑎) = (𝑑 ↾ ∅))
2625fveq2d 6336 . . . . . . . . . . 11 (𝑎 = ∅ → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
2726mpteq2dv 4879 . . . . . . . . . 10 (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
2827eqeq2d 2781 . . . . . . . . 9 (𝑎 = ∅ → (((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
2924, 28anbi12d 608 . . . . . . . 8 (𝑎 = ∅ → ((𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3023, 29rexeqbidv 3302 . . . . . . 7 (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3130rspcev 3460 . . . . . 6 ((∅ ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
322, 22, 31sylancr 567 . . . . 5 (𝑓 ∈ ℤ → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
3332adantl 467 . . . 4 ((⊤ ∧ 𝑓 ∈ ℤ) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
34 snfi 8194 . . . . . 6 {𝑓} ∈ Fin
35 snex 5036 . . . . . . . . 9 {𝑓} ∈ V
36 vsnid 4348 . . . . . . . . 9 𝑓 ∈ {𝑓}
37 mzpproj 37826 . . . . . . . . 9 (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
3835, 36, 37mp2an 664 . . . . . . . 8 (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓})
3938a1i 11 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
40 snssi 4474 . . . . . . 7 (𝑓𝐵 → {𝑓} ⊆ 𝐵)
41 fveq1 6331 . . . . . . . . 9 (𝑔 = 𝑑 → (𝑔𝑓) = (𝑑𝑓))
4241cbvmptv 4884 . . . . . . . 8 (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑑𝑓))
43 simpr 471 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → 𝑑 ∈ (ℤ ↑𝑚 𝐵))
44 simpl 468 . . . . . . . . . . . . 13 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → 𝑓𝐵)
4544snssd 4475 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → {𝑓} ⊆ 𝐵)
46 elmapssres 8034 . . . . . . . . . . . 12 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑𝑚 {𝑓}))
4743, 45, 46syl2anc 565 . . . . . . . . . . 11 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑𝑚 {𝑓}))
48 fveq1 6331 . . . . . . . . . . . 12 (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49 eqid 2771 . . . . . . . . . . . 12 (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))
50 fvex 6342 . . . . . . . . . . . 12 ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
5148, 49, 50fvmpt 6424 . . . . . . . . . . 11 ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑𝑚 {𝑓}) → ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
5247, 51syl 17 . . . . . . . . . 10 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53 fvres 6348 . . . . . . . . . . 11 (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓))
5436, 53ax-mp 5 . . . . . . . . . 10 ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓)
5552, 54syl6req 2822 . . . . . . . . 9 ((𝑓𝐵𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑𝑓) = ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5655mpteq2dva 4878 . . . . . . . 8 (𝑓𝐵 → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑑𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
5742, 56syl5eq 2817 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
58 fveq1 6331 . . . . . . . . . . 11 (𝑏 = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5958mpteq2dv 4879 . . . . . . . . . 10 (𝑏 = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
6059eqeq2d 2781 . . . . . . . . 9 (𝑏 = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) → ((𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))))
6160anbi2d 606 . . . . . . . 8 (𝑏 = (𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))))
6261rspcev 3460 . . . . . . 7 (((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑔 ∈ (ℤ ↑𝑚 {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
6339, 40, 57, 62syl12anc 1474 . . . . . 6 (𝑓𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64 fveq2 6332 . . . . . . . 8 (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65 sseq1 3775 . . . . . . . . 9 (𝑎 = {𝑓} → (𝑎𝐵 ↔ {𝑓} ⊆ 𝐵))
66 reseq2 5529 . . . . . . . . . . . 12 (𝑎 = {𝑓} → (𝑑𝑎) = (𝑑 ↾ {𝑓}))
6766fveq2d 6336 . . . . . . . . . . 11 (𝑎 = {𝑓} → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
6867mpteq2dv 4879 . . . . . . . . . 10 (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
6968eqeq2d 2781 . . . . . . . . 9 (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
7065, 69anbi12d 608 . . . . . . . 8 (𝑎 = {𝑓} → ((𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7164, 70rexeqbidv 3302 . . . . . . 7 (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7271rspcev 3460 . . . . . 6 (({𝑓} ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7334, 63, 72sylancr 567 . . . . 5 (𝑓𝐵 → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7473adantl 467 . . . 4 ((⊤ ∧ 𝑓𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
75 simplll 750 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∈ Fin)
76 simprll 756 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗 ∈ Fin)
77 unfi 8383 . . . . . . . . . . . . . . . . . 18 (( ∈ Fin ∧ 𝑗 ∈ Fin) → (𝑗) ∈ Fin)
7875, 76, 77syl2anc 565 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ Fin)
79 vex 3354 . . . . . . . . . . . . . . . . . . . . . 22 ∈ V
80 vex 3354 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ V
8179, 80unex 7103 . . . . . . . . . . . . . . . . . . . . 21 (𝑗) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ V)
83 ssun1 3927 . . . . . . . . . . . . . . . . . . . . 21 ⊆ (𝑗)
8483a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ⊆ (𝑗))
85 simpllr 752 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑖 ∈ (mzPoly‘))
86 mzpresrename 37839 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ ⊆ (𝑗) ∧ 𝑖 ∈ (mzPoly‘)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
8782, 84, 85, 86syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
88 ssun2 3928 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ⊆ (𝑗)
8988a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗 ⊆ (𝑗))
90 simprlr 757 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91 mzpresrename 37839 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ 𝑗 ⊆ (𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
9282, 89, 90, 91syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
93 mzpaddmpt 37830 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
9487, 92, 93syl2anc 565 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
95 simplr 744 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝐵)
96 simprr 748 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗𝐵)
9795, 96unssd 3940 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ⊆ 𝐵)
98 ovex 6823 . . . . . . . . . . . . . . . . . . . . 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 37839 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝐵𝑖 ∈ (mzPoly‘)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
103101, 95, 85, 102syl3anc 1476 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
104 mzpf 37825 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑𝑚 𝐵)⟶ℤ)
105 ffn 6185 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑𝑚 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑𝑚 𝐵))
106103, 104, 1053syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑𝑚 𝐵))
107 mzpresrename 37839 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝑗𝐵𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
108101, 96, 90, 107syl3anc 1476 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
109 mzpf 37825 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑𝑚 𝐵)⟶ℤ)
110 ffn 6185 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑𝑚 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑𝑚 𝐵))
111108, 109, 1103syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑𝑚 𝐵))
112 ofmpteq 7063 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑𝑚 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑𝑚 𝐵) ∧ (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑𝑚 𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
11399, 106, 111, 112syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
114 elmapi 8031 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 ∈ (ℤ ↑𝑚 𝐵) → 𝑑:𝐵⟶ℤ)
115 fssres 6210 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑑:𝐵⟶ℤ ∧ (𝑗) ⊆ 𝐵) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
116114, 97, 115syl2anr 576 . . . . . . . . . . . . . . . . . . . . . . 23 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
117 zex 11588 . . . . . . . . . . . . . . . . . . . . . . . 24 ℤ ∈ V
118117, 81elmap 8038 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑𝑚 (𝑗)) ↔ (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
119116, 118sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → (𝑑 ↾ (𝑗)) ∈ (ℤ ↑𝑚 (𝑗)))
120 reseq1 5528 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙) = ((𝑑 ↾ (𝑗)) ↾ ))
121120fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑖‘(𝑙)) = (𝑖‘((𝑑 ↾ (𝑗)) ↾ )))
122 reseq1 5528 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙𝑗) = ((𝑑 ↾ (𝑗)) ↾ 𝑗))
123122fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑘‘(𝑙𝑗)) = (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)))
124121, 123oveq12d 6811 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
125 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))
126 ovex 6823 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
127124, 125, 126fvmpt 6424 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑𝑚 (𝑗)) → ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
128119, 127syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
129 resabs1 5568 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑))
13083, 129ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑)
131130fveq2i 6335 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖‘((𝑑 ↾ (𝑗)) ↾ )) = (𝑖‘(𝑑))
132 resabs1 5568 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗))
13388, 132ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗)
134133fveq2i 6335 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑𝑗))
135131, 134oveq12i 6805 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))
136128, 135syl6req 2822 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
137136mpteq2dva 4878 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
138113, 137eqtrd 2805 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
139 fveq1 6331 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
140139mpteq2dv 4879 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
141140eqeq2d 2781 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
142141anbi2d 606 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
143142rspcev 3460 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
14494, 97, 138, 143syl12anc 1474 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
145 mzpmulmpt 37831 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
14687, 92, 145syl2anc 565 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
147 ofmpteq 7063 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑𝑚 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑𝑚 𝐵) ∧ (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑𝑚 𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
14899, 106, 111, 147syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
149121, 123oveq12d 6811 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
150 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))
151 ovex 6823 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
152149, 150, 151fvmpt 6424 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑𝑚 (𝑗)) → ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
153119, 152syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
154131, 134oveq12i 6805 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))
155153, 154syl6req 2822 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑𝑚 𝐵)) → ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
156155mpteq2dva 4878 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
157148, 156eqtrd 2805 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
158 fveq1 6331 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
159158mpteq2dv 4879 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
160159eqeq2d 2781 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
161160anbi2d 606 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
162161rspcev 3460 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ ((𝑙 ∈ (ℤ ↑𝑚 (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
163146, 97, 157, 162syl12anc 1474 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
164 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → (mzPoly‘𝑎) = (mzPoly‘(𝑗)))
165 sseq1 3775 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (𝑎𝐵 ↔ (𝑗) ⊆ 𝐵))
166 reseq2 5529 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑗) → (𝑑𝑎) = (𝑑 ↾ (𝑗)))
167166fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑗) → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ (𝑗))))
168167mpteq2dv 4879 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑗) → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))
169168eqeq2d 2781 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
170165, 169anbi12d 608 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
171164, 170rexeqbidv 3302 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
172168eqeq2d 2781 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
173165, 172anbi12d 608 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
174164, 173rexeqbidv 3302 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
175171, 174anbi12d 608 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑗) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))))
176175rspcev 3460 . . . . . . . . . . . . . . . . 17 (((𝑗) ∈ Fin ∧ (∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
17778, 144, 163, 176syl12anc 1474 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
178177adantlrr 692 . . . . . . . . . . . . . . 15 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
179178adantrrr 696 . . . . . . . . . . . . . 14 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
180 simplrr 755 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → 𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))
181 simprrr 759 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → 𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))
182180, 181oveq12d 6811 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓𝑓 + 𝑔) = ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
183182eqeq1d 2773 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
184183anbi2d 606 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
185184rexbidv 3200 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
186180, 181oveq12d 6811 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓𝑓 · 𝑔) = ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
187186eqeq1d 2773 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
188187anbi2d 606 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
189188rexbidv 3200 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
190185, 189anbi12d 608 . . . . . . . . . . . . . . 15 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 + (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))) ∘𝑓 · (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
191190rexbidv 3200 . . . . . . . . . . . . . 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 3236 . . . . . . . . . . . . 13 (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
194192, 193syl 17 . . . . . . . . . . . 12 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
195194exp32 407 . . . . . . . . . . 11 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) → ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
196195rexlimdvv 3185 . . . . . . . . . 10 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
197196ex 397 . . . . . . . . 9 (( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
198197rexlimivv 3184 . . . . . . . 8 (∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
199198imp 393 . . . . . . 7 ((∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))) ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
200199ad2ant2l 732 . . . . . 6 (((𝑓:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2012003adant1 1124 . . . . 5 ((⊤ ∧ (𝑓:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
202201simpld 476 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
203201simprd 477 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑𝑚 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
204 eqeq1 2775 . . . . . 6 (𝑒 = ((ℤ ↑𝑚 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
205204anbi2d 606 . . . . 5 (𝑒 = ((ℤ ↑𝑚 𝐵) × {𝑓}) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2062052rexbidv 3205 . . . 4 (𝑒 = ((ℤ ↑𝑚 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑𝑚 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
207 eqeq1 2775 . . . . . 6 (𝑒 = (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
208207anbi2d 606 . . . . 5 (𝑒 = (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2092082rexbidv 3205 . . . 4 (𝑒 = (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
210 eqeq1 2775 . . . . . . 7 (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
211210anbi2d 606 . . . . . 6 (𝑒 = 𝑓 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2122112rexbidv 3205 . . . . 5 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
213 fveq2 6332 . . . . . . . 8 (𝑎 = → (mzPoly‘𝑎) = (mzPoly‘))
214 sseq1 3775 . . . . . . . . 9 (𝑎 = → (𝑎𝐵𝐵))
215 reseq2 5529 . . . . . . . . . . . 12 (𝑎 = → (𝑑𝑎) = (𝑑))
216215fveq2d 6336 . . . . . . . . . . 11 (𝑎 = → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑)))
217216mpteq2dv 4879 . . . . . . . . . 10 (𝑎 = → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))))
218217eqeq2d 2781 . . . . . . . . 9 (𝑎 = → (𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑)))))
219214, 218anbi12d 608 . . . . . . . 8 (𝑎 = → ((𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))))))
220213, 219rexeqbidv 3302 . . . . . . 7 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))))))
221 fveq1 6331 . . . . . . . . . . 11 (𝑏 = 𝑖 → (𝑏‘(𝑑)) = (𝑖‘(𝑑)))
222221mpteq2dv 4879 . . . . . . . . . 10 (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))
223222eqeq2d 2781 . . . . . . . . 9 (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))))
224223anbi2d 606 . . . . . . . 8 (𝑏 = 𝑖 → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))))
225224cbvrexv 3321 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))))
226220, 225syl6bb 276 . . . . . 6 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))))
227226cbvrexv 3321 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑)))))
228212, 227syl6bb 276 . . . 4 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑖‘(𝑑))))))
229 eqeq1 2775 . . . . . . 7 (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
230229anbi2d 606 . . . . . 6 (𝑒 = 𝑔 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2312302rexbidv 3205 . . . . 5 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
232 fveq2 6332 . . . . . . . 8 (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233 sseq1 3775 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑎𝐵𝑗𝐵))
234 reseq2 5529 . . . . . . . . . . . 12 (𝑎 = 𝑗 → (𝑑𝑎) = (𝑑𝑗))
235234fveq2d 6336 . . . . . . . . . . 11 (𝑎 = 𝑗 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑𝑗)))
236235mpteq2dv 4879 . . . . . . . . . 10 (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))))
237236eqeq2d 2781 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗)))))
238233, 237anbi12d 608 . . . . . . . 8 (𝑎 = 𝑗 → ((𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
239232, 238rexeqbidv 3302 . . . . . . 7 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
240 fveq1 6331 . . . . . . . . . . 11 (𝑏 = 𝑘 → (𝑏‘(𝑑𝑗)) = (𝑘‘(𝑑𝑗)))
241240mpteq2dv 4879 . . . . . . . . . 10 (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))
242241eqeq2d 2781 . . . . . . . . 9 (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
243242anbi2d 606 . . . . . . . 8 (𝑏 = 𝑘 → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
244243cbvrexv 3321 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
245239, 244syl6bb 276 . . . . . 6 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
246245cbvrexv 3321 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
247231, 246syl6bb 276 . . . 4 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
248 eqeq1 2775 . . . . . 6 (𝑒 = (𝑓𝑓 + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
249248anbi2d 606 . . . . 5 (𝑒 = (𝑓𝑓 + 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2502492rexbidv 3205 . . . 4 (𝑒 = (𝑓𝑓 + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 + 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
251 eqeq1 2775 . . . . . 6 (𝑒 = (𝑓𝑓 · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
252251anbi2d 606 . . . . 5 (𝑒 = (𝑓𝑓 · 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2532522rexbidv 3205 . . . 4 (𝑒 = (𝑓𝑓 · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓𝑓 · 𝑔) = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
254 eqeq1 2775 . . . . . 6 (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
255254anbi2d 606 . . . . 5 (𝑒 = 𝐴 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2562552rexbidv 3205 . . . 4 (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
25733, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256mzpindd 37835 . . 3 ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
2581, 257mpan 662 . 2 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
259 reseq1 5528 . . . . . . 7 (𝑑 = 𝑐 → (𝑑𝑎) = (𝑐𝑎))
260259fveq2d 6336 . . . . . 6 (𝑑 = 𝑐 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑐𝑎)))
261260cbvmptv 4884 . . . . 5 (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎)))
262261eqeq2i 2783 . . . 4 (𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎))))
263262anbi2i 601 . . 3 ((𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
2642632rexbii 3190 . 2 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
265258, 264sylib 208 1 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071   = wceq 1631  wtru 1632  wcel 2145  wrex 3062  Vcvv 3351  cun 3721  wss 3723  c0 4063  {csn 4316  cmpt 4863   × cxp 5247  cres 5251   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  𝑓 cof 7042  𝑚 cmap 8009  Fincfn 8109   + caddc 10141   · cmul 10143  cz 11579  mzPolycmzp 37811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-n0 11495  df-z 11580  df-mzpcl 37812  df-mzp 37813
This theorem is referenced by:  mzpcompact2  37841
  Copyright terms: Public domain W3C validator