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∈VN∥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∈VN∥X⁡k−Y⁡k→V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k
3 simp1 ⊢F∈mzPoly⁡V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k→F∈mzPoly⁡V
4 simpl3l ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b∈ℤ→N∈ℤ
5 simpr ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥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∈VN∥X⁡k−Y⁡k∧b∈ℤ→N∥b−b
8 simpl2l ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥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∈VN∥X⁡k−Y⁡k∧b∈ℤ→ℤV×b⁡X=b
12 simpl2r ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥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∈VN∥X⁡k−Y⁡k∧b∈ℤ→ℤV×b⁡Y=b
15 11 14 oveq12d ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥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∈VN∥X⁡k−Y⁡k∧b∈ℤ→N∥ℤV×b⁡X−ℤV×b⁡Y
17 simpr ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b∈V→b∈V
18 simpl3r ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b∈V→∀k∈VN∥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∈VN∥X⁡k−Y⁡k→N∥X⁡b−Y⁡b
24 17 18 23 syl2anc ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b∈V→N∥X⁡b−Y⁡b
25 simpl2l ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥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∈VN∥X⁡k−Y⁡k∧b∈V→c∈ℤV⟼c⁡b⁡X=X⁡b
31 simpl2r ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥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∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→bFnℤV
52 44 ffnd ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→cFnℤV
53 ovexd ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→ℤV∈V
54 fnfvof ⊢bFnℤV∧cFnℤV∧ℤV∈V∧X∈ℤV→b+fc⁡X=b⁡X+c⁡X
55 51 52 53 40 54 syl22anc ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→b+fc⁡X=b⁡X+c⁡X
56 fnfvof ⊢bFnℤV∧cFnℤV∧ℤV∈V∧Y∈ℤV→b+fc⁡Y=b⁡Y+c⁡Y
57 51 52 53 42 56 syl22anc ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→b+fc⁡Y=b⁡Y+c⁡Y
58 55 57 oveq12d ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→b+fc⁡X−b+fc⁡Y=b⁡X+c⁡X-b⁡Y+c⁡Y
59 50 58 breqtrrd ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→N∥b+fc⁡X−b+fc⁡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∈VN∥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 ⊢bFnℤV∧cFnℤV∧ℤV∈V∧X∈ℤV→b×fc⁡X=b⁡X⁢c⁡X
63 51 52 53 40 62 syl22anc ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→b×fc⁡X=b⁡X⁢c⁡X
64 fnfvof ⊢bFnℤV∧cFnℤV∧ℤV∈V∧Y∈ℤV→b×fc⁡Y=b⁡Y⁢c⁡Y
65 51 52 53 42 64 syl22anc ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→b×fc⁡Y=b⁡Y⁢c⁡Y
66 63 65 oveq12d ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→b×fc⁡X−b×fc⁡Y=b⁡X⁢c⁡X−b⁡Y⁢c⁡Y
67 61 66 breqtrrd ⊢V∈V∧X∈ℤV∧Y∈ℤV∧N∈ℤ∧∀k∈VN∥X⁡k−Y⁡k∧b:ℤV⟶ℤ∧N∥b⁡X−b⁡Y∧c:ℤV⟶ℤ∧N∥c⁡X−c⁡Y→N∥b×fc⁡X−b×fc⁡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+fc→a⁡X=b+fc⁡X
85 fveq1 ⊢a=b+fc→a⁡Y=b+fc⁡Y
86 84 85 oveq12d ⊢a=b+fc→a⁡X−a⁡Y=b+fc⁡X−b+fc⁡Y
87 86 breq2d ⊢a=b+fc→N∥a⁡X−a⁡Y↔N∥b+fc⁡X−b+fc⁡Y
88 fveq1 ⊢a=b×fc→a⁡X=b×fc⁡X
89 fveq1 ⊢a=b×fc→a⁡Y=b×fc⁡Y
90 88 89 oveq12d ⊢a=b×fc→a⁡X−a⁡Y=b×fc⁡X−b×fc⁡Y
91 90 breq2d ⊢a=b×fc→N∥a⁡X−a⁡Y↔N∥b×fc⁡X−b×fc⁡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∈VN∥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∈VN∥X⁡k−Y⁡k→N∥F⁡X−F⁡Y