Metamath Proof Explorer

Theorem mzpindd

Description: "Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Hypotheses mzpindd.co ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → 𝜒 )
mzpindd.pr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑉 ) → 𝜃 )
mzpindd.ad ⊢ ( ( 𝜑 ∧ ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) → 𝜁 )
mzpindd.mu ⊢ ( ( 𝜑 ∧ ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) → 𝜎 )
mzpindd.1 ⊢ ( 𝑥 = ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) → ( 𝜓 ↔ 𝜒 ) )
mzpindd.2 ⊢ ( 𝑥 = ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) → ( 𝜓 ↔ 𝜃 ) )
mzpindd.3 ⊢ ( 𝑥 = 𝑓 → ( 𝜓 ↔ 𝜏 ) )
mzpindd.4 ⊢ ( 𝑥 = 𝑔 → ( 𝜓 ↔ 𝜂 ) )
mzpindd.5 ⊢ ( 𝑥 = ( 𝑓 ∘f + 𝑔 ) → ( 𝜓 ↔ 𝜁 ) )
mzpindd.6 ⊢ ( 𝑥 = ( 𝑓 ∘f · 𝑔 ) → ( 𝜓 ↔ 𝜎 ) )
mzpindd.7 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜌 ) )
Assertion mzpindd ( ( 𝜑 ∧ 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝜌 )

Proof

Step Hyp Ref Expression
1 mzpindd.co ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → 𝜒 )
2 mzpindd.pr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑉 ) → 𝜃 )
3 mzpindd.ad ⊢ ( ( 𝜑 ∧ ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) → 𝜁 )
4 mzpindd.mu ⊢ ( ( 𝜑 ∧ ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) → 𝜎 )
5 mzpindd.1 ⊢ ( 𝑥 = ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) → ( 𝜓 ↔ 𝜒 ) )
6 mzpindd.2 ⊢ ( 𝑥 = ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) → ( 𝜓 ↔ 𝜃 ) )
7 mzpindd.3 ⊢ ( 𝑥 = 𝑓 → ( 𝜓 ↔ 𝜏 ) )
8 mzpindd.4 ⊢ ( 𝑥 = 𝑔 → ( 𝜓 ↔ 𝜂 ) )
9 mzpindd.5 ⊢ ( 𝑥 = ( 𝑓 ∘f + 𝑔 ) → ( 𝜓 ↔ 𝜁 ) )
10 mzpindd.6 ⊢ ( 𝑥 = ( 𝑓 ∘f · 𝑔 ) → ( 𝜓 ↔ 𝜎 ) )
11 mzpindd.7 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜌 ) )
12 elfvex ⊢ ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) → 𝑉 ∈ V )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝑉 ∈ V )
14 mzpval ⊢ ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) = ∩ ( mzPolyCld ‘ 𝑉 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → ( mzPoly ‘ 𝑉 ) = ∩ ( mzPolyCld ‘ 𝑉 ) )
16 ssrab2 ⊢ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) )
17 16 a1i ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
18 ovex ⊢ ( ℤ ↑m 𝑉 ) ∈ V
19 zex ⊢ ℤ ∈ V
20 18 19 constmap ⊢ ( 𝑓 ∈ ℤ → ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
22 5 elrab ⊢ ( ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ↔ ( ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜒 ) )
23 21 1 22 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
26 19 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) ∧ 𝑔 ∈ ( ℤ ↑m 𝑉 ) ) → ℤ ∈ V )
27 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) ∧ 𝑔 ∈ ( ℤ ↑m 𝑉 ) ) → 𝑉 ∈ V )
28 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) ∧ 𝑔 ∈ ( ℤ ↑m 𝑉 ) ) → 𝑔 ∈ ( ℤ ↑m 𝑉 ) )
29 elmapg ⊢ ( ( ℤ ∈ V ∧ 𝑉 ∈ V ) → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↔ 𝑔 : 𝑉 ⟶ ℤ ) )
30 29 biimpa ⊢ ( ( ( ℤ ∈ V ∧ 𝑉 ∈ V ) ∧ 𝑔 ∈ ( ℤ ↑m 𝑉 ) ) → 𝑔 : 𝑉 ⟶ ℤ )
31 26 27 28 30 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) ∧ 𝑔 ∈ ( ℤ ↑m 𝑉 ) ) → 𝑔 : 𝑉 ⟶ ℤ )
32 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) ∧ 𝑔 ∈ ( ℤ ↑m 𝑉 ) ) → 𝑓 ∈ 𝑉 )
33 31 32 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) ∧ 𝑔 ∈ ( ℤ ↑m 𝑉 ) ) → ( 𝑔 ‘ 𝑓 ) ∈ ℤ )
34 33 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
35 19 18 elmap ⊢ ( ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ↔ ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
36 34 35 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
37 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) → 𝜃 )
38 6 elrab ⊢ ( ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ↔ ( ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜃 ) )
39 36 37 38 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝑓 ∈ 𝑉 ) → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
40 39 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
41 25 40 jca ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) )
42 zaddcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
43 42 adantl ⊢ ( ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
44 simpl ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ) → 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
45 simpr ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ) → 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
46 18 a1i ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ) → ( ℤ ↑m 𝑉 ) ∈ V )
47 inidm ⊢ ( ( ℤ ↑m 𝑉 ) ∩ ( ℤ ↑m 𝑉 ) ) = ( ℤ ↑m 𝑉 )
48 43 44 45 46 46 47 off ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ) → ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
49 48 ad2ant2r ⊢ ( ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) → ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
50 49 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) ) → ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
51 3 3expb ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) ) → 𝜁 )
52 50 51 jca ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜁 ) )
53 zmulcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
54 53 adantl ⊢ ( ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
55 54 44 45 46 46 47 off ⊢ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ) → ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
56 55 ad2ant2r ⊢ ( ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) → ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
57 56 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) ) → ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
58 4 3expb ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) ) → 𝜎 )
59 52 57 58 jca32 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) ) → ( ( ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜁 ) ∧ ( ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜎 ) ) )
60 59 ex ⊢ ( 𝜑 → ( ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) → ( ( ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜁 ) ∧ ( ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜎 ) ) ) )
61 19 18 elmap ⊢ ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ↔ 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
62 61 anbi1i ⊢ ( ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜏 ) ↔ ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) )
63 19 18 elmap ⊢ ( 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ↔ 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
64 63 anbi1i ⊢ ( ( 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜂 ) ↔ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) )
65 62 64 anbi12i ⊢ ( ( ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜏 ) ∧ ( 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜂 ) ) ↔ ( ( 𝑓 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜏 ) ∧ ( 𝑔 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜂 ) ) )
66 19 18 elmap ⊢ ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ↔ ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
67 66 anbi1i ⊢ ( ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜁 ) ↔ ( ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜁 ) )
68 19 18 elmap ⊢ ( ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ↔ ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
69 68 anbi1i ⊢ ( ( ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜎 ) ↔ ( ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜎 ) )
70 67 69 anbi12i ⊢ ( ( ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜁 ) ∧ ( ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜎 ) ) ↔ ( ( ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜁 ) ∧ ( ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝜎 ) ) )
71 60 65 70 3imtr4g ⊢ ( 𝜑 → ( ( ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜏 ) ∧ ( 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜂 ) ) → ( ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜁 ) ∧ ( ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜎 ) ) ) )
72 7 elrab ⊢ ( 𝑓 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ↔ ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜏 ) )
73 8 elrab ⊢ ( 𝑔 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ↔ ( 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜂 ) )
74 72 73 anbi12i ⊢ ( ( 𝑓 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ 𝑔 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) ↔ ( ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜏 ) ∧ ( 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜂 ) ) )
75 9 elrab ⊢ ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ↔ ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜁 ) )
76 10 elrab ⊢ ( ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ↔ ( ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜎 ) )
77 75 76 anbi12i ⊢ ( ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) ↔ ( ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜁 ) ∧ ( ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜎 ) ) )
78 71 74 77 3imtr4g ⊢ ( 𝜑 → ( ( 𝑓 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ 𝑔 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) → ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) ) )
79 78 ralrimivv ⊢ ( 𝜑 → ∀ 𝑓 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∀ 𝑔 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → ∀ 𝑓 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∀ 𝑔 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) )
81 17 41 80 jca32 ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → ( { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) ∧ ∀ 𝑓 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∀ 𝑔 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) ) ) )
82 elmzpcl ⊢ ( 𝑉 ∈ V → ( { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∈ ( mzPolyCld ‘ 𝑉 ) ↔ ( { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) ∧ ∀ 𝑓 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∀ 𝑔 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) ) ) ) )
83 82 adantl ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → ( { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∈ ( mzPolyCld ‘ 𝑉 ) ↔ ( { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) ∧ ∀ 𝑓 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∀ 𝑔 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∧ ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ) ) ) ) )
84 81 83 mpbird ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∈ ( mzPolyCld ‘ 𝑉 ) )
85 intss1 ⊢ ( { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ∈ ( mzPolyCld ‘ 𝑉 ) → ∩ ( mzPolyCld ‘ 𝑉 ) ⊆ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
86 84 85 syl ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → ∩ ( mzPolyCld ‘ 𝑉 ) ⊆ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
87 15 86 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑉 ∈ V ) → ( mzPoly ‘ 𝑉 ) ⊆ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
88 87 sselda ⊢ ( ( ( 𝜑 ∧ 𝑉 ∈ V ) ∧ 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝐴 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
89 88 an32s ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑉 ∈ V ) → 𝐴 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
90 13 89 mpdan ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝐴 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } )
91 11 elrab ⊢ ( 𝐴 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } ↔ ( 𝐴 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ 𝜌 ) )
92 91 simprbi ⊢ ( 𝐴 ∈ { 𝑥 ∈ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ 𝜓 } → 𝜌 )
93 90 92 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝜌 )