mzpcong - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mzpcong		Structured version Visualization version GIF version

Theorem mzpcong 43400

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

**Assertion**
Ref	Expression
mzpcong	⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))

Distinct variable groups: 𝑘,𝑋 𝑘,𝑉 𝑘,𝑌 𝑘,𝑁 Allowed substitution hint: 𝐹(𝑘)

Proof of Theorem mzpcong Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfvex 6876	. . 3 ⊢ (𝐹 ∈ (mzPoly‘𝑉) → 𝑉 ∈ V)
2	1	3anim1i 1153	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → (𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))))
3		simp1 1137	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝐹 ∈ (mzPoly‘𝑉))
4		simpl3l 1230	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
5		simpr 484	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
6		congid 43399	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
7	4, 5, 6	syl2anc 585	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
8		simpl2l 1228	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈ (ℤ ↑_m 𝑉))
9		vex 3434	. . . . . . 7 ⊢ 𝑏 ∈ V
10	9	fvconst2 7159	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
11	8, 10	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
12		simpl2r 1229	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑌 ∈ (ℤ ↑_m 𝑉))
13	9	fvconst2 7159	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
14	12, 13	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
15	11, 14	oveq12d 7385	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)) = (𝑏 − 𝑏))
16	7, 15	breqtrrd 5114	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
17		simpr 484	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉)
18		simpl3r 1231	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))
19		fveq2 6841	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑋‘𝑘) = (𝑋‘𝑏))
20		fveq2 6841	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑌‘𝑘) = (𝑌‘𝑏))
21	19, 20	oveq12d 7385	. . . . . . 7 ⊢ (𝑘 = 𝑏 → ((𝑋‘𝑘) − (𝑌‘𝑘)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
22	21	breq2d 5098	. . . . . 6 ⊢ (𝑘 = 𝑏 → (𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)) ↔ 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏))))
23	22	rspcva 3563	. . . . 5 ⊢ ((𝑏 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘))) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
24	17, 18, 23	syl2anc 585	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
25		simpl2l 1228	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑋 ∈ (ℤ ↑_m 𝑉))
26		fveq1 6840	. . . . . . 7 ⊢ (𝑐 = 𝑋 → (𝑐‘𝑏) = (𝑋‘𝑏))
27		eqid 2737	. . . . . . 7 ⊢ (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))
28		fvex 6854	. . . . . . 7 ⊢ (𝑋‘𝑏) ∈ V
29	26, 27, 28	fvmpt 6948	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
30	25, 29	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
31		simpl2r 1229	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑌 ∈ (ℤ ↑_m 𝑉))
32		fveq1 6840	. . . . . . 7 ⊢ (𝑐 = 𝑌 → (𝑐‘𝑏) = (𝑌‘𝑏))
33		fvex 6854	. . . . . . 7 ⊢ (𝑌‘𝑏) ∈ V
34	32, 27, 33	fvmpt 6948	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
35	31, 34	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
36	30, 35	oveq12d 7385	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
37	24, 36	breqtrrd 5114	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
38		simp13l 1290	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∈ ℤ)
39		simp2l 1201	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏:(ℤ ↑_m 𝑉)⟶ℤ)
40		simp12l 1288	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑋 ∈ (ℤ ↑_m 𝑉))
41	39, 40	ffvelcdmd 7038	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑋) ∈ ℤ)
42		simp12r 1289	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑌 ∈ (ℤ ↑_m 𝑉))
43	39, 42	ffvelcdmd 7038	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑌) ∈ ℤ)
44		simp3l 1203	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐:(ℤ ↑_m 𝑉)⟶ℤ)
45	44, 40	ffvelcdmd 7038	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑋) ∈ ℤ)
46	44, 42	ffvelcdmd 7038	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑌) ∈ ℤ)
47		simp2r 1202	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)))
48		simp3r 1204	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))
49		congadd 43394	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
50	38, 41, 43, 45, 46, 47, 48, 49	syl322anc 1401	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
51	39	ffnd 6670	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏 Fn (ℤ ↑_m 𝑉))
52	44	ffnd 6670	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐 Fn (ℤ ↑_m 𝑉))
53		ovexd 7402	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (ℤ ↑_m 𝑉) ∈ V)
54		fnfvof 7648	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f + 𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋)))
55	51, 52, 53, 40, 54	syl22anc 839	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f + 𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋)))
56		fnfvof 7648	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f + 𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌)))
57	51, 52, 53, 42, 56	syl22anc 839	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f + 𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌)))
58	55, 57	oveq12d 7385	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)) = (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
59	50, 58	breqtrrd 5114	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
60		congmul 43395	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
61	38, 41, 43, 45, 46, 47, 48, 60	syl322anc 1401	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
62		fnfvof 7648	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f · 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋)))
63	51, 52, 53, 40, 62	syl22anc 839	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f · 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋)))
64		fnfvof 7648	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f · 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌)))
65	51, 52, 53, 42, 64	syl22anc 839	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f · 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌)))
66	63, 65	oveq12d 7385	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)) = (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
67	61, 66	breqtrrd 5114	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
68		fveq1 6840	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑋) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋))
69		fveq1 6840	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑌) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))
70	68, 69	oveq12d 7385	. . . 4 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
71	70	breq2d 5098	. . 3 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))))
72		fveq1 6840	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑋) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋))
73		fveq1 6840	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑌) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))
74	72, 73	oveq12d 7385	. . . 4 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
75	74	breq2d 5098	. . 3 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))))
76		fveq1 6840	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑋) = (𝑏‘𝑋))
77		fveq1 6840	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑌) = (𝑏‘𝑌))
78	76, 77	oveq12d 7385	. . . 4 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑏‘𝑋) − (𝑏‘𝑌)))
79	78	breq2d 5098	. . 3 ⊢ (𝑎 = 𝑏 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))))
80		fveq1 6840	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑋) = (𝑐‘𝑋))
81		fveq1 6840	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑌) = (𝑐‘𝑌))
82	80, 81	oveq12d 7385	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑐‘𝑋) − (𝑐‘𝑌)))
83	82	breq2d 5098	. . 3 ⊢ (𝑎 = 𝑐 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌))))
84		fveq1 6840	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f + 𝑐)‘𝑋))
85		fveq1 6840	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f + 𝑐)‘𝑌))
86	84, 85	oveq12d 7385	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
87	86	breq2d 5098	. . 3 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌))))
88		fveq1 6840	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f · 𝑐)‘𝑋))
89		fveq1 6840	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f · 𝑐)‘𝑌))
90	88, 89	oveq12d 7385	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
91	90	breq2d 5098	. . 3 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌))))
92		fveq1 6840	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑋) = (𝐹‘𝑋))
93		fveq1 6840	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑌) = (𝐹‘𝑌))
94	92, 93	oveq12d 7385	. . . 4 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝐹‘𝑋) − (𝐹‘𝑌)))
95	94	breq2d 5098	. . 3 ⊢ (𝑎 = 𝐹 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))))
96	16, 37, 59, 67, 71, 75, 79, 83, 87, 91, 95	mzpindd 43178	. 2 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝐹 ∈ (mzPoly‘𝑉)) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))
97	2, 3, 96	syl2anc 585	1 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 Vcvv 3430 {csn 4568 class class class wbr 5086 ↦ cmpt 5167 × cxp 5629 Fn wfn 6494 ⟶wf 6495 ‘cfv 6499 (class class class)co 7367 ∘_f cof 7629 ↑_m cmap 8773 + caddc 11041 · cmul 11043 − cmin 11377 ℤcz 12524 ∥ cdvds 16221 mzPolycmzp 43154

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5308 ax-pr 5376 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6266 df-ord 6327 df-on 6328 df-lim 6329 df-suc 6330 df-iota 6455 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-map 8775 df-en 8894 df-dom 8895 df-sdom 8896 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-n0 12438 df-z 12525 df-dvds 16222 df-mzpcl 43155 df-mzp 43156

This theorem is referenced by: (None)

W3C validator