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	ffvelcdmd	⊢ ( ( ( 𝑉 ∈ V ∧ ( 𝑋 ∈ ( ℤ ↑m 𝑉 ) ∧ 𝑌 ∈ ( ℤ ↑m 𝑉 ) ) ∧ ( 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ 𝑉 𝑁 ∥ ( ( 𝑋 ‘ 𝑘 ) − ( 𝑌 ‘ 𝑘 ) ) ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑏 ‘ 𝑋 ) − ( 𝑏 ‘ 𝑌 ) ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑐 ‘ 𝑋 ) − ( 𝑐 ‘ 𝑌 ) ) ) ) → ( 𝑏 ‘ 𝑋 ) ∈ ℤ )
42		simp12r	⊢ ( ( ( 𝑉 ∈ V ∧ ( 𝑋 ∈ ( ℤ ↑m 𝑉 ) ∧ 𝑌 ∈ ( ℤ ↑m 𝑉 ) ) ∧ ( 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ 𝑉 𝑁 ∥ ( ( 𝑋 ‘ 𝑘 ) − ( 𝑌 ‘ 𝑘 ) ) ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑏 ‘ 𝑋 ) − ( 𝑏 ‘ 𝑌 ) ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑐 ‘ 𝑋 ) − ( 𝑐 ‘ 𝑌 ) ) ) ) → 𝑌 ∈ ( ℤ ↑m 𝑉 ) )
43	39 42	ffvelcdmd	⊢ ( ( ( 𝑉 ∈ V ∧ ( 𝑋 ∈ ( ℤ ↑m 𝑉 ) ∧ 𝑌 ∈ ( ℤ ↑m 𝑉 ) ) ∧ ( 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ 𝑉 𝑁 ∥ ( ( 𝑋 ‘ 𝑘 ) − ( 𝑌 ‘ 𝑘 ) ) ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑏 ‘ 𝑋 ) − ( 𝑏 ‘ 𝑌 ) ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑐 ‘ 𝑋 ) − ( 𝑐 ‘ 𝑌 ) ) ) ) → ( 𝑏 ‘ 𝑌 ) ∈ ℤ )
44		simp3l	⊢ ( ( ( 𝑉 ∈ V ∧ ( 𝑋 ∈ ( ℤ ↑m 𝑉 ) ∧ 𝑌 ∈ ( ℤ ↑m 𝑉 ) ) ∧ ( 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ 𝑉 𝑁 ∥ ( ( 𝑋 ‘ 𝑘 ) − ( 𝑌 ‘ 𝑘 ) ) ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑏 ‘ 𝑋 ) − ( 𝑏 ‘ 𝑌 ) ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑐 ‘ 𝑋 ) − ( 𝑐 ‘ 𝑌 ) ) ) ) → 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
45	44 40	ffvelcdmd	⊢ ( ( ( 𝑉 ∈ V ∧ ( 𝑋 ∈ ( ℤ ↑m 𝑉 ) ∧ 𝑌 ∈ ( ℤ ↑m 𝑉 ) ) ∧ ( 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ 𝑉 𝑁 ∥ ( ( 𝑋 ‘ 𝑘 ) − ( 𝑌 ‘ 𝑘 ) ) ) ) ∧ ( 𝑏 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑏 ‘ 𝑋 ) − ( 𝑏 ‘ 𝑌 ) ) ) ∧ ( 𝑐 : ( ℤ ↑m 𝑉 ) ⟶ ℤ ∧ 𝑁 ∥ ( ( 𝑐 ‘ 𝑋 ) − ( 𝑐 ‘ 𝑌 ) ) ) ) → ( 𝑐 ‘ 𝑋 ) ∈ ℤ )
46	44 42	ffvelcdmd	⊢ ( ( ( 𝑉 ∈ 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 𝑉 ) ) ∧ ( 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ 𝑉 𝑁 ∥ ( ( 𝑋 ‘ 𝑘 ) − ( 𝑌 ‘ 𝑘 ) ) ) ) → 𝑁 ∥ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑌 ) ) )