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

Proof of Theorem mzpcompact2lem
Dummy variables 𝑑 𝑒 𝑓 𝑔 𝑖 𝑗 𝑘 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tru 1542 . . 3
2 0fin 8753 . . . . . 6 ∅ ∈ Fin
3 0ex 5181 . . . . . . . 8 ∅ ∈ V
4 mzpconst 40084 . . . . . . . 8 ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑m ∅) × {𝑓}) ∈ (mzPoly‘∅))
53, 4mpan 689 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑m ∅) × {𝑓}) ∈ (mzPoly‘∅))
6 0ss 4295 . . . . . . . 8 ∅ ⊆ 𝐵
76a1i 11 . . . . . . 7 (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8 fconstmpt 5588 . . . . . . . 8 ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ 𝑓)
9 simpr 488 . . . . . . . . . . 11 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → 𝑑 ∈ (ℤ ↑m 𝐵))
10 elmapssres 8462 . . . . . . . . . . 11 ((𝑑 ∈ (ℤ ↑m 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑m ∅))
119, 6, 10sylancl 589 . . . . . . . . . 10 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑m ∅))
12 vex 3413 . . . . . . . . . . 11 𝑓 ∈ V
1312fvconst2 6963 . . . . . . . . . 10 ((𝑑 ↾ ∅) ∈ (ℤ ↑m ∅) → (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1411, 13syl 17 . . . . . . . . 9 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1514mpteq2dva 5131 . . . . . . . 8 (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ 𝑓))
168, 15eqtr4id 2812 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17 fveq1 6662 . . . . . . . . . . 11 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)))
1817mpteq2dv 5132 . . . . . . . . . 10 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
1918eqeq2d 2769 . . . . . . . . 9 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → (((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
2019anbi2d 631 . . . . . . . 8 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
2120rspcev 3543 . . . . . . 7 ((((ℤ ↑m ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
225, 7, 16, 21syl12anc 835 . . . . . 6 (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23 fveq2 6663 . . . . . . . 8 (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24 sseq1 3919 . . . . . . . . 9 (𝑎 = ∅ → (𝑎𝐵 ↔ ∅ ⊆ 𝐵))
25 reseq2 5823 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑑𝑎) = (𝑑 ↾ ∅))
2625fveq2d 6667 . . . . . . . . . . 11 (𝑎 = ∅ → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
2726mpteq2dv 5132 . . . . . . . . . 10 (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
2827eqeq2d 2769 . . . . . . . . 9 (𝑎 = ∅ → (((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
2924, 28anbi12d 633 . . . . . . . 8 (𝑎 = ∅ → ((𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3023, 29rexeqbidv 3320 . . . . . . 7 (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3130rspcev 3543 . . . . . 6 ((∅ ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
322, 22, 31sylancr 590 . . . . 5 (𝑓 ∈ ℤ → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
3332adantl 485 . . . 4 ((⊤ ∧ 𝑓 ∈ ℤ) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
34 snfi 8627 . . . . . 6 {𝑓} ∈ Fin
35 snex 5304 . . . . . . . . 9 {𝑓} ∈ V
36 vsnid 4562 . . . . . . . . 9 𝑓 ∈ {𝑓}
37 mzpproj 40086 . . . . . . . . 9 (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
3835, 36, 37mp2an 691 . . . . . . . 8 (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓})
3938a1i 11 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
40 snssi 4701 . . . . . . 7 (𝑓𝐵 → {𝑓} ⊆ 𝐵)
41 fveq1 6662 . . . . . . . . 9 (𝑔 = 𝑑 → (𝑔𝑓) = (𝑑𝑓))
4241cbvmptv 5139 . . . . . . . 8 (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑑𝑓))
43 simpr 488 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → 𝑑 ∈ (ℤ ↑m 𝐵))
44 simpl 486 . . . . . . . . . . . . 13 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → 𝑓𝐵)
4544snssd 4702 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → {𝑓} ⊆ 𝐵)
46 elmapssres 8462 . . . . . . . . . . . 12 ((𝑑 ∈ (ℤ ↑m 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑m {𝑓}))
4743, 45, 46syl2anc 587 . . . . . . . . . . 11 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑m {𝑓}))
48 fveq1 6662 . . . . . . . . . . . 12 (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49 eqid 2758 . . . . . . . . . . . 12 (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))
50 fvex 6676 . . . . . . . . . . . 12 ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
5148, 49, 50fvmpt 6764 . . . . . . . . . . 11 ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑m {𝑓}) → ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
5247, 51syl 17 . . . . . . . . . 10 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53 fvres 6682 . . . . . . . . . . 11 (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓))
5436, 53ax-mp 5 . . . . . . . . . 10 ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓)
5552, 54eqtr2di 2810 . . . . . . . . 9 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑𝑓) = ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5655mpteq2dva 5131 . . . . . . . 8 (𝑓𝐵 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑑𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
5742, 56syl5eq 2805 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
58 fveq1 6662 . . . . . . . . . . 11 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5958mpteq2dv 5132 . . . . . . . . . 10 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
6059eqeq2d 2769 . . . . . . . . 9 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → ((𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))))
6160anbi2d 631 . . . . . . . 8 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))))
6261rspcev 3543 . . . . . . 7 (((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
6339, 40, 57, 62syl12anc 835 . . . . . 6 (𝑓𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64 fveq2 6663 . . . . . . . 8 (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65 sseq1 3919 . . . . . . . . 9 (𝑎 = {𝑓} → (𝑎𝐵 ↔ {𝑓} ⊆ 𝐵))
66 reseq2 5823 . . . . . . . . . . . 12 (𝑎 = {𝑓} → (𝑑𝑎) = (𝑑 ↾ {𝑓}))
6766fveq2d 6667 . . . . . . . . . . 11 (𝑎 = {𝑓} → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
6867mpteq2dv 5132 . . . . . . . . . 10 (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
6968eqeq2d 2769 . . . . . . . . 9 (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
7065, 69anbi12d 633 . . . . . . . 8 (𝑎 = {𝑓} → ((𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7164, 70rexeqbidv 3320 . . . . . . 7 (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7271rspcev 3543 . . . . . 6 (({𝑓} ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7334, 63, 72sylancr 590 . . . . 5 (𝑓𝐵 → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7473adantl 485 . . . 4 ((⊤ ∧ 𝑓𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
75 simplll 774 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∈ Fin)
76 simprll 778 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗 ∈ Fin)
77 unfi 8754 . . . . . . . . . . . . . . . . . 18 (( ∈ Fin ∧ 𝑗 ∈ Fin) → (𝑗) ∈ Fin)
7875, 76, 77syl2anc 587 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ Fin)
79 vex 3413 . . . . . . . . . . . . . . . . . . . . . 22 ∈ V
80 vex 3413 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ V
8179, 80unex 7473 . . . . . . . . . . . . . . . . . . . . 21 (𝑗) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ V)
83 ssun1 4079 . . . . . . . . . . . . . . . . . . . . 21 ⊆ (𝑗)
8483a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ⊆ (𝑗))
85 simpllr 775 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑖 ∈ (mzPoly‘))
86 mzpresrename 40099 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ ⊆ (𝑗) ∧ 𝑖 ∈ (mzPoly‘)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
8782, 84, 85, 86syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
88 ssun2 4080 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ⊆ (𝑗)
8988a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗 ⊆ (𝑗))
90 simprlr 779 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91 mzpresrename 40099 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ 𝑗 ⊆ (𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
9282, 89, 90, 91syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
93 mzpaddmpt 40090 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
9487, 92, 93syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
95 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝐵)
96 simprr 772 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗𝐵)
9795, 96unssd 4093 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ⊆ 𝐵)
98 ovex 7189 . . . . . . . . . . . . . . . . . . . . 21 (ℤ ↑m 𝐵) ∈ V
9998a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (ℤ ↑m 𝐵) ∈ V)
100 mzpcompact2lem.i . . . . . . . . . . . . . . . . . . . . . . 23 𝐵 ∈ V
101100a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝐵 ∈ V)
102 mzpresrename 40099 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝐵𝑖 ∈ (mzPoly‘)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
103101, 95, 85, 102syl3anc 1368 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
104 mzpf 40085 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑m 𝐵)⟶ℤ)
105 ffn 6503 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵))
106103, 104, 1053syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵))
107 mzpresrename 40099 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝑗𝐵𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
108101, 96, 90, 107syl3anc 1368 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
109 mzpf 40085 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑m 𝐵)⟶ℤ)
110 ffn 6503 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵))
111108, 109, 1103syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵))
112 ofmpteq 7432 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵) ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
11399, 106, 111, 112syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
114 elmapi 8444 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 ∈ (ℤ ↑m 𝐵) → 𝑑:𝐵⟶ℤ)
115 fssres 6534 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑑:𝐵⟶ℤ ∧ (𝑗) ⊆ 𝐵) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
116114, 97, 115syl2anr 599 . . . . . . . . . . . . . . . . . . . . . . 23 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
117 zex 12042 . . . . . . . . . . . . . . . . . . . . . . . 24 ℤ ∈ V
118117, 81elmap 8466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)) ↔ (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
119116, 118sylibr 237 . . . . . . . . . . . . . . . . . . . . . 22 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)))
120 reseq1 5822 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙) = ((𝑑 ↾ (𝑗)) ↾ ))
121120fveq2d 6667 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑖‘(𝑙)) = (𝑖‘((𝑑 ↾ (𝑗)) ↾ )))
122 reseq1 5822 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙𝑗) = ((𝑑 ↾ (𝑗)) ↾ 𝑗))
123122fveq2d 6667 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑘‘(𝑙𝑗)) = (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)))
124121, 123oveq12d 7174 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
125 eqid 2758 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))
126 ovex 7189 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
127124, 125, 126fvmpt 6764 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
128119, 127syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
129 resabs1 5858 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑))
13083, 129ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑)
131130fveq2i 6666 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖‘((𝑑 ↾ (𝑗)) ↾ )) = (𝑖‘(𝑑))
132 resabs1 5858 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗))
13388, 132ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗)
134133fveq2i 6666 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑𝑗))
135131, 134oveq12i 7168 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))
136128, 135eqtr2di 2810 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
137136mpteq2dva 5131 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
138113, 137eqtrd 2793 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
139 fveq1 6662 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
140139mpteq2dv 5132 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
141140eqeq2d 2769 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
142141anbi2d 631 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
143142rspcev 3543 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
14494, 97, 138, 143syl12anc 835 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
145 mzpmulmpt 40091 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
14687, 92, 145syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
147 ofmpteq 7432 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵) ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
14899, 106, 111, 147syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
149121, 123oveq12d 7174 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
150 eqid 2758 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))
151 ovex 7189 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
152149, 150, 151fvmpt 6764 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
153119, 152syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
154131, 134oveq12i 7168 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))
155153, 154eqtr2di 2810 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
156155mpteq2dva 5131 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
157148, 156eqtrd 2793 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
158 fveq1 6662 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
159158mpteq2dv 5132 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
160159eqeq2d 2769 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
161160anbi2d 631 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
162161rspcev 3543 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
163146, 97, 157, 162syl12anc 835 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
164 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → (mzPoly‘𝑎) = (mzPoly‘(𝑗)))
165 sseq1 3919 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (𝑎𝐵 ↔ (𝑗) ⊆ 𝐵))
166 reseq2 5823 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑗) → (𝑑𝑎) = (𝑑 ↾ (𝑗)))
167166fveq2d 6667 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑗) → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ (𝑗))))
168167mpteq2dv 5132 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑗) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))
169168eqeq2d 2769 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
170165, 169anbi12d 633 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
171164, 170rexeqbidv 3320 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
172168eqeq2d 2769 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
173165, 172anbi12d 633 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
174164, 173rexeqbidv 3320 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
175171, 174anbi12d 633 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑗) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))))
176175rspcev 3543 . . . . . . . . . . . . . . . . 17 (((𝑗) ∈ Fin ∧ (∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
17778, 144, 163, 176syl12anc 835 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
178177adantlrr 720 . . . . . . . . . . . . . . 15 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
179178adantrrr 724 . . . . . . . . . . . . . 14 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
180 simplrr 777 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))
181 simprrr 781 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))
182180, 181oveq12d 7174 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓f + 𝑔) = ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
183182eqeq1d 2760 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
184183anbi2d 631 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
185184rexbidv 3221 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
186180, 181oveq12d 7174 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓f · 𝑔) = ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
187186eqeq1d 2760 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
188187anbi2d 631 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
189188rexbidv 3221 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
190185, 189anbi12d 633 . . . . . . . . . . . . . . 15 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
191190rexbidv 3221 . . . . . . . . . . . . . 14 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
192179, 191mpbird 260 . . . . . . . . . . . . 13 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
193 r19.40 3264 . . . . . . . . . . . . 13 (∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
194192, 193syl 17 . . . . . . . . . . . 12 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
195194exp32 424 . . . . . . . . . . 11 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) → ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
196195rexlimdvv 3217 . . . . . . . . . 10 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
197196ex 416 . . . . . . . . 9 (( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
198197rexlimivv 3216 . . . . . . . 8 (∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
199198imp 410 . . . . . . 7 ((∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))) ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
200199ad2ant2l 745 . . . . . 6 (((𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2012003adant1 1127 . . . . 5 ((⊤ ∧ (𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
202201simpld 498 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
203201simprd 499 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
204 eqeq1 2762 . . . . . 6 (𝑒 = ((ℤ ↑m 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
205204anbi2d 631 . . . . 5 (𝑒 = ((ℤ ↑m 𝐵) × {𝑓}) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2062052rexbidv 3224 . . . 4 (𝑒 = ((ℤ ↑m 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
207 eqeq1 2762 . . . . . 6 (𝑒 = (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
208207anbi2d 631 . . . . 5 (𝑒 = (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2092082rexbidv 3224 . . . 4 (𝑒 = (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
210 eqeq1 2762 . . . . . . 7 (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
211210anbi2d 631 . . . . . 6 (𝑒 = 𝑓 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2122112rexbidv 3224 . . . . 5 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
213 fveq2 6663 . . . . . . . 8 (𝑎 = → (mzPoly‘𝑎) = (mzPoly‘))
214 sseq1 3919 . . . . . . . . 9 (𝑎 = → (𝑎𝐵𝐵))
215 reseq2 5823 . . . . . . . . . . . 12 (𝑎 = → (𝑑𝑎) = (𝑑))
216215fveq2d 6667 . . . . . . . . . . 11 (𝑎 = → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑)))
217216mpteq2dv 5132 . . . . . . . . . 10 (𝑎 = → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))))
218217eqeq2d 2769 . . . . . . . . 9 (𝑎 = → (𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑)))))
219214, 218anbi12d 633 . . . . . . . 8 (𝑎 = → ((𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))))))
220213, 219rexeqbidv 3320 . . . . . . 7 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))))))
221 fveq1 6662 . . . . . . . . . . 11 (𝑏 = 𝑖 → (𝑏‘(𝑑)) = (𝑖‘(𝑑)))
222221mpteq2dv 5132 . . . . . . . . . 10 (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))
223222eqeq2d 2769 . . . . . . . . 9 (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))))
224223anbi2d 631 . . . . . . . 8 (𝑏 = 𝑖 → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))))
225224cbvrexvw 3362 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))))
226220, 225bitrdi 290 . . . . . 6 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))))
227226cbvrexvw 3362 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))))
228212, 227bitrdi 290 . . . 4 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))))
229 eqeq1 2762 . . . . . . 7 (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
230229anbi2d 631 . . . . . 6 (𝑒 = 𝑔 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2312302rexbidv 3224 . . . . 5 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
232 fveq2 6663 . . . . . . . 8 (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233 sseq1 3919 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑎𝐵𝑗𝐵))
234 reseq2 5823 . . . . . . . . . . . 12 (𝑎 = 𝑗 → (𝑑𝑎) = (𝑑𝑗))
235234fveq2d 6667 . . . . . . . . . . 11 (𝑎 = 𝑗 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑𝑗)))
236235mpteq2dv 5132 . . . . . . . . . 10 (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))))
237236eqeq2d 2769 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗)))))
238233, 237anbi12d 633 . . . . . . . 8 (𝑎 = 𝑗 → ((𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
239232, 238rexeqbidv 3320 . . . . . . 7 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
240 fveq1 6662 . . . . . . . . . . 11 (𝑏 = 𝑘 → (𝑏‘(𝑑𝑗)) = (𝑘‘(𝑑𝑗)))
241240mpteq2dv 5132 . . . . . . . . . 10 (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))
242241eqeq2d 2769 . . . . . . . . 9 (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
243242anbi2d 631 . . . . . . . 8 (𝑏 = 𝑘 → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
244243cbvrexvw 3362 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
245239, 244bitrdi 290 . . . . . 6 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
246245cbvrexvw 3362 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
247231, 246bitrdi 290 . . . 4 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
248 eqeq1 2762 . . . . . 6 (𝑒 = (𝑓f + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
249248anbi2d 631 . . . . 5 (𝑒 = (𝑓f + 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2502492rexbidv 3224 . . . 4 (𝑒 = (𝑓f + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
251 eqeq1 2762 . . . . . 6 (𝑒 = (𝑓f · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
252251anbi2d 631 . . . . 5 (𝑒 = (𝑓f · 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2532522rexbidv 3224 . . . 4 (𝑒 = (𝑓f · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
254 eqeq1 2762 . . . . . 6 (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
255254anbi2d 631 . . . . 5 (𝑒 = 𝐴 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2562552rexbidv 3224 . . . 4 (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
25733, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256mzpindd 40095 . . 3 ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
2581, 257mpan 689 . 2 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
259 reseq1 5822 . . . . . . 7 (𝑑 = 𝑐 → (𝑑𝑎) = (𝑐𝑎))
260259fveq2d 6667 . . . . . 6 (𝑑 = 𝑐 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑐𝑎)))
261260cbvmptv 5139 . . . . 5 (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))
262261eqeq2i 2771 . . . 4 (𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎))))
263262anbi2i 625 . . 3 ((𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
2642632rexbii 3176 . 2 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
265258, 264sylib 221 1 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ⊤wtru 1539   ∈ wcel 2111  ∃wrex 3071  Vcvv 3409   ∪ cun 3858   ⊆ wss 3860  ∅c0 4227  {csn 4525   ↦ cmpt 5116   × cxp 5526   ↾ cres 5530   Fn wfn 6335  ⟶wf 6336  ‘cfv 6340  (class class class)co 7156   ∘f cof 7409   ↑m cmap 8422  Fincfn 8540   + caddc 10591   · cmul 10593  ℤcz 12033  mzPolycmzp 40071 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-of 7411  df-om 7586  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-1o 8118  df-er 8305  df-map 8424  df-en 8541  df-dom 8542  df-sdom 8543  df-fin 8544  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-nn 11688  df-n0 11948  df-z 12034  df-mzpcl 40072  df-mzp 40073 This theorem is referenced by:  mzpcompact2  40101
 Copyright terms: Public domain W3C validator