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	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑉 ∈ 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 ‘ 𝑉 ) ) → 𝜌 )