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 43497

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 6891	. . 3 ⊢ (𝐹 ∈ (mzPoly‘𝑉) → 𝑉 ∈ V)
2	1	3anim1i 1161	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → (𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))))
3		simp1 1145	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝐹 ∈ (mzPoly‘𝑉))
4		simpl3l 1238	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
5		simpr 487	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
6		congid 43496	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
7	4, 5, 6	syl2anc 592	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
8		simpl2l 1236	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈ (ℤ ↑_m 𝑉))
9		vex 3452	. . . . . . 7 ⊢ 𝑏 ∈ V
10	9	fvconst2 7177	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
11	8, 10	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
12		simpl2r 1237	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑌 ∈ (ℤ ↑_m 𝑉))
13	9	fvconst2 7177	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
14	12, 13	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
15	11, 14	oveq12d 7403	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)) = (𝑏 − 𝑏))
16	7, 15	breqtrrd 5122	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
17		simpr 487	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉)
18		simpl3r 1239	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))
19		fveq2 6856	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑋‘𝑘) = (𝑋‘𝑏))
20		fveq2 6856	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑌‘𝑘) = (𝑌‘𝑏))
21	19, 20	oveq12d 7403	. . . . . . 7 ⊢ (𝑘 = 𝑏 → ((𝑋‘𝑘) − (𝑌‘𝑘)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
22	21	breq2d 5106	. . . . . 6 ⊢ (𝑘 = 𝑏 → (𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)) ↔ 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏))))
23	22	rspcva 3574	. . . . 5 ⊢ ((𝑏 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘))) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
24	17, 18, 23	syl2anc 592	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
25		simpl2l 1236	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑋 ∈ (ℤ ↑_m 𝑉))
26		fveq1 6855	. . . . . . 7 ⊢ (𝑐 = 𝑋 → (𝑐‘𝑏) = (𝑋‘𝑏))
27		eqid 2756	. . . . . . 7 ⊢ (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))
28		fvex 6869	. . . . . . 7 ⊢ (𝑋‘𝑏) ∈ V
29	26, 27, 28	fvmpt 6964	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
30	25, 29	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
31		simpl2r 1237	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑌 ∈ (ℤ ↑_m 𝑉))
32		fveq1 6855	. . . . . . 7 ⊢ (𝑐 = 𝑌 → (𝑐‘𝑏) = (𝑌‘𝑏))
33		fvex 6869	. . . . . . 7 ⊢ (𝑌‘𝑏) ∈ V
34	32, 27, 33	fvmpt 6964	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
35	31, 34	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
36	30, 35	oveq12d 7403	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
37	24, 36	breqtrrd 5122	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
38		simp13l 1298	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∈ ℤ)
39		simp2l 1209	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏:(ℤ ↑_m 𝑉)⟶ℤ)
40		simp12l 1296	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑋 ∈ (ℤ ↑_m 𝑉))
41	39, 40	ffvelcdmd 7055	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑋) ∈ ℤ)
42		simp12r 1297	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑌 ∈ (ℤ ↑_m 𝑉))
43	39, 42	ffvelcdmd 7055	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑌) ∈ ℤ)
44		simp3l 1211	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐:(ℤ ↑_m 𝑉)⟶ℤ)
45	44, 40	ffvelcdmd 7055	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑋) ∈ ℤ)
46	44, 42	ffvelcdmd 7055	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑌) ∈ ℤ)
47		simp2r 1210	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)))
48		simp3r 1212	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))
49		congadd 43491	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
50	38, 41, 43, 45, 46, 47, 48, 49	syl322anc 1413	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
51	39	ffnd 6681	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏 Fn (ℤ ↑_m 𝑉))
52	44	ffnd 6681	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐 Fn (ℤ ↑_m 𝑉))
53		ovexd 7420	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (ℤ ↑_m 𝑉) ∈ V)
54		fnfvof 7666	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f + 𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋)))
55	51, 52, 53, 40, 54	syl22anc 847	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f + 𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋)))
56		fnfvof 7666	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f + 𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌)))
57	51, 52, 53, 42, 56	syl22anc 847	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f + 𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌)))
58	55, 57	oveq12d 7403	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)) = (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
59	50, 58	breqtrrd 5122	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
60		congmul 43492	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
61	38, 41, 43, 45, 46, 47, 48, 60	syl322anc 1413	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
62		fnfvof 7666	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f · 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋)))
63	51, 52, 53, 40, 62	syl22anc 847	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f · 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋)))
64		fnfvof 7666	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f · 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌)))
65	51, 52, 53, 42, 64	syl22anc 847	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f · 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌)))
66	63, 65	oveq12d 7403	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)) = (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
67	61, 66	breqtrrd 5122	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
68		fveq1 6855	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑋) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋))
69		fveq1 6855	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑌) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))
70	68, 69	oveq12d 7403	. . . 4 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
71	70	breq2d 5106	. . 3 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))))
72		fveq1 6855	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑋) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋))
73		fveq1 6855	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑌) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))
74	72, 73	oveq12d 7403	. . . 4 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
75	74	breq2d 5106	. . 3 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))))
76		fveq1 6855	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑋) = (𝑏‘𝑋))
77		fveq1 6855	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑌) = (𝑏‘𝑌))
78	76, 77	oveq12d 7403	. . . 4 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑏‘𝑋) − (𝑏‘𝑌)))
79	78	breq2d 5106	. . 3 ⊢ (𝑎 = 𝑏 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))))
80		fveq1 6855	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑋) = (𝑐‘𝑋))
81		fveq1 6855	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑌) = (𝑐‘𝑌))
82	80, 81	oveq12d 7403	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑐‘𝑋) − (𝑐‘𝑌)))
83	82	breq2d 5106	. . 3 ⊢ (𝑎 = 𝑐 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌))))
84		fveq1 6855	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f + 𝑐)‘𝑋))
85		fveq1 6855	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f + 𝑐)‘𝑌))
86	84, 85	oveq12d 7403	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
87	86	breq2d 5106	. . 3 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌))))
88		fveq1 6855	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f · 𝑐)‘𝑋))
89		fveq1 6855	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f · 𝑐)‘𝑌))
90	88, 89	oveq12d 7403	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
91	90	breq2d 5106	. . 3 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌))))
92		fveq1 6855	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑋) = (𝐹‘𝑋))
93		fveq1 6855	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑌) = (𝐹‘𝑌))
94	92, 93	oveq12d 7403	. . . 4 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝐹‘𝑋) − (𝐹‘𝑌)))
95	94	breq2d 5106	. . 3 ⊢ (𝑎 = 𝐹 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))))
96	16, 37, 59, 67, 71, 75, 79, 83, 87, 91, 95	mzpindd 43275	. 2 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝐹 ∈ (mzPoly‘𝑉)) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))
97	2, 3, 96	syl2anc 592	1 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1095 = wceq 1554 ∈ wcel 2136 ∀wral 3070 Vcvv 3448 {csn 4576 class class class wbr 5094 ↦ cmpt 5175 × cxp 5638 Fn wfn 6505 ⟶wf 6506 ‘cfv 6510 (class class class)co 7385 ∘_f cof 7647 ↑_m cmap 8796 + caddc 11066 · cmul 11068 − cmin 11404 ℤcz 12558 ∥ cdvds 16262 mzPolycmzp 43251

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1809 ax-4 1823 ax-5 1924 ax-6 1981 ax-7 2022 ax-8 2138 ax-9 2146 ax-10 2169 ax-11 2185 ax-12 2206 ax-ext 2728 ax-rep 5221 ax-sep 5240 ax-nul 5250 ax-pow 5316 ax-pr 5384 ax-un 7707 ax-cnex 11119 ax-resscn 11120 ax-1cn 11121 ax-icn 11122 ax-addcl 11123 ax-addrcl 11124 ax-mulcl 11125 ax-mulrcl 11126 ax-mulcom 11127 ax-addass 11128 ax-mulass 11129 ax-distr 11130 ax-i2m1 11131 ax-1ne0 11132 ax-1rid 11133 ax-rnegex 11134 ax-rrecex 11135 ax-cnre 11136 ax-pre-lttri 11137 ax-pre-lttrn 11138 ax-pre-ltadd 11139 ax-pre-mulgt0 11140

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1557 df-fal 1567 df-ex 1794 df-nf 1798 df-sb 2085 df-mo 2560 df-eu 2590 df-clab 2735 df-cleq 2748 df-clel 2831 df-nfc 2905 df-ne 2952 df-nel 3056 df-ral 3071 df-rex 3081 df-reu 3362 df-rab 3409 df-v 3450 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4281 df-if 4475 df-pw 4551 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-int 4900 df-iun 4945 df-br 5095 df-opab 5157 df-mpt 5176 df-tr 5202 df-id 5535 df-eprel 5540 df-po 5548 df-so 5549 df-fr 5593 df-we 5595 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6466 df-fun 6512 df-fn 6513 df-f 6514 df-f1 6515 df-fo 6516 df-f1o 6517 df-fv 6518 df-riota 7342 df-ov 7388 df-oprab 7389 df-mpo 7390 df-of 7649 df-om 7836 df-2nd 7960 df-frecs 8250 df-wrecs 8281 df-recs 8330 df-rdg 8369 df-er 8666 df-map 8798 df-en 8917 df-dom 8918 df-sdom 8919 df-pnf 11208 df-mnf 11209 df-xr 11210 df-ltxr 11211 df-le 11212 df-sub 11406 df-neg 11407 df-nn 12201 df-n0 12472 df-z 12559 df-dvds 16263 df-mzpcl 43252 df-mzp 43253

This theorem is referenced by: (None)

W3C validator