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 41422
Description: Lemma for mzpcompact2 41423. (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 1546 . . 3
2 0fin 9167 . . . . . 6 ∅ ∈ Fin
3 0ex 5306 . . . . . . . 8 ∅ ∈ V
4 mzpconst 41406 . . . . . . . 8 ((∅ ∈ V ∧ 𝑓 ∈ ℤ) → ((ℤ ↑m ∅) × {𝑓}) ∈ (mzPoly‘∅))
53, 4mpan 689 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑m ∅) × {𝑓}) ∈ (mzPoly‘∅))
6 0ss 4395 . . . . . . . 8 ∅ ⊆ 𝐵
76a1i 11 . . . . . . 7 (𝑓 ∈ ℤ → ∅ ⊆ 𝐵)
8 fconstmpt 5736 . . . . . . . 8 ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ 𝑓)
9 simpr 486 . . . . . . . . . . 11 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → 𝑑 ∈ (ℤ ↑m 𝐵))
10 elmapssres 8857 . . . . . . . . . . 11 ((𝑑 ∈ (ℤ ↑m 𝐵) ∧ ∅ ⊆ 𝐵) → (𝑑 ↾ ∅) ∈ (ℤ ↑m ∅))
119, 6, 10sylancl 587 . . . . . . . . . 10 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ ∅) ∈ (ℤ ↑m ∅))
12 vex 3479 . . . . . . . . . . 11 𝑓 ∈ V
1312fvconst2 7200 . . . . . . . . . 10 ((𝑑 ↾ ∅) ∈ (ℤ ↑m ∅) → (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1411, 13syl 17 . . . . . . . . 9 ((𝑓 ∈ ℤ ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)) = 𝑓)
1514mpteq2dva 5247 . . . . . . . 8 (𝑓 ∈ ℤ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ 𝑓))
168, 15eqtr4id 2792 . . . . . . 7 (𝑓 ∈ ℤ → ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
17 fveq1 6887 . . . . . . . . . . 11 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → (𝑏‘(𝑑 ↾ ∅)) = (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)))
1817mpteq2dv 5249 . . . . . . . . . 10 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))
1918eqeq2d 2744 . . . . . . . . 9 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → (((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))) ↔ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅)))))
2019anbi2d 630 . . . . . . . 8 (𝑏 = ((ℤ ↑m ∅) × {𝑓}) → ((∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))))
2120rspcev 3612 . . . . . . 7 ((((ℤ ↑m ∅) × {𝑓}) ∈ (mzPoly‘∅) ∧ (∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (((ℤ ↑m ∅) × {𝑓})‘(𝑑 ↾ ∅))))) → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
225, 7, 16, 21syl12anc 836 . . . . . 6 (𝑓 ∈ ℤ → ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
23 fveq2 6888 . . . . . . . 8 (𝑎 = ∅ → (mzPoly‘𝑎) = (mzPoly‘∅))
24 sseq1 4006 . . . . . . . . 9 (𝑎 = ∅ → (𝑎𝐵 ↔ ∅ ⊆ 𝐵))
25 reseq2 5974 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑑𝑎) = (𝑑 ↾ ∅))
2625fveq2d 6892 . . . . . . . . . . 11 (𝑎 = ∅ → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ ∅)))
2726mpteq2dv 5249 . . . . . . . . . 10 (𝑎 = ∅ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))
2827eqeq2d 2744 . . . . . . . . 9 (𝑎 = ∅ → (((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅)))))
2924, 28anbi12d 632 . . . . . . . 8 (𝑎 = ∅ → ((𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3023, 29rexeqbidv 3344 . . . . . . 7 (𝑎 = ∅ → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))))
3130rspcev 3612 . . . . . 6 ((∅ ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘∅)(∅ ⊆ 𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ ∅))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
322, 22, 31sylancr 588 . . . . 5 (𝑓 ∈ ℤ → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
3332adantl 483 . . . 4 ((⊤ ∧ 𝑓 ∈ ℤ) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
34 snfi 9040 . . . . . 6 {𝑓} ∈ Fin
35 vsnex 5428 . . . . . . . . 9 {𝑓} ∈ V
36 vsnid 4664 . . . . . . . . 9 𝑓 ∈ {𝑓}
37 mzpproj 41408 . . . . . . . . 9 (({𝑓} ∈ V ∧ 𝑓 ∈ {𝑓}) → (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
3835, 36, 37mp2an 691 . . . . . . . 8 (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓})
3938a1i 11 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}))
40 snssi 4810 . . . . . . 7 (𝑓𝐵 → {𝑓} ⊆ 𝐵)
41 fveq1 6887 . . . . . . . . 9 (𝑔 = 𝑑 → (𝑔𝑓) = (𝑑𝑓))
4241cbvmptv 5260 . . . . . . . 8 (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑑𝑓))
43 simpr 486 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → 𝑑 ∈ (ℤ ↑m 𝐵))
44 simpl 484 . . . . . . . . . . . . 13 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → 𝑓𝐵)
4544snssd 4811 . . . . . . . . . . . 12 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → {𝑓} ⊆ 𝐵)
46 elmapssres 8857 . . . . . . . . . . . 12 ((𝑑 ∈ (ℤ ↑m 𝐵) ∧ {𝑓} ⊆ 𝐵) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑m {𝑓}))
4743, 45, 46syl2anc 585 . . . . . . . . . . 11 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ {𝑓}) ∈ (ℤ ↑m {𝑓}))
48 fveq1 6887 . . . . . . . . . . . 12 (𝑔 = (𝑑 ↾ {𝑓}) → (𝑔𝑓) = ((𝑑 ↾ {𝑓})‘𝑓))
49 eqid 2733 . . . . . . . . . . . 12 (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))
50 fvex 6901 . . . . . . . . . . . 12 ((𝑑 ↾ {𝑓})‘𝑓) ∈ V
5148, 49, 50fvmpt 6994 . . . . . . . . . . 11 ((𝑑 ↾ {𝑓}) ∈ (ℤ ↑m {𝑓}) → ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
5247, 51syl 17 . . . . . . . . . 10 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})) = ((𝑑 ↾ {𝑓})‘𝑓))
53 fvres 6907 . . . . . . . . . . 11 (𝑓 ∈ {𝑓} → ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓))
5436, 53ax-mp 5 . . . . . . . . . 10 ((𝑑 ↾ {𝑓})‘𝑓) = (𝑑𝑓)
5552, 54eqtr2di 2790 . . . . . . . . 9 ((𝑓𝐵𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑𝑓) = ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5655mpteq2dva 5247 . . . . . . . 8 (𝑓𝐵 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑑𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
5742, 56eqtrid 2785 . . . . . . 7 (𝑓𝐵 → (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
58 fveq1 6887 . . . . . . . . . . 11 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → (𝑏‘(𝑑 ↾ {𝑓})) = ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))
5958mpteq2dv 5249 . . . . . . . . . 10 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))
6059eqeq2d 2744 . . . . . . . . 9 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → ((𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))) ↔ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓})))))
6160anbi2d 630 . . . . . . . 8 (𝑏 = (𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) → (({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))))
6261rspcev 3612 . . . . . . 7 (((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓)) ∈ (mzPoly‘{𝑓}) ∧ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑔 ∈ (ℤ ↑m {𝑓}) ↦ (𝑔𝑓))‘(𝑑 ↾ {𝑓}))))) → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
6339, 40, 57, 62syl12anc 836 . . . . . 6 (𝑓𝐵 → ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
64 fveq2 6888 . . . . . . . 8 (𝑎 = {𝑓} → (mzPoly‘𝑎) = (mzPoly‘{𝑓}))
65 sseq1 4006 . . . . . . . . 9 (𝑎 = {𝑓} → (𝑎𝐵 ↔ {𝑓} ⊆ 𝐵))
66 reseq2 5974 . . . . . . . . . . . 12 (𝑎 = {𝑓} → (𝑑𝑎) = (𝑑 ↾ {𝑓}))
6766fveq2d 6892 . . . . . . . . . . 11 (𝑎 = {𝑓} → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ {𝑓})))
6867mpteq2dv 5249 . . . . . . . . . 10 (𝑎 = {𝑓} → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))
6968eqeq2d 2744 . . . . . . . . 9 (𝑎 = {𝑓} → ((𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓})))))
7065, 69anbi12d 632 . . . . . . . 8 (𝑎 = {𝑓} → ((𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7164, 70rexeqbidv 3344 . . . . . . 7 (𝑎 = {𝑓} → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))))
7271rspcev 3612 . . . . . 6 (({𝑓} ∈ Fin ∧ ∃𝑏 ∈ (mzPoly‘{𝑓})({𝑓} ⊆ 𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ {𝑓}))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7334, 63, 72sylancr 588 . . . . 5 (𝑓𝐵 → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
7473adantl 483 . . . 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 9168 . . . . . . . . . . . . . . . . . 18 (( ∈ Fin ∧ 𝑗 ∈ Fin) → (𝑗) ∈ Fin)
7875, 76, 77syl2anc 585 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ Fin)
79 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 ∈ V
80 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ V
8179, 80unex 7728 . . . . . . . . . . . . . . . . . . . . 21 (𝑗) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ∈ V)
83 ssun1 4171 . . . . . . . . . . . . . . . . . . . . 21 ⊆ (𝑗)
8483a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ⊆ (𝑗))
85 simpllr 775 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑖 ∈ (mzPoly‘))
86 mzpresrename 41421 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ ⊆ (𝑗) ∧ 𝑖 ∈ (mzPoly‘)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
8782, 84, 85, 86syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)))
88 ssun2 4172 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ⊆ (𝑗)
8988a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑗 ⊆ (𝑗))
90 simprlr 779 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → 𝑘 ∈ (mzPoly‘𝑗))
91 mzpresrename 41421 . . . . . . . . . . . . . . . . . . . 20 (((𝑗) ∈ V ∧ 𝑗 ⊆ (𝑗) ∧ 𝑘 ∈ (mzPoly‘𝑗)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
9282, 89, 90, 91syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗)))
93 mzpaddmpt 41412 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
9487, 92, 93syl2anc 585 . . . . . . . . . . . . . . . . . 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 4185 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑗) ⊆ 𝐵)
98 ovex 7437 . . . . . . . . . . . . . . . . . . . . 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 41421 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝐵𝑖 ∈ (mzPoly‘)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
103101, 95, 85, 102syl3anc 1372 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵))
104 mzpf 41407 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑m 𝐵)⟶ℤ)
105 ffn 6714 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))):(ℤ ↑m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵))
106103, 104, 1053syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵))
107 mzpresrename 41421 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ V ∧ 𝑗𝐵𝑘 ∈ (mzPoly‘𝑗)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
108101, 96, 90, 107syl3anc 1372 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵))
109 mzpf 41407 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) ∈ (mzPoly‘𝐵) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑m 𝐵)⟶ℤ)
110 ffn 6714 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))):(ℤ ↑m 𝐵)⟶ℤ → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵))
111108, 109, 1103syl 18 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵))
112 ofmpteq 7687 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵) ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
11399, 106, 111, 112syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))))
114 elmapi 8839 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 ∈ (ℤ ↑m 𝐵) → 𝑑:𝐵⟶ℤ)
115 fssres 6754 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑑:𝐵⟶ℤ ∧ (𝑗) ⊆ 𝐵) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
116114, 97, 115syl2anr 598 . . . . . . . . . . . . . . . . . . . . . . 23 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
117 zex 12563 . . . . . . . . . . . . . . . . . . . . . . . 24 ℤ ∈ V
118117, 81elmap 8861 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)) ↔ (𝑑 ↾ (𝑗)):(𝑗)⟶ℤ)
119116, 118sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → (𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)))
120 reseq1 5973 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙) = ((𝑑 ↾ (𝑗)) ↾ ))
121120fveq2d 6892 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑖‘(𝑙)) = (𝑖‘((𝑑 ↾ (𝑗)) ↾ )))
122 reseq1 5973 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑙𝑗) = ((𝑑 ↾ (𝑗)) ↾ 𝑗))
123122fveq2d 6892 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = (𝑑 ↾ (𝑗)) → (𝑘‘(𝑙𝑗)) = (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)))
124121, 123oveq12d 7422 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
125 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))
126 ovex 7437 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
127124, 125, 126fvmpt 6994 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
128119, 127syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
129 resabs1 6009 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑))
13083, 129ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ ) = (𝑑)
131130fveq2i 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖‘((𝑑 ↾ (𝑗)) ↾ )) = (𝑖‘(𝑑))
132 resabs1 6009 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ⊆ (𝑗) → ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗))
13388, 132ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑑 ↾ (𝑗)) ↾ 𝑗) = (𝑑𝑗)
134133fveq2i 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗)) = (𝑘‘(𝑑𝑗))
135131, 134oveq12i 7416 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) + (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))
136128, 135eqtr2di 2790 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
137136mpteq2dva 5247 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) + (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
138113, 137eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
139 fveq1 6887 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
140139mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
141140eqeq2d 2744 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
142141anbi2d 630 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
143142rspcev 3612 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) + (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
14494, 97, 138, 143syl12anc 836 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
145 mzpmulmpt 41413 . . . . . . . . . . . . . . . . . . 19 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑖‘(𝑙))) ∈ (mzPoly‘(𝑗)) ∧ (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ (𝑘‘(𝑙𝑗))) ∈ (mzPoly‘(𝑗))) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
14687, 92, 145syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)))
147 ofmpteq 7687 . . . . . . . . . . . . . . . . . . . 20 (((ℤ ↑m 𝐵) ∈ V ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) Fn (ℤ ↑m 𝐵) ∧ (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))) Fn (ℤ ↑m 𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
14899, 106, 111, 147syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))))
149121, 123oveq12d 7422 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = (𝑑 ↾ (𝑗)) → ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
150 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))
151 ovex 7437 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) ∈ V
152149, 150, 151fvmpt 6994 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ↾ (𝑗)) ∈ (ℤ ↑m (𝑗)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
153119, 152syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))) = ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))))
154131, 134oveq12i 7416 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖‘((𝑑 ↾ (𝑗)) ↾ )) · (𝑘‘((𝑑 ↾ (𝑗)) ↾ 𝑗))) = ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))
155153, 154eqtr2di 2790 . . . . . . . . . . . . . . . . . . . 20 ((((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) ∧ 𝑑 ∈ (ℤ ↑m 𝐵)) → ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
156155mpteq2dva 5247 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑖‘(𝑑)) · (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
157148, 156eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
158 fveq1 6887 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑏‘(𝑑 ↾ (𝑗))) = ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))
159158mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))
160159eqeq2d 2744 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗))))))
161160anbi2d 630 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) → (((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))))
162161rspcev 3612 . . . . . . . . . . . . . . . . . 18 (((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗)))) ∈ (mzPoly‘(𝑗)) ∧ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ ((𝑙 ∈ (ℤ ↑m (𝑗)) ↦ ((𝑖‘(𝑙)) · (𝑘‘(𝑙𝑗))))‘(𝑑 ↾ (𝑗)))))) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
163146, 97, 157, 162syl12anc 836 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ 𝐵) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ 𝑗𝐵)) → ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
164 fveq2 6888 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → (mzPoly‘𝑎) = (mzPoly‘(𝑗)))
165 sseq1 4006 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (𝑎𝐵 ↔ (𝑗) ⊆ 𝐵))
166 reseq2 5974 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑗) → (𝑑𝑎) = (𝑑 ↾ (𝑗)))
167166fveq2d 6892 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑗) → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑 ↾ (𝑗))))
168167mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑗) → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))
169168eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
170165, 169anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
171164, 170rexeqbidv 3344 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
172168eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑗) → (((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))
173165, 172anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑗) → ((𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
174164, 173rexeqbidv 3344 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑗) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗)))))))
175171, 174anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑗) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))) ∧ ∃𝑏 ∈ (mzPoly‘(𝑗))((𝑗) ⊆ 𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑 ↾ (𝑗))))))))
176175rspcev 3612 . . . . . . . . . . . . . . . . 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 836 . . . . . . . . . . . . . . . 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 7422 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓f + 𝑔) = ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
183182eqeq1d 2735 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
184183anbi2d 630 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
185184rexbidv 3179 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
186180, 181oveq12d 7422 . . . . . . . . . . . . . . . . . . 19 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (𝑓f · 𝑔) = ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
187186eqeq1d 2735 . . . . . . . . . . . . . . . . . 18 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
188187anbi2d 630 . . . . . . . . . . . . . . . . 17 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
189188rexbidv 3179 . . . . . . . . . . . . . . . 16 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
190185, 189anbi12d 632 . . . . . . . . . . . . . . 15 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ((∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))) ↔ (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f + (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))) ∘f · (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
191190rexbidv 3179 . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . 13 (((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) ∧ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
193 r19.40 3120 . . . . . . . . . . . . 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 422 . . . . . . . . . . 11 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) → ((𝑗 ∈ Fin ∧ 𝑘 ∈ (mzPoly‘𝑗)) → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
196195rexlimdvv 3211 . . . . . . . . . 10 ((( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) ∧ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
197196ex 414 . . . . . . . . 9 (( ∈ Fin ∧ 𝑖 ∈ (mzPoly‘)) → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))))
198197rexlimivv 3200 . . . . . . . 8 (∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))) → (∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))))
199198imp 408 . . . . . . 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 1131 . . . . 5 ((⊤ ∧ (𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ∧ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
202201simpld 496 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
203201simprd 497 . . . 4 ((⊤ ∧ (𝑓:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))) ∧ (𝑔:(ℤ ↑m 𝐵)⟶ℤ ∧ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
204 eqeq1 2737 . . . . . 6 (𝑒 = ((ℤ ↑m 𝐵) × {𝑓}) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
205204anbi2d 630 . . . . 5 (𝑒 = ((ℤ ↑m 𝐵) × {𝑓}) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2062052rexbidv 3220 . . . 4 (𝑒 = ((ℤ ↑m 𝐵) × {𝑓}) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ ((ℤ ↑m 𝐵) × {𝑓}) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
207 eqeq1 2737 . . . . . 6 (𝑒 = (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
208207anbi2d 630 . . . . 5 (𝑒 = (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2092082rexbidv 3220 . . . 4 (𝑒 = (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑔 ∈ (ℤ ↑m 𝐵) ↦ (𝑔𝑓)) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
210 eqeq1 2737 . . . . . . 7 (𝑒 = 𝑓 → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
211210anbi2d 630 . . . . . 6 (𝑒 = 𝑓 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2122112rexbidv 3220 . . . . 5 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
213 fveq2 6888 . . . . . . . 8 (𝑎 = → (mzPoly‘𝑎) = (mzPoly‘))
214 sseq1 4006 . . . . . . . . 9 (𝑎 = → (𝑎𝐵𝐵))
215 reseq2 5974 . . . . . . . . . . . 12 (𝑎 = → (𝑑𝑎) = (𝑑))
216215fveq2d 6892 . . . . . . . . . . 11 (𝑎 = → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑)))
217216mpteq2dv 5249 . . . . . . . . . 10 (𝑎 = → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))))
218217eqeq2d 2744 . . . . . . . . 9 (𝑎 = → (𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑)))))
219214, 218anbi12d 632 . . . . . . . 8 (𝑎 = → ((𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))))))
220213, 219rexeqbidv 3344 . . . . . . 7 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))))))
221 fveq1 6887 . . . . . . . . . . 11 (𝑏 = 𝑖 → (𝑏‘(𝑑)) = (𝑖‘(𝑑)))
222221mpteq2dv 5249 . . . . . . . . . 10 (𝑏 = 𝑖 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))
223222eqeq2d 2744 . . . . . . . . 9 (𝑏 = 𝑖 → (𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑))) ↔ 𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))))
224223anbi2d 630 . . . . . . . 8 (𝑏 = 𝑖 → ((𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑)))) ↔ (𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))))
225224cbvrexvw 3236 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))))
226220, 225bitrdi 287 . . . . . 6 (𝑎 = → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))))
227226cbvrexvw 3236 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑)))))
228212, 227bitrdi 287 . . . 4 (𝑒 = 𝑓 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃ ∈ Fin ∃𝑖 ∈ (mzPoly‘)(𝐵𝑓 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑖‘(𝑑))))))
229 eqeq1 2737 . . . . . . 7 (𝑒 = 𝑔 → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
230229anbi2d 630 . . . . . 6 (𝑒 = 𝑔 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2312302rexbidv 3220 . . . . 5 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
232 fveq2 6888 . . . . . . . 8 (𝑎 = 𝑗 → (mzPoly‘𝑎) = (mzPoly‘𝑗))
233 sseq1 4006 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑎𝐵𝑗𝐵))
234 reseq2 5974 . . . . . . . . . . . 12 (𝑎 = 𝑗 → (𝑑𝑎) = (𝑑𝑗))
235234fveq2d 6892 . . . . . . . . . . 11 (𝑎 = 𝑗 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑑𝑗)))
236235mpteq2dv 5249 . . . . . . . . . 10 (𝑎 = 𝑗 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))))
237236eqeq2d 2744 . . . . . . . . 9 (𝑎 = 𝑗 → (𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗)))))
238233, 237anbi12d 632 . . . . . . . 8 (𝑎 = 𝑗 → ((𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
239232, 238rexeqbidv 3344 . . . . . . 7 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))))))
240 fveq1 6887 . . . . . . . . . . 11 (𝑏 = 𝑘 → (𝑏‘(𝑑𝑗)) = (𝑘‘(𝑑𝑗)))
241240mpteq2dv 5249 . . . . . . . . . 10 (𝑏 = 𝑘 → (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))
242241eqeq2d 2744 . . . . . . . . 9 (𝑏 = 𝑘 → (𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗))) ↔ 𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
243242anbi2d 630 . . . . . . . 8 (𝑏 = 𝑘 → ((𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ (𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
244243cbvrexvw 3236 . . . . . . 7 (∃𝑏 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑗)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
245239, 244bitrdi 287 . . . . . 6 (𝑎 = 𝑗 → (∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
246245cbvrexvw 3236 . . . . 5 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗)))))
247231, 246bitrdi 287 . . . 4 (𝑒 = 𝑔 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑗 ∈ Fin ∃𝑘 ∈ (mzPoly‘𝑗)(𝑗𝐵𝑔 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑘‘(𝑑𝑗))))))
248 eqeq1 2737 . . . . . 6 (𝑒 = (𝑓f + 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
249248anbi2d 630 . . . . 5 (𝑒 = (𝑓f + 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2502492rexbidv 3220 . . . 4 (𝑒 = (𝑓f + 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f + 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
251 eqeq1 2737 . . . . . 6 (𝑒 = (𝑓f · 𝑔) → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
252251anbi2d 630 . . . . 5 (𝑒 = (𝑓f · 𝑔) → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2532522rexbidv 3220 . . . 4 (𝑒 = (𝑓f · 𝑔) → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵 ∧ (𝑓f · 𝑔) = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
254 eqeq1 2737 . . . . . 6 (𝑒 = 𝐴 → (𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
255254anbi2d 630 . . . . 5 (𝑒 = 𝐴 → ((𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
2562552rexbidv 3220 . . . 4 (𝑒 = 𝐴 → (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝑒 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))))))
25733, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256mzpindd 41417 . . 3 ((⊤ ∧ 𝐴 ∈ (mzPoly‘𝐵)) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
2581, 257mpan 689 . 2 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))))
259 reseq1 5973 . . . . . . 7 (𝑑 = 𝑐 → (𝑑𝑎) = (𝑐𝑎))
260259fveq2d 6892 . . . . . 6 (𝑑 = 𝑐 → (𝑏‘(𝑑𝑎)) = (𝑏‘(𝑐𝑎)))
261260cbvmptv 5260 . . . . 5 (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))
262261eqeq2i 2746 . . . 4 (𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎))) ↔ 𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎))))
263262anbi2i 624 . . 3 ((𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ (𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
2642632rexbii 3130 . 2 (∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑑 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑑𝑎)))) ↔ ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
265258, 264sylib 217 1 (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎𝐵𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐𝑎)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088   = wceq 1542  wtru 1543  wcel 2107  wrex 3071  Vcvv 3475  cun 3945  wss 3947  c0 4321  {csn 4627  cmpt 5230   × cxp 5673  cres 5677   Fn wfn 6535  wf 6536  cfv 6540  (class class class)co 7404  f cof 7663  m cmap 8816  Fincfn 8935   + caddc 11109   · cmul 11111  cz 12554  mzPolycmzp 41393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-om 7851  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555  df-mzpcl 41394  df-mzp 41395
This theorem is referenced by:  mzpcompact2  41423
  Copyright terms: Public domain W3C validator