Metamath Proof Explorer

Theorem mzpcong

Description: Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion mzpcong ⊢ F ∈ mzPoly ⁡ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k → N ∥ F ⁡ X − F ⁡ Y

Proof

Step Hyp Ref Expression
1 elfvex ⊢ F ∈ mzPoly ⁡ V → V ∈ V
2 1 3anim1i ⊢ F ∈ mzPoly ⁡ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k → V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k
3 simp1 ⊢ F ∈ mzPoly ⁡ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k → F ∈ mzPoly ⁡ V
4 simpl3l ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ ℤ → N ∈ ℤ
5 simpr ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ ℤ → b ∈ ℤ
6 congid ⊢ N ∈ ℤ ∧ b ∈ ℤ → N ∥ b − b
7 4 5 6 syl2anc ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ ℤ → N ∥ b − b
8 simpl2l ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ ℤ → X ∈ ℤ V
9 vex ⊢ b ∈ V
10 9 fvconst2 ⊢ X ∈ ℤ V → ℤ V × b ⁡ X = b
11 8 10 syl ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ ℤ → ℤ V × b ⁡ X = b
12 simpl2r ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ ℤ → Y ∈ ℤ V
13 9 fvconst2 ⊢ Y ∈ ℤ V → ℤ V × b ⁡ Y = b
14 12 13 syl ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ ℤ → ℤ V × b ⁡ Y = b
15 11 14 oveq12d ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ ℤ → ℤ V × b ⁡ X − ℤ V × b ⁡ Y = b − b
16 7 15 breqtrrd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ ℤ → N ∥ ℤ V × b ⁡ X − ℤ V × b ⁡ Y
17 simpr ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ V → b ∈ V
18 simpl3r ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ V → ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k
19 fveq2 ⊢ k = b → X ⁡ k = X ⁡ b
20 fveq2 ⊢ k = b → Y ⁡ k = Y ⁡ b
21 19 20 oveq12d ⊢ k = b → X ⁡ k − Y ⁡ k = X ⁡ b − Y ⁡ b
22 21 breq2d ⊢ k = b → N ∥ X ⁡ k − Y ⁡ k ↔ N ∥ X ⁡ b − Y ⁡ b
23 22 rspcva ⊢ b ∈ V ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k → N ∥ X ⁡ b − Y ⁡ b
24 17 18 23 syl2anc ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ V → N ∥ X ⁡ b − Y ⁡ b
25 simpl2l ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ V → X ∈ ℤ V
26 fveq1 ⊢ c = X → c ⁡ b = X ⁡ b
27 eqid ⊢ c ∈ ℤ V ⟼ c ⁡ b = c ∈ ℤ V ⟼ c ⁡ b
28 fvex ⊢ X ⁡ b ∈ V
29 26 27 28 fvmpt ⊢ X ∈ ℤ V → c ∈ ℤ V ⟼ c ⁡ b ⁡ X = X ⁡ b
30 25 29 syl ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ V → c ∈ ℤ V ⟼ c ⁡ b ⁡ X = X ⁡ b
31 simpl2r ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ V → Y ∈ ℤ V
32 fveq1 ⊢ c = Y → c ⁡ b = Y ⁡ b
33 fvex ⊢ Y ⁡ b ∈ V
34 32 27 33 fvmpt ⊢ Y ∈ ℤ V → c ∈ ℤ V ⟼ c ⁡ b ⁡ Y = Y ⁡ b
35 31 34 syl ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ V → c ∈ ℤ V ⟼ c ⁡ b ⁡ Y = Y ⁡ b
36 30 35 oveq12d ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ V → c ∈ ℤ V ⟼ c ⁡ b ⁡ X − c ∈ ℤ V ⟼ c ⁡ b ⁡ Y = X ⁡ b − Y ⁡ b
37 24 36 breqtrrd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b ∈ V → N ∥ c ∈ ℤ V ⟼ c ⁡ b ⁡ X − c ∈ ℤ V ⟼ c ⁡ b ⁡ Y
38 simp13l ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → N ∈ ℤ
39 simp2l ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b : ℤ V ⟶ ℤ
40 simp12l ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → X ∈ ℤ V
41 39 40 ffvelcdmd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b ⁡ X ∈ ℤ
42 simp12r ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → Y ∈ ℤ V
43 39 42 ffvelcdmd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b ⁡ Y ∈ ℤ
44 simp3l ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → c : ℤ V ⟶ ℤ
45 44 40 ffvelcdmd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → c ⁡ X ∈ ℤ
46 44 42 ffvelcdmd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → c ⁡ Y ∈ ℤ
47 simp2r ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → N ∥ b ⁡ X − b ⁡ Y
48 simp3r ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → N ∥ c ⁡ X − c ⁡ Y
49 congadd ⊢ N ∈ ℤ ∧ b ⁡ X ∈ ℤ ∧ b ⁡ Y ∈ ℤ ∧ c ⁡ X ∈ ℤ ∧ c ⁡ Y ∈ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ N ∥ c ⁡ X − c ⁡ Y → N ∥ b ⁡ X + c ⁡ X - b ⁡ Y + c ⁡ Y
50 38 41 43 45 46 47 48 49 syl322anc ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → N ∥ b ⁡ X + c ⁡ X - b ⁡ Y + c ⁡ Y
51 39 ffnd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b Fn ℤ V
52 44 ffnd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → c Fn ℤ V
53 ovexd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → ℤ V ∈ V
54 fnfvof ⊢ b Fn ℤ V ∧ c Fn ℤ V ∧ ℤ V ∈ V ∧ X ∈ ℤ V → b + f c ⁡ X = b ⁡ X + c ⁡ X
55 51 52 53 40 54 syl22anc ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b + f c ⁡ X = b ⁡ X + c ⁡ X
56 fnfvof ⊢ b Fn ℤ V ∧ c Fn ℤ V ∧ ℤ V ∈ V ∧ Y ∈ ℤ V → b + f c ⁡ Y = b ⁡ Y + c ⁡ Y
57 51 52 53 42 56 syl22anc ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b + f c ⁡ Y = b ⁡ Y + c ⁡ Y
58 55 57 oveq12d ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b + f c ⁡ X − b + f c ⁡ Y = b ⁡ X + c ⁡ X - b ⁡ Y + c ⁡ Y
59 50 58 breqtrrd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → N ∥ b + f c ⁡ X − b + f c ⁡ Y
60 congmul ⊢ N ∈ ℤ ∧ b ⁡ X ∈ ℤ ∧ b ⁡ Y ∈ ℤ ∧ c ⁡ X ∈ ℤ ∧ c ⁡ Y ∈ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ N ∥ c ⁡ X − c ⁡ Y → N ∥ b ⁡ X ⁢ c ⁡ X − b ⁡ Y ⁢ c ⁡ Y
61 38 41 43 45 46 47 48 60 syl322anc ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → N ∥ b ⁡ X ⁢ c ⁡ X − b ⁡ Y ⁢ c ⁡ Y
62 fnfvof ⊢ b Fn ℤ V ∧ c Fn ℤ V ∧ ℤ V ∈ V ∧ X ∈ ℤ V → b × f c ⁡ X = b ⁡ X ⁢ c ⁡ X
63 51 52 53 40 62 syl22anc ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b × f c ⁡ X = b ⁡ X ⁢ c ⁡ X
64 fnfvof ⊢ b Fn ℤ V ∧ c Fn ℤ V ∧ ℤ V ∈ V ∧ Y ∈ ℤ V → b × f c ⁡ Y = b ⁡ Y ⁢ c ⁡ Y
65 51 52 53 42 64 syl22anc ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b × f c ⁡ Y = b ⁡ Y ⁢ c ⁡ Y
66 63 65 oveq12d ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → b × f c ⁡ X − b × f c ⁡ Y = b ⁡ X ⁢ c ⁡ X − b ⁡ Y ⁢ c ⁡ Y
67 61 66 breqtrrd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ b : ℤ V ⟶ ℤ ∧ N ∥ b ⁡ X − b ⁡ Y ∧ c : ℤ V ⟶ ℤ ∧ N ∥ c ⁡ X − c ⁡ Y → N ∥ b × f c ⁡ X − b × f c ⁡ Y
68 fveq1 ⊢ a = ℤ V × b → a ⁡ X = ℤ V × b ⁡ X
69 fveq1 ⊢ a = ℤ V × b → a ⁡ Y = ℤ V × b ⁡ Y
70 68 69 oveq12d ⊢ a = ℤ V × b → a ⁡ X − a ⁡ Y = ℤ V × b ⁡ X − ℤ V × b ⁡ Y
71 70 breq2d ⊢ a = ℤ V × b → N ∥ a ⁡ X − a ⁡ Y ↔ N ∥ ℤ V × b ⁡ X − ℤ V × b ⁡ Y
72 fveq1 ⊢ a = c ∈ ℤ V ⟼ c ⁡ b → a ⁡ X = c ∈ ℤ V ⟼ c ⁡ b ⁡ X
73 fveq1 ⊢ a = c ∈ ℤ V ⟼ c ⁡ b → a ⁡ Y = c ∈ ℤ V ⟼ c ⁡ b ⁡ Y
74 72 73 oveq12d ⊢ a = c ∈ ℤ V ⟼ c ⁡ b → a ⁡ X − a ⁡ Y = c ∈ ℤ V ⟼ c ⁡ b ⁡ X − c ∈ ℤ V ⟼ c ⁡ b ⁡ Y
75 74 breq2d ⊢ a = c ∈ ℤ V ⟼ c ⁡ b → N ∥ a ⁡ X − a ⁡ Y ↔ N ∥ c ∈ ℤ V ⟼ c ⁡ b ⁡ X − c ∈ ℤ V ⟼ c ⁡ b ⁡ Y
76 fveq1 ⊢ a = b → a ⁡ X = b ⁡ X
77 fveq1 ⊢ a = b → a ⁡ Y = b ⁡ Y
78 76 77 oveq12d ⊢ a = b → a ⁡ X − a ⁡ Y = b ⁡ X − b ⁡ Y
79 78 breq2d ⊢ a = b → N ∥ a ⁡ X − a ⁡ Y ↔ N ∥ b ⁡ X − b ⁡ Y
80 fveq1 ⊢ a = c → a ⁡ X = c ⁡ X
81 fveq1 ⊢ a = c → a ⁡ Y = c ⁡ Y
82 80 81 oveq12d ⊢ a = c → a ⁡ X − a ⁡ Y = c ⁡ X − c ⁡ Y
83 82 breq2d ⊢ a = c → N ∥ a ⁡ X − a ⁡ Y ↔ N ∥ c ⁡ X − c ⁡ Y
84 fveq1 ⊢ a = b + f c → a ⁡ X = b + f c ⁡ X
85 fveq1 ⊢ a = b + f c → a ⁡ Y = b + f c ⁡ Y
86 84 85 oveq12d ⊢ a = b + f c → a ⁡ X − a ⁡ Y = b + f c ⁡ X − b + f c ⁡ Y
87 86 breq2d ⊢ a = b + f c → N ∥ a ⁡ X − a ⁡ Y ↔ N ∥ b + f c ⁡ X − b + f c ⁡ Y
88 fveq1 ⊢ a = b × f c → a ⁡ X = b × f c ⁡ X
89 fveq1 ⊢ a = b × f c → a ⁡ Y = b × f c ⁡ Y
90 88 89 oveq12d ⊢ a = b × f c → a ⁡ X − a ⁡ Y = b × f c ⁡ X − b × f c ⁡ Y
91 90 breq2d ⊢ a = b × f c → N ∥ a ⁡ X − a ⁡ Y ↔ N ∥ b × f c ⁡ X − b × f c ⁡ Y
92 fveq1 ⊢ a = F → a ⁡ X = F ⁡ X
93 fveq1 ⊢ a = F → a ⁡ Y = F ⁡ Y
94 92 93 oveq12d ⊢ a = F → a ⁡ X − a ⁡ Y = F ⁡ X − F ⁡ Y
95 94 breq2d ⊢ a = F → N ∥ a ⁡ X − a ⁡ Y ↔ N ∥ F ⁡ X − F ⁡ Y
96 16 37 59 67 71 75 79 83 87 91 95 mzpindd ⊢ V ∈ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k ∧ F ∈ mzPoly ⁡ V → N ∥ F ⁡ X − F ⁡ Y
97 2 3 96 syl2anc ⊢ F ∈ mzPoly ⁡ V ∧ X ∈ ℤ V ∧ Y ∈ ℤ V ∧ N ∈ ℤ ∧ ∀ k ∈ V N ∥ X ⁡ k − Y ⁡ k → N ∥ F ⁡ X − F ⁡ Y