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 39228
Description: Lemma for mzpcompact2 39229. (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 1532 . . 3
2 0fin 8735 . . . . . 6 ∅ ∈ Fin
3 0ex 5203 . . . . . . . 8 ∅ ∈ V
4 mzpconst 39212 . . . . . . . 8 ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑m ∅) × {𝑓}) ∈ (mzPoly‘∅))
53, 4mpan 686 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑m ∅) × {𝑓}) ∈ (mzPoly‘∅))
6 0ss 4349 . . . . . . . 8 ∅ ⊆ 𝐵
76a1i 11 . . . . . . 7 (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8 simpr 485 . . . . . . . . . . 11 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → 𝑑 ∈ (ℤ ↑m 𝐵))
9 elmapssres 8421 . . . . . . . . . . 11 ((𝑑 ∈ (ℤ ↑m 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑m ∅))
108, 6, 9sylancl 586 . . . . . . . . . 10 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑m ∅))
11 vex 3498 . . . . . . . . . . 11 𝑓 ∈ V
1211fvconst2 6959 . . . . . . . . . 10 ((𝑑 ↾ ∅) ∈ (ℤ ↑m ∅) → (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1310, 12syl 17 . . . . . . . . 9 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1413mpteq2dva 5153 . . . . . . . 8 (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ 𝑓))
15 fconstmpt 5608 . . . . . . . 8 ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ 𝑓)
1614, 15syl6reqr 2875 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17 fveq1 6663 . . . . . . . . . . 11 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)))
1817mpteq2dv 5154 . . . . . . . . . 10 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
1918eqeq2d 2832 . . . . . . . . 9 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → (((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
2019anbi2d 628 . . . . . . . 8 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
2120rspcev 3622 . . . . . . 7 ((((ℤ ↑m ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
225, 7, 16, 21syl12anc 832 . . . . . 6 (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23 fveq2 6664 . . . . . . . 8 (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24 sseq1 3991 . . . . . . . . 9 (𝑎 = ∅ → (𝑎𝐵 ↔ ∅ ⊆ 𝐵))
25 reseq2 5842 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑑𝑎) = (𝑑 ↾ ∅))
2625fveq2d 6668 . . . . . . . . . . 11 (𝑎 = ∅ → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
2726mpteq2dv 5154 . . . . . . . . . 10 (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
2827eqeq2d 2832 . . . . . . . . 9 (𝑎 = ∅ → (((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
2924, 28anbi12d 630 . . . . . . . 8 (𝑎 = ∅ → ((𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3023, 29rexeqbidv 3403 . . . . . . 7 (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3130rspcev 3622 . . . . . 6 ((∅ ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
322, 22, 31sylancr 587 . . . . 5 (𝑓 ∈ ℤ → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
3332adantl 482 . . . 4 ((⊤ ∧ 𝑓 ∈ ℤ) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
34 snfi 8583 . . . . . 6 {𝑓} ∈ Fin
35 snex 5323 . . . . . . . . 9 {𝑓} ∈ V
36 vsnid 4594 . . . . . . . . 9 𝑓 ∈ {𝑓}
37 mzpproj 39214 . . . . . . . . 9 (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
3835, 36, 37mp2an 688 . . . . . . . 8 (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓})
3938a1i 11 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
40 snssi 4735 . . . . . . 7 (𝑓𝐵 → {𝑓} ⊆ 𝐵)
41 fveq1 6663 . . . . . . . . 9 (𝑔 = 𝑑 → (𝑔𝑓) = (𝑑𝑓))
4241cbvmptv 5161 . . . . . . . 8 (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑑𝑓))
43 simpr 485 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → 𝑑 ∈ (ℤ ↑m 𝐵))
44 simpl 483 . . . . . . . . . . . . 13 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → 𝑓𝐵)
4544snssd 4736 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → {𝑓} ⊆ 𝐵)
46 elmapssres 8421 . . . . . . . . . . . 12 ((𝑑 ∈ (ℤ ↑m 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑m {𝑓}))
4743, 45, 46syl2anc 584 . . . . . . . . . . 11 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑m {𝑓}))
48 fveq1 6663 . . . . . . . . . . . 12 (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49 eqid 2821 . . . . . . . . . . . 12 (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))
50 fvex 6677 . . . . . . . . . . . 12 ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
5148, 49, 50fvmpt 6762 . . . . . . . . . . 11 ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑m {𝑓}) → ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
5247, 51syl 17 . . . . . . . . . 10 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53 fvres 6683 . . . . . . . . . . 11 (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓))
5436, 53ax-mp 5 . . . . . . . . . 10 ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓)
5552, 54syl6req 2873 . . . . . . . . 9 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑𝑓) = ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5655mpteq2dva 5153 . . . . . . . 8 (𝑓𝐵 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑑𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
5742, 56syl5eq 2868 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
58 fveq1 6663 . . . . . . . . . . 11 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5958mpteq2dv 5154 . . . . . . . . . 10 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
6059eqeq2d 2832 . . . . . . . . 9 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → ((𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))))
6160anbi2d 628 . . . . . . . 8 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))))
6261rspcev 3622 . . . . . . 7 (((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
6339, 40, 57, 62syl12anc 832 . . . . . 6 (𝑓𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64 fveq2 6664 . . . . . . . 8 (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65 sseq1 3991 . . . . . . . . 9 (𝑎 = {𝑓} → (𝑎𝐵 ↔ {𝑓} ⊆ 𝐵))
66 reseq2 5842 . . . . . . . . . . . 12 (𝑎 = {𝑓} → (𝑑𝑎) = (𝑑 ↾ {𝑓}))
6766fveq2d 6668 . . . . . . . . . . 11 (𝑎 = {𝑓} → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
6867mpteq2dv 5154 . . . . . . . . . 10 (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
6968eqeq2d 2832 . . . . . . . . 9 (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
7065, 69anbi12d 630 . . . . . . . 8 (𝑎 = {𝑓} → ((𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7164, 70rexeqbidv 3403 . . . . . . 7 (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7271rspcev 3622 . . . . . 6 (({𝑓} ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7334, 63, 72sylancr 587 . . . . 5 (𝑓𝐵 → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7473adantl 482 . . . 4 ((⊤ ∧ 𝑓𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
75 simplll 771 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∈ Fin)
76 simprll 775 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗 ∈ Fin)
77 unfi 8774 . . . . . . . . . . . . . . . . . 18 (( ∈ Fin ∧ 𝑗 ∈ Fin) → (𝑗) ∈ Fin)
7875, 76, 77syl2anc 584 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ Fin)
79 vex 3498 . . . . . . . . . . . . . . . . . . . . . 22 ∈ V
80 vex 3498 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ V
8179, 80unex 7457 . . . . . . . . . . . . . . . . . . . . 21 (𝑗) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ V)
83 ssun1 4147 . . . . . . . . . . . . . . . . . . . . 21 ⊆ (𝑗)
8483a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ⊆ (𝑗))
85 simpllr 772 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑖 ∈ (mzPoly‘))
86 mzpresrename 39227 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ ⊆ (𝑗) ∧ 𝑖 ∈ (mzPoly‘)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
8782, 84, 85, 86syl3anc 1363 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
88 ssun2 4148 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ⊆ (𝑗)
8988a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗 ⊆ (𝑗))
90 simprlr 776 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91 mzpresrename 39227 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ 𝑗 ⊆ (𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
9282, 89, 90, 91syl3anc 1363 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
93 mzpaddmpt 39218 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
9487, 92, 93syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
95 simplr 765 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝐵)
96 simprr 769 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗𝐵)
9795, 96unssd 4161 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ⊆ 𝐵)
98 ovex 7178 . . . . . . . . . . . . . . . . . . . . 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 39227 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝐵𝑖 ∈ (mzPoly‘)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
103101, 95, 85, 102syl3anc 1363 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
104 mzpf 39213 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑m 𝐵)⟶ℤ)
105 ffn 6508 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵))
106103, 104, 1053syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵))
107 mzpresrename 39227 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝑗𝐵𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
108101, 96, 90, 107syl3anc 1363 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
109 mzpf 39213 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑m 𝐵)⟶ℤ)
110 ffn 6508 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵))
111108, 109, 1103syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵))
112 ofmpteq 7417 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵) ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
11399, 106, 111, 112syl3anc 1363 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
114 elmapi 8418 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 ∈ (ℤ ↑m 𝐵) → 𝑑:𝐵⟶ℤ)
115 fssres 6538 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑑:𝐵⟶ℤ ∧ (𝑗) ⊆ 𝐵) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
116114, 97, 115syl2anr 596 . . . . . . . . . . . . . . . . . . . . . . 23 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
117 zex 11979 . . . . . . . . . . . . . . . . . . . . . . . 24 ℤ ∈ V
118117, 81elmap 8425 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)) ↔ (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
119116, 118sylibr 235 . . . . . . . . . . . . . . . . . . . . . 22 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)))
120 reseq1 5841 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙) = ((𝑑 ↾ (𝑗)) ↾ ))
121120fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑖‘(𝑙)) = (𝑖‘((𝑑 ↾ (𝑗)) ↾ )))
122 reseq1 5841 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙𝑗) = ((𝑑 ↾ (𝑗)) ↾ 𝑗))
123122fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑘‘(𝑙𝑗)) = (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)))
124121, 123oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
125 eqid 2821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))
126 ovex 7178 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
127124, 125, 126fvmpt 6762 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
128119, 127syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
129 resabs1 5877 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑))
13083, 129ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑)
131130fveq2i 6667 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖‘((𝑑 ↾ (𝑗)) ↾ )) = (𝑖‘(𝑑))
132 resabs1 5877 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗))
13388, 132ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗)
134133fveq2i 6667 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑𝑗))
135131, 134oveq12i 7157 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))
136128, 135syl6req 2873 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
137136mpteq2dva 5153 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
138113, 137eqtrd 2856 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
139 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
140139mpteq2dv 5154 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
141140eqeq2d 2832 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
142141anbi2d 628 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
143142rspcev 3622 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
14494, 97, 138, 143syl12anc 832 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
145 mzpmulmpt 39219 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
14687, 92, 145syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
147 ofmpteq 7417 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵) ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
14899, 106, 111, 147syl3anc 1363 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
149121, 123oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
150 eqid 2821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))
151 ovex 7178 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
152149, 150, 151fvmpt 6762 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
153119, 152syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
154131, 134oveq12i 7157 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))
155153, 154syl6req 2873 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
156155mpteq2dva 5153 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
157148, 156eqtrd 2856 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
158 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
159158mpteq2dv 5154 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
160159eqeq2d 2832 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
161160anbi2d 628 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
162161rspcev 3622 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
163146, 97, 157, 162syl12anc 832 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
164 fveq2 6664 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → (mzPoly‘𝑎) = (mzPoly‘(𝑗)))
165 sseq1 3991 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (𝑎𝐵 ↔ (𝑗) ⊆ 𝐵))
166 reseq2 5842 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑗) → (𝑑𝑎) = (𝑑 ↾ (𝑗)))
167166fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑗) → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ (𝑗))))
168167mpteq2dv 5154 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑗) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))
169168eqeq2d 2832 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
170165, 169anbi12d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
171164, 170rexeqbidv 3403 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
172168eqeq2d 2832 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
173165, 172anbi12d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
174164, 173rexeqbidv 3403 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
175171, 174anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑗) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))))
176175rspcev 3622 . . . . . . . . . . . . . . . . 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 832 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
178177adantlrr 717 . . . . . . . . . . . . . . 15 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
179178adantrrr 721 . . . . . . . . . . . . . 14 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
180 simplrr 774 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))
181 simprrr 778 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))
182180, 181oveq12d 7163 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓f + 𝑔) = ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
183182eqeq1d 2823 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
184183anbi2d 628 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
185184rexbidv 3297 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
186180, 181oveq12d 7163 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓f · 𝑔) = ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
187186eqeq1d 2823 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
188187anbi2d 628 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
189188rexbidv 3297 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
190185, 189anbi12d 630 . . . . . . . . . . . . . . 15 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
191190rexbidv 3297 . . . . . . . . . . . . . 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 258 . . . . . . . . . . . . 13 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
193 r19.40 3346 . . . . . . . . . . . . 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 421 . . . . . . . . . . 11 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) → ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
196195rexlimdvv 3293 . . . . . . . . . 10 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
197196ex 413 . . . . . . . . 9 (( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
198197rexlimivv 3292 . . . . . . . 8 (∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
199198imp 407 . . . . . . 7 ((∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))) ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
200199ad2ant2l 742 . . . . . 6 (((𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2012003adant1 1122 . . . . 5 ((⊤ ∧ (𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
202201simpld 495 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
203201simprd 496 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
204 eqeq1 2825 . . . . . 6 (𝑒 = ((ℤ ↑m 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
205204anbi2d 628 . . . . 5 (𝑒 = ((ℤ ↑m 𝐵) × {𝑓}) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2062052rexbidv 3300 . . . 4 (𝑒 = ((ℤ ↑m 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
207 eqeq1 2825 . . . . . 6 (𝑒 = (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
208207anbi2d 628 . . . . 5 (𝑒 = (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2092082rexbidv 3300 . . . 4 (𝑒 = (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
210 eqeq1 2825 . . . . . . 7 (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
211210anbi2d 628 . . . . . 6 (𝑒 = 𝑓 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2122112rexbidv 3300 . . . . 5 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
213 fveq2 6664 . . . . . . . 8 (𝑎 = → (mzPoly‘𝑎) = (mzPoly‘))
214 sseq1 3991 . . . . . . . . 9 (𝑎 = → (𝑎𝐵𝐵))
215 reseq2 5842 . . . . . . . . . . . 12 (𝑎 = → (𝑑𝑎) = (𝑑))
216215fveq2d 6668 . . . . . . . . . . 11 (𝑎 = → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑)))
217216mpteq2dv 5154 . . . . . . . . . 10 (𝑎 = → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))))
218217eqeq2d 2832 . . . . . . . . 9 (𝑎 = → (𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑)))))
219214, 218anbi12d 630 . . . . . . . 8 (𝑎 = → ((𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))))))
220213, 219rexeqbidv 3403 . . . . . . 7 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))))))
221 fveq1 6663 . . . . . . . . . . 11 (𝑏 = 𝑖 → (𝑏‘(𝑑)) = (𝑖‘(𝑑)))
222221mpteq2dv 5154 . . . . . . . . . 10 (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))
223222eqeq2d 2832 . . . . . . . . 9 (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))))
224223anbi2d 628 . . . . . . . 8 (𝑏 = 𝑖 → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))))
225224cbvrexvw 3451 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))))
226220, 225syl6bb 288 . . . . . 6 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))))
227226cbvrexvw 3451 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))))
228212, 227syl6bb 288 . . . 4 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))))
229 eqeq1 2825 . . . . . . 7 (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
230229anbi2d 628 . . . . . 6 (𝑒 = 𝑔 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2312302rexbidv 3300 . . . . 5 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
232 fveq2 6664 . . . . . . . 8 (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233 sseq1 3991 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑎𝐵𝑗𝐵))
234 reseq2 5842 . . . . . . . . . . . 12 (𝑎 = 𝑗 → (𝑑𝑎) = (𝑑𝑗))
235234fveq2d 6668 . . . . . . . . . . 11 (𝑎 = 𝑗 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑𝑗)))
236235mpteq2dv 5154 . . . . . . . . . 10 (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))))
237236eqeq2d 2832 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗)))))
238233, 237anbi12d 630 . . . . . . . 8 (𝑎 = 𝑗 → ((𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
239232, 238rexeqbidv 3403 . . . . . . 7 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
240 fveq1 6663 . . . . . . . . . . 11 (𝑏 = 𝑘 → (𝑏‘(𝑑𝑗)) = (𝑘‘(𝑑𝑗)))
241240mpteq2dv 5154 . . . . . . . . . 10 (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))
242241eqeq2d 2832 . . . . . . . . 9 (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
243242anbi2d 628 . . . . . . . 8 (𝑏 = 𝑘 → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
244243cbvrexvw 3451 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
245239, 244syl6bb 288 . . . . . 6 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
246245cbvrexvw 3451 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
247231, 246syl6bb 288 . . . 4 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
248 eqeq1 2825 . . . . . 6 (𝑒 = (𝑓f + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
249248anbi2d 628 . . . . 5 (𝑒 = (𝑓f + 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2502492rexbidv 3300 . . . 4 (𝑒 = (𝑓f + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
251 eqeq1 2825 . . . . . 6 (𝑒 = (𝑓f · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
252251anbi2d 628 . . . . 5 (𝑒 = (𝑓f · 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2532522rexbidv 3300 . . . 4 (𝑒 = (𝑓f · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
254 eqeq1 2825 . . . . . 6 (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
255254anbi2d 628 . . . . 5 (𝑒 = 𝐴 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2562552rexbidv 3300 . . . 4 (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
25733, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256mzpindd 39223 . . 3 ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
2581, 257mpan 686 . 2 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
259 reseq1 5841 . . . . . . 7 (𝑑 = 𝑐 → (𝑑𝑎) = (𝑐𝑎))
260259fveq2d 6668 . . . . . 6 (𝑑 = 𝑐 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑐𝑎)))
261260cbvmptv 5161 . . . . 5 (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))
262261eqeq2i 2834 . . . 4 (𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎))))
263262anbi2i 622 . . 3 ((𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
2642632rexbii 3248 . 2 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
265258, 264sylib 219 1 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079   = wceq 1528  wtru 1529  wcel 2105  wrex 3139  Vcvv 3495  cun 3933  wss 3935  c0 4290  {csn 4559  cmpt 5138   × cxp 5547  cres 5551   Fn wfn 6344  wf 6345  cfv 6349  (class class class)co 7145  f cof 7396  m cmap 8396  Fincfn 8498   + caddc 10529   · cmul 10531  cz 11970  mzPolycmzp 39199
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-map 8398  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-n0 11887  df-z 11971  df-mzpcl 39200  df-mzp 39201
This theorem is referenced by:  mzpcompact2  39229
  Copyright terms: Public domain W3C validator