Metamath Proof Explorer

Theorem eldioph2

Description: Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 . (Contributed by Stefan O'Rear, 8-Oct-2014) (Revised by Stefan O'Rear, 5-Jun-2015)

Ref Expression
Assertion eldioph2 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 mzpcompact2 ⊢ ( 𝑃 ∈ ( mzPoly ‘ 𝑆 ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝑆 ∧ 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ) )
2 1 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) → ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝑆 ∧ 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ) )
3 fveq1 ⊢ ( 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) → ( 𝑃 ‘ 𝑢 ) = ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) )
4 3 eqeq1d ⊢ ( 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) → ( ( 𝑃 ‘ 𝑢 ) = 0 ↔ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) )
5 4 anbi2d ⊢ ( 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) → ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) ↔ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) ) )
6 5 rexbidv ⊢ ( 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) → ( ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) ↔ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) ) )
7 6 abbidv ⊢ ( 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } )
8 7 ad2antll ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ ( 𝑎 ⊆ 𝑆 ∧ 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } )
9 simplll ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → 𝑁 ∈ ℕ0 )
10 simplrl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → 𝑎 ∈ Fin )
11 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
12 unfi ⊢ ( ( 𝑎 ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∈ Fin )
13 10 11 12 sylancl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∈ Fin )
14 ssun2 ⊢ ( 1 ... 𝑁 ) ⊆ ( 𝑎 ∪ ( 1 ... 𝑁 ) )
15 14 a1i ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → ( 1 ... 𝑁 ) ⊆ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) )
16 eldioph2lem1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ) → ∃ 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑑 ∈ V ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
17 9 13 15 16 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → ∃ 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑑 ∈ V ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
18 f1ococnv2 ⊢ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) → ( 𝑑 ∘ ◡ 𝑑 ) = ( I ↾ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ) )
19 18 ad2antrl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( 𝑑 ∘ ◡ 𝑑 ) = ( I ↾ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ) )
20 19 reseq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( ( 𝑑 ∘ ◡ 𝑑 ) ↾ 𝑎 ) = ( ( I ↾ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ) ↾ 𝑎 ) )
21 ssun1 ⊢ 𝑎 ⊆ ( 𝑎 ∪ ( 1 ... 𝑁 ) )
22 resabs1 ⊢ ( 𝑎 ⊆ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) → ( ( I ↾ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ) ↾ 𝑎 ) = ( I ↾ 𝑎 ) )
23 21 22 ax-mp ⊢ ( ( I ↾ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ) ↾ 𝑎 ) = ( I ↾ 𝑎 )
24 20 23 eqtr2di ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( I ↾ 𝑎 ) = ( ( 𝑑 ∘ ◡ 𝑑 ) ↾ 𝑎 ) )
25 resco ⊢ ( ( 𝑑 ∘ ◡ 𝑑 ) ↾ 𝑎 ) = ( 𝑑 ∘ ( ◡ 𝑑 ↾ 𝑎 ) )
26 24 25 eqtrdi ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( I ↾ 𝑎 ) = ( 𝑑 ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) )
27 26 adantr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → ( I ↾ 𝑎 ) = ( 𝑑 ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) )
28 27 coeq2d ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → ( 𝑒 ∘ ( I ↾ 𝑎 ) ) = ( 𝑒 ∘ ( 𝑑 ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) )
29 coires1 ⊢ ( 𝑒 ∘ ( I ↾ 𝑎 ) ) = ( 𝑒 ↾ 𝑎 )
30 coass ⊢ ( ( 𝑒 ∘ 𝑑 ) ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) = ( 𝑒 ∘ ( 𝑑 ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) )
31 30 eqcomi ⊢ ( 𝑒 ∘ ( 𝑑 ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) = ( ( 𝑒 ∘ 𝑑 ) ∘ ( ◡ 𝑑 ↾ 𝑎 ) )
32 28 29 31 3eqtr3g ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → ( 𝑒 ↾ 𝑎 ) = ( ( 𝑒 ∘ 𝑑 ) ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) )
33 32 fveq2d ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) = ( 𝑏 ‘ ( ( 𝑒 ∘ 𝑑 ) ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) )
34 ovexd ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → ( 1 ... 𝑐 ) ∈ V )
35 simpr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → 𝑒 ∈ ( ℤ ↑m 𝑆 ) )
36 f1of1 ⊢ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) → 𝑑 : ( 1 ... 𝑐 ) –1-1→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) )
37 36 ad2antrl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑑 : ( 1 ... 𝑐 ) –1-1→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) )
38 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → 𝑎 ⊆ 𝑆 )
39 simprr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) → ( 1 ... 𝑁 ) ⊆ 𝑆 )
40 39 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → ( 1 ... 𝑁 ) ⊆ 𝑆 )
41 38 40 unssd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ⊆ 𝑆 )
42 41 ad2antrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ⊆ 𝑆 )
43 f1ss ⊢ ( ( 𝑑 : ( 1 ... 𝑐 ) –1-1→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ⊆ 𝑆 ) → 𝑑 : ( 1 ... 𝑐 ) –1-1→ 𝑆 )
44 37 42 43 syl2anc ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑑 : ( 1 ... 𝑐 ) –1-1→ 𝑆 )
45 f1f ⊢ ( 𝑑 : ( 1 ... 𝑐 ) –1-1→ 𝑆 → 𝑑 : ( 1 ... 𝑐 ) ⟶ 𝑆 )
46 44 45 syl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑑 : ( 1 ... 𝑐 ) ⟶ 𝑆 )
47 46 adantr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → 𝑑 : ( 1 ... 𝑐 ) ⟶ 𝑆 )
48 mapco2g ⊢ ( ( ( 1 ... 𝑐 ) ∈ V ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ∧ 𝑑 : ( 1 ... 𝑐 ) ⟶ 𝑆 ) → ( 𝑒 ∘ 𝑑 ) ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) )
49 34 35 47 48 syl3anc ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → ( 𝑒 ∘ 𝑑 ) ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) )
50 coeq1 ⊢ ( ℎ = ( 𝑒 ∘ 𝑑 ) → ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) = ( ( 𝑒 ∘ 𝑑 ) ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) )
51 50 fveq2d ⊢ ( ℎ = ( 𝑒 ∘ 𝑑 ) → ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) = ( 𝑏 ‘ ( ( 𝑒 ∘ 𝑑 ) ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) )
52 eqid ⊢ ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) = ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) )
53 fvex ⊢ ( 𝑏 ‘ ( ( 𝑒 ∘ 𝑑 ) ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ∈ V
54 51 52 53 fvmpt ⊢ ( ( 𝑒 ∘ 𝑑 ) ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) → ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) = ( 𝑏 ‘ ( ( 𝑒 ∘ 𝑑 ) ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) )
55 49 54 syl ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) = ( 𝑏 ‘ ( ( 𝑒 ∘ 𝑑 ) ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) )
56 33 55 eqtr4d ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑒 ∈ ( ℤ ↑m 𝑆 ) ) → ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) = ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) )
57 56 mpteq2dva ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) ) )
58 57 fveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) ) ‘ 𝑢 ) )
59 58 eqeq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ↔ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) ) ‘ 𝑢 ) = 0 ) )
60 59 anbi2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) ↔ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) ) ‘ 𝑢 ) = 0 ) ) )
61 60 rexbidv ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) ↔ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) ) ‘ 𝑢 ) = 0 ) ) )
62 61 abbidv ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) ) ‘ 𝑢 ) = 0 ) } )
63 simplrl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) → 𝑆 ∈ V )
64 63 ad3antrrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑆 ∈ V )
65 simprr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) )
66 diophrw ⊢ ( ( 𝑆 ∈ V ∧ 𝑑 : ( 1 ... 𝑐 ) –1-1→ 𝑆 ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) ) ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑔 ∈ ( ℕ0 ↑m ( 1 ... 𝑐 ) ) ( 𝑡 = ( 𝑔 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ 𝑔 ) = 0 ) } )
67 64 44 65 66 syl3anc ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ ( 𝑒 ∘ 𝑑 ) ) ) ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑔 ∈ ( ℕ0 ↑m ( 1 ... 𝑐 ) ) ( 𝑡 = ( 𝑔 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ 𝑔 ) = 0 ) } )
68 62 67 eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑔 ∈ ( ℕ0 ↑m ( 1 ... 𝑐 ) ) ( 𝑡 = ( 𝑔 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ 𝑔 ) = 0 ) } )
69 simp-5l ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑁 ∈ ℕ0 )
70 simplrl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) )
71 ovexd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( 1 ... 𝑐 ) ∈ V )
72 simplrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → 𝑏 ∈ ( mzPoly ‘ 𝑎 ) )
73 72 ad2antrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑏 ∈ ( mzPoly ‘ 𝑎 ) )
74 f1ocnv ⊢ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) → ◡ 𝑑 : ( 𝑎 ∪ ( 1 ... 𝑁 ) ) –1-1-onto→ ( 1 ... 𝑐 ) )
75 f1of ⊢ ( ◡ 𝑑 : ( 𝑎 ∪ ( 1 ... 𝑁 ) ) –1-1-onto→ ( 1 ... 𝑐 ) → ◡ 𝑑 : ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ⟶ ( 1 ... 𝑐 ) )
76 74 75 syl ⊢ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) → ◡ 𝑑 : ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ⟶ ( 1 ... 𝑐 ) )
77 fssres ⊢ ( ( ◡ 𝑑 : ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ⟶ ( 1 ... 𝑐 ) ∧ 𝑎 ⊆ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ) → ( ◡ 𝑑 ↾ 𝑎 ) : 𝑎 ⟶ ( 1 ... 𝑐 ) )
78 76 21 77 sylancl ⊢ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) → ( ◡ 𝑑 ↾ 𝑎 ) : 𝑎 ⟶ ( 1 ... 𝑐 ) )
79 78 ad2antrl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( ◡ 𝑑 ↾ 𝑎 ) : 𝑎 ⟶ ( 1 ... 𝑐 ) )
80 mzprename ⊢ ( ( ( 1 ... 𝑐 ) ∈ V ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ∧ ( ◡ 𝑑 ↾ 𝑎 ) : 𝑎 ⟶ ( 1 ... 𝑐 ) ) → ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑐 ) ) )
81 71 73 79 80 syl3anc ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑐 ) ) )
82 eldioph ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑐 ) ) ) → { 𝑡 ∣ ∃ 𝑔 ∈ ( ℕ0 ↑m ( 1 ... 𝑐 ) ) ( 𝑡 = ( 𝑔 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ 𝑔 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
83 69 70 81 82 syl3anc ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → { 𝑡 ∣ ∃ 𝑔 ∈ ( ℕ0 ↑m ( 1 ... 𝑐 ) ) ( 𝑡 = ( 𝑔 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( ℎ ∈ ( ℤ ↑m ( 1 ... 𝑐 ) ) ↦ ( 𝑏 ‘ ( ℎ ∘ ( ◡ 𝑑 ↾ 𝑎 ) ) ) ) ‘ 𝑔 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
84 68 83 eqeltrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) ∧ ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
85 84 ex ⊢ ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) ∧ ( 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑑 ∈ V ) ) → ( ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) ) )
86 85 rexlimdvva ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → ( ∃ 𝑐 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑑 ∈ V ( 𝑑 : ( 1 ... 𝑐 ) –1-1-onto→ ( 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) ) )
87 17 86 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
88 87 exp31 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) → ( ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) → ( 𝑎 ⊆ 𝑆 → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) ) ) )
89 88 3adant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) → ( ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) → ( 𝑎 ⊆ 𝑆 → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) ) ) )
90 89 imp31 ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ 𝑎 ⊆ 𝑆 ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
91 90 adantrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ ( 𝑎 ⊆ 𝑆 ∧ 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
92 8 91 eqeltrd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) ∧ ( 𝑎 ⊆ 𝑆 ∧ 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
93 92 ex ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ Fin ∧ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ) ) → ( ( 𝑎 ⊆ 𝑆 ∧ 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) ) )
94 93 rexlimdvva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) → ( ∃ 𝑎 ∈ Fin ∃ 𝑏 ∈ ( mzPoly ‘ 𝑎 ) ( 𝑎 ⊆ 𝑆 ∧ 𝑃 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ↾ 𝑎 ) ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) ) )
95 2 94 mpd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑃 ∈ ( mzPoly ‘ 𝑆 ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )