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 39562

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 6698	. . 3 ⊢ (𝐹 ∈ (mzPoly‘𝑉) → 𝑉 ∈ V)
2	1	3anim1i 1148	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → (𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))))
3		simp1 1132	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝐹 ∈ (mzPoly‘𝑉))
4		simpl3l 1224	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
5		simpr 487	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
6		congid 39561	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
7	4, 5, 6	syl2anc 586	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
8		simpl2l 1222	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈ (ℤ ↑_m 𝑉))
9		vex 3498	. . . . . . 7 ⊢ 𝑏 ∈ V
10	9	fvconst2 6961	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
11	8, 10	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
12		simpl2r 1223	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑌 ∈ (ℤ ↑_m 𝑉))
13	9	fvconst2 6961	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
14	12, 13	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
15	11, 14	oveq12d 7168	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)) = (𝑏 − 𝑏))
16	7, 15	breqtrrd 5087	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
17		simpr 487	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉)
18		simpl3r 1225	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))
19		fveq2 6665	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑋‘𝑘) = (𝑋‘𝑏))
20		fveq2 6665	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑌‘𝑘) = (𝑌‘𝑏))
21	19, 20	oveq12d 7168	. . . . . . 7 ⊢ (𝑘 = 𝑏 → ((𝑋‘𝑘) − (𝑌‘𝑘)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
22	21	breq2d 5071	. . . . . 6 ⊢ (𝑘 = 𝑏 → (𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)) ↔ 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏))))
23	22	rspcva 3621	. . . . 5 ⊢ ((𝑏 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘))) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
24	17, 18, 23	syl2anc 586	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
25		simpl2l 1222	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑋 ∈ (ℤ ↑_m 𝑉))
26		fveq1 6664	. . . . . . 7 ⊢ (𝑐 = 𝑋 → (𝑐‘𝑏) = (𝑋‘𝑏))
27		eqid 2821	. . . . . . 7 ⊢ (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))
28		fvex 6678	. . . . . . 7 ⊢ (𝑋‘𝑏) ∈ V
29	26, 27, 28	fvmpt 6763	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
30	25, 29	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
31		simpl2r 1223	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑌 ∈ (ℤ ↑_m 𝑉))
32		fveq1 6664	. . . . . . 7 ⊢ (𝑐 = 𝑌 → (𝑐‘𝑏) = (𝑌‘𝑏))
33		fvex 6678	. . . . . . 7 ⊢ (𝑌‘𝑏) ∈ V
34	32, 27, 33	fvmpt 6763	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
35	31, 34	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
36	30, 35	oveq12d 7168	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
37	24, 36	breqtrrd 5087	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
38		simp13l 1284	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∈ ℤ)
39		simp2l 1195	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏:(ℤ ↑_m 𝑉)⟶ℤ)
40		simp12l 1282	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑋 ∈ (ℤ ↑_m 𝑉))
41	39, 40	ffvelrnd 6847	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑋) ∈ ℤ)
42		simp12r 1283	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑌 ∈ (ℤ ↑_m 𝑉))
43	39, 42	ffvelrnd 6847	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑌) ∈ ℤ)
44		simp3l 1197	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐:(ℤ ↑_m 𝑉)⟶ℤ)
45	44, 40	ffvelrnd 6847	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑋) ∈ ℤ)
46	44, 42	ffvelrnd 6847	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑌) ∈ ℤ)
47		simp2r 1196	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)))
48		simp3r 1198	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))
49		congadd 39556	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
50	38, 41, 43, 45, 46, 47, 48, 49	syl322anc 1394	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
51	39	ffnd 6510	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏 Fn (ℤ ↑_m 𝑉))
52	44	ffnd 6510	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐 Fn (ℤ ↑_m 𝑉))
53		ovexd 7185	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (ℤ ↑_m 𝑉) ∈ V)
54		fnfvof 7417	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f + 𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋)))
55	51, 52, 53, 40, 54	syl22anc 836	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f + 𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋)))
56		fnfvof 7417	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f + 𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌)))
57	51, 52, 53, 42, 56	syl22anc 836	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f + 𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌)))
58	55, 57	oveq12d 7168	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)) = (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
59	50, 58	breqtrrd 5087	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
60		congmul 39557	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
61	38, 41, 43, 45, 46, 47, 48, 60	syl322anc 1394	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
62		fnfvof 7417	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f · 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋)))
63	51, 52, 53, 40, 62	syl22anc 836	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f · 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋)))
64		fnfvof 7417	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f · 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌)))
65	51, 52, 53, 42, 64	syl22anc 836	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f · 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌)))
66	63, 65	oveq12d 7168	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)) = (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
67	61, 66	breqtrrd 5087	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
68		fveq1 6664	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑋) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋))
69		fveq1 6664	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑌) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))
70	68, 69	oveq12d 7168	. . . 4 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
71	70	breq2d 5071	. . 3 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))))
72		fveq1 6664	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑋) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋))
73		fveq1 6664	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑌) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))
74	72, 73	oveq12d 7168	. . . 4 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
75	74	breq2d 5071	. . 3 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))))
76		fveq1 6664	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑋) = (𝑏‘𝑋))
77		fveq1 6664	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑌) = (𝑏‘𝑌))
78	76, 77	oveq12d 7168	. . . 4 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑏‘𝑋) − (𝑏‘𝑌)))
79	78	breq2d 5071	. . 3 ⊢ (𝑎 = 𝑏 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))))
80		fveq1 6664	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑋) = (𝑐‘𝑋))
81		fveq1 6664	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑌) = (𝑐‘𝑌))
82	80, 81	oveq12d 7168	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑐‘𝑋) − (𝑐‘𝑌)))
83	82	breq2d 5071	. . 3 ⊢ (𝑎 = 𝑐 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌))))
84		fveq1 6664	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f + 𝑐)‘𝑋))
85		fveq1 6664	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f + 𝑐)‘𝑌))
86	84, 85	oveq12d 7168	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
87	86	breq2d 5071	. . 3 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌))))
88		fveq1 6664	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f · 𝑐)‘𝑋))
89		fveq1 6664	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f · 𝑐)‘𝑌))
90	88, 89	oveq12d 7168	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
91	90	breq2d 5071	. . 3 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌))))
92		fveq1 6664	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑋) = (𝐹‘𝑋))
93		fveq1 6664	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑌) = (𝐹‘𝑌))
94	92, 93	oveq12d 7168	. . . 4 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝐹‘𝑋) − (𝐹‘𝑌)))
95	94	breq2d 5071	. . 3 ⊢ (𝑎 = 𝐹 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))))
96	16, 37, 59, 67, 71, 75, 79, 83, 87, 91, 95	mzpindd 39336	. 2 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝐹 ∈ (mzPoly‘𝑉)) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))
97	2, 3, 96	syl2anc 586	1 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∀wral 3138 Vcvv 3495 {csn 4561 class class class wbr 5059 ↦ cmpt 5139 × cxp 5548 Fn wfn 6345 ⟶wf 6346 ‘cfv 6350 (class class class)co 7150 ∘_f cof 7401 ↑_m cmap 8400 + caddc 10534 · cmul 10536 − cmin 10864 ℤcz 11975 ∥ cdvds 15601 mzPolycmzp 39312

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-int 4870 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-of 7403 df-om 7575 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-er 8283 df-map 8402 df-en 8504 df-dom 8505 df-sdom 8506 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-nn 11633 df-n0 11892 df-z 11976 df-dvds 15602 df-mzpcl 39313 df-mzp 39314

This theorem is referenced by: (None)

W3C validator