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 ( ( 𝐹 ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑋 ∈ ( ℤ ↑m 𝑉 ) ∧ 𝑌 ∈ ( ℤ ↑m 𝑉 ) ) ∧ ( 𝑁 ∈ ℤ ∧ ∀ 𝑘𝑉 𝑁 ∥ ( ( 𝑋𝑘 ) − ( 𝑌𝑘 ) ) ) ) → 𝑁 ∥ ( ( 𝐹𝑋 ) − ( 𝐹𝑌 ) ) )

Proof

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