Metamath Proof Explorer

Theorem mzpsubst

Description: Substituting polynomials for the variables of a polynomial results in a polynomial. G is expected to depend on y and provide the polynomials which are being substituted. (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion mzpsubst ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) → 𝑊 ∈ V )
2 elfvex ⊢ ( 𝐹 ∈ ( mzPoly ‘ 𝑉 ) → 𝑉 ∈ V )
3 2 3ad2ant2 ⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) → 𝑉 ∈ V )
4 simp3 ⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) → ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) )
5 simp2 ⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) → 𝐹 ∈ ( mzPoly ‘ 𝑉 ) )
6 simpr ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑥 ∈ ( ℤ ↑m 𝑊 ) )
7 simpll3 ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) )
8 simpll2 ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑉 ∈ V )
9 mzpf ⊢ ( 𝐺 ∈ ( mzPoly ‘ 𝑊 ) → 𝐺 : ( ℤ ↑m 𝑊 ) ⟶ ℤ )
10 9 ffvelrnda ⊢ ( ( 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
11 10 expcom ⊢ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) → ( 𝐺 ∈ ( mzPoly ‘ 𝑊 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ ) )
12 11 ralimdv ⊢ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) → ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) → ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) ∈ ℤ ) )
13 12 imp ⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) → ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
14 eqid ⊢ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) )
15 14 fmpt ⊢ ( ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) ∈ ℤ ↔ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) : 𝑉 ⟶ ℤ )
16 13 15 sylib ⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) → ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) : 𝑉 ⟶ ℤ )
17 16 adantr ⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑉 ∈ V ) → ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) : 𝑉 ⟶ ℤ )
18 zex ⊢ ℤ ∈ V
19 simpr ⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑉 ∈ V ) → 𝑉 ∈ V )
20 elmapg ⊢ ( ( ℤ ∈ V ∧ 𝑉 ∈ V ) → ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) ↔ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) : 𝑉 ⟶ ℤ ) )
21 18 19 20 sylancr ⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑉 ∈ V ) → ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) ↔ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) : 𝑉 ⟶ ℤ ) )
22 17 21 mpbird ⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑉 ∈ V ) → ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) )
23 6 7 8 22 syl21anc ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) )
24 vex ⊢ 𝑏 ∈ V
25 24 fvconst2 ⊢ ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) → ( ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = 𝑏 )
26 23 25 syl ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = 𝑏 )
27 26 mpteq2dva ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ 𝑏 ) )
28 mzpconstmpt ⊢ ( ( 𝑊 ∈ V ∧ 𝑏 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ 𝑏 ) ∈ ( mzPoly ‘ 𝑊 ) )
29 28 3ad2antl1 ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ 𝑏 ) ∈ ( mzPoly ‘ 𝑊 ) )
30 27 29 eqeltrd ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
31 simpr ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑥 ∈ ( ℤ ↑m 𝑊 ) )
32 simpll3 ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) )
33 simpll2 ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑉 ∈ V )
34 31 32 33 22 syl21anc ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) )
35 fveq1 ⊢ ( 𝑐 = ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) → ( 𝑐 ‘ 𝑏 ) = ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ 𝑏 ) )
36 eqid ⊢ ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) = ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) )
37 fvex ⊢ ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ 𝑏 ) ∈ V
38 35 36 37 fvmpt ⊢ ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) → ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ 𝑏 ) )
39 34 38 syl ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ 𝑏 ) )
40 simplr ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑏 ∈ 𝑉 )
41 fvex ⊢ ( ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) ∈ V
42 csbeq1 ⊢ ( 𝑎 = 𝑏 → ⦋ 𝑎 / 𝑦 ⦌ 𝐺 = ⦋ 𝑏 / 𝑦 ⦌ 𝐺 )
43 42 fveq1d ⊢ ( 𝑎 = 𝑏 → ( ⦋ 𝑎 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) = ( ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) )
44 nfcv ⊢ Ⅎ 𝑎 ( 𝐺 ‘ 𝑥 )
45 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑎 / 𝑦 ⦌ 𝐺
46 nfcv ⊢ Ⅎ 𝑦 𝑥
47 45 46 nffv ⊢ Ⅎ 𝑦 ( ⦋ 𝑎 / 𝑦 ⦌ 𝐺 ‘ 𝑥 )
48 csbeq1a ⊢ ( 𝑦 = 𝑎 → 𝐺 = ⦋ 𝑎 / 𝑦 ⦌ 𝐺 )
49 48 fveq1d ⊢ ( 𝑦 = 𝑎 → ( 𝐺 ‘ 𝑥 ) = ( ⦋ 𝑎 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) )
50 44 47 49 cbvmpt ⊢ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) = ( 𝑎 ∈ 𝑉 ↦ ( ⦋ 𝑎 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) )
51 43 50 fvmptg ⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) ∈ V ) → ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ 𝑏 ) = ( ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) )
52 40 41 51 sylancl ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ 𝑏 ) = ( ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) )
53 39 52 eqtrd ⊢ ( ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) )
54 53 mpteq2dva ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) ) )
55 simpr ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
56 simpl3 ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) )
57 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ 𝐺
58 57 nfel1 ⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ∈ ( mzPoly ‘ 𝑊 )
59 csbeq1a ⊢ ( 𝑦 = 𝑏 → 𝐺 = ⦋ 𝑏 / 𝑦 ⦌ 𝐺 )
60 59 eleq1d ⊢ ( 𝑦 = 𝑏 → ( 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ↔ ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) )
61 58 60 rspc ⊢ ( 𝑏 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) → ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) )
62 55 56 61 sylc ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) → ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ∈ ( mzPoly ‘ 𝑊 ) )
63 mzpf ⊢ ( ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ∈ ( mzPoly ‘ 𝑊 ) → ⦋ 𝑏 / 𝑦 ⦌ 𝐺 : ( ℤ ↑m 𝑊 ) ⟶ ℤ )
64 62 63 syl ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) → ⦋ 𝑏 / 𝑦 ⦌ 𝐺 : ( ℤ ↑m 𝑊 ) ⟶ ℤ )
65 64 feqmptd ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) → ⦋ 𝑏 / 𝑦 ⦌ 𝐺 = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ⦋ 𝑏 / 𝑦 ⦌ 𝐺 ‘ 𝑥 ) ) )
66 54 65 eqtr4d ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ⦋ 𝑏 / 𝑦 ⦌ 𝐺 )
67 66 62 eqeltrd ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
68 simp2l ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
69 68 ffnd ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → 𝑏 Fn ( ℤ ↑m 𝑉 ) )
70 simp3l ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
71 70 ffnd ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → 𝑐 Fn ( ℤ ↑m 𝑉 ) )
72 simp13 ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) )
73 simp12 ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → 𝑉 ∈ V )
74 simplll ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑏 Fn ( ℤ ↑m 𝑉 ) )
75 simpllr ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑐 Fn ( ℤ ↑m 𝑉 ) )
76 ovexd ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( ℤ ↑m 𝑉 ) ∈ V )
77 simpr ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑥 ∈ ( ℤ ↑m 𝑊 ) )
78 simplrl ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) )
79 77 78 12 sylc ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
80 79 15 sylib ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) : 𝑉 ⟶ ℤ )
81 simplrr ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → 𝑉 ∈ V )
82 18 81 20 sylancr ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) ↔ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) : 𝑉 ⟶ ℤ ) )
83 80 82 mpbird ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) )
84 fnfvof ⊢ ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ( ℤ ↑m 𝑉 ) ∈ V ∧ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) ) ) → ( ( 𝑏 ∘f + 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) + ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
85 74 75 76 83 84 syl22anc ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( ( 𝑏 ∘f + 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) + ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
86 85 mpteq2dva ⊢ ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f + 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) + ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
87 69 71 72 73 86 syl22anc ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f + 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) + ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
88 simp2r ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
89 simp3r ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
90 mzpaddmpt ⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) + ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
91 88 89 90 syl2anc ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) + ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
92 87 91 eqeltrd ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f + 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
93 fnfvof ⊢ ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ( ℤ ↑m 𝑉 ) ∈ V ∧ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ℤ ↑m 𝑉 ) ) ) → ( ( 𝑏 ∘f · 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) · ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
94 74 75 76 83 93 syl22anc ⊢ ( ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑊 ) ) → ( ( 𝑏 ∘f · 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) · ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
95 94 mpteq2dva ⊢ ( ( ( 𝑏 Fn ( ℤ ↑m 𝑉 ) ∧ 𝑐 Fn ( ℤ ↑m 𝑉 ) ) ∧ ( ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ∧ 𝑉 ∈ V ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f · 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) · ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
96 69 71 72 73 95 syl22anc ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f · 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) · ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
97 mzpmulmpt ⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) · ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
98 88 89 97 syl2anc ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) · ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
99 96 98 eqeltrd ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f · 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
100 fveq1 ⊢ ( 𝑎 = ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) → ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
101 100 mpteq2dv ⊢ ( 𝑎 = ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
102 101 eleq1d ⊢ ( 𝑎 = ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( ( ℤ ↑m 𝑉 ) × { 𝑏 } ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) )
103 fveq1 ⊢ ( 𝑎 = ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) → ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
104 103 mpteq2dv ⊢ ( 𝑎 = ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
105 104 eleq1d ⊢ ( 𝑎 = ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑐 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑐 ‘ 𝑏 ) ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) )
106 fveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
107 106 mpteq2dv ⊢ ( 𝑎 = 𝑏 → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
108 107 eleq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑏 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) )
109 fveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
110 109 mpteq2dv ⊢ ( 𝑎 = 𝑐 → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
111 110 eleq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑐 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) )
112 fveq1 ⊢ ( 𝑎 = ( 𝑏 ∘f + 𝑐 ) → ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝑏 ∘f + 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
113 112 mpteq2dv ⊢ ( 𝑎 = ( 𝑏 ∘f + 𝑐 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f + 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
114 113 eleq1d ⊢ ( 𝑎 = ( 𝑏 ∘f + 𝑐 ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f + 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) )
115 fveq1 ⊢ ( 𝑎 = ( 𝑏 ∘f · 𝑐 ) → ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝑏 ∘f · 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
116 115 mpteq2dv ⊢ ( 𝑎 = ( 𝑏 ∘f · 𝑐 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f · 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
117 116 eleq1d ⊢ ( 𝑎 = ( 𝑏 ∘f · 𝑐 ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( ( 𝑏 ∘f · 𝑐 ) ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) )
118 fveq1 ⊢ ( 𝑎 = 𝐹 → ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
119 118 mpteq2dv ⊢ ( 𝑎 = 𝐹 → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) )
120 119 eleq1d ⊢ ( 𝑎 = 𝐹 → ( ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝑎 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) ) )
121 30 67 92 99 102 105 108 111 114 117 120 mzpindd ⊢ ( ( ( 𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )
122 1 3 4 5 121 syl31anc ⊢ ( ( 𝑊 ∈ V ∧ 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑉 𝐺 ∈ ( mzPoly ‘ 𝑊 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑦 ∈ 𝑉 ↦ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ( mzPoly ‘ 𝑊 ) )