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 42961

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 6945	. . 3 ⊢ (𝐹 ∈ (mzPoly‘𝑉) → 𝑉 ∈ V)
2	1	3anim1i 1151	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → (𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))))
3		simp1 1135	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝐹 ∈ (mzPoly‘𝑉))
4		simpl3l 1227	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
5		simpr 484	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
6		congid 42960	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
7	4, 5, 6	syl2anc 584	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
8		simpl2l 1225	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈ (ℤ ↑_m 𝑉))
9		vex 3482	. . . . . . 7 ⊢ 𝑏 ∈ V
10	9	fvconst2 7224	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
11	8, 10	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
12		simpl2r 1226	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑌 ∈ (ℤ ↑_m 𝑉))
13	9	fvconst2 7224	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
14	12, 13	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
15	11, 14	oveq12d 7449	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)) = (𝑏 − 𝑏))
16	7, 15	breqtrrd 5176	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
17		simpr 484	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉)
18		simpl3r 1228	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))
19		fveq2 6907	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑋‘𝑘) = (𝑋‘𝑏))
20		fveq2 6907	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑌‘𝑘) = (𝑌‘𝑏))
21	19, 20	oveq12d 7449	. . . . . . 7 ⊢ (𝑘 = 𝑏 → ((𝑋‘𝑘) − (𝑌‘𝑘)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
22	21	breq2d 5160	. . . . . 6 ⊢ (𝑘 = 𝑏 → (𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)) ↔ 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏))))
23	22	rspcva 3620	. . . . 5 ⊢ ((𝑏 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘))) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
24	17, 18, 23	syl2anc 584	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
25		simpl2l 1225	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑋 ∈ (ℤ ↑_m 𝑉))
26		fveq1 6906	. . . . . . 7 ⊢ (𝑐 = 𝑋 → (𝑐‘𝑏) = (𝑋‘𝑏))
27		eqid 2735	. . . . . . 7 ⊢ (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))
28		fvex 6920	. . . . . . 7 ⊢ (𝑋‘𝑏) ∈ V
29	26, 27, 28	fvmpt 7016	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
30	25, 29	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
31		simpl2r 1226	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑌 ∈ (ℤ ↑_m 𝑉))
32		fveq1 6906	. . . . . . 7 ⊢ (𝑐 = 𝑌 → (𝑐‘𝑏) = (𝑌‘𝑏))
33		fvex 6920	. . . . . . 7 ⊢ (𝑌‘𝑏) ∈ V
34	32, 27, 33	fvmpt 7016	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
35	31, 34	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
36	30, 35	oveq12d 7449	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
37	24, 36	breqtrrd 5176	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
38		simp13l 1287	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∈ ℤ)
39		simp2l 1198	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏:(ℤ ↑_m 𝑉)⟶ℤ)
40		simp12l 1285	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑋 ∈ (ℤ ↑_m 𝑉))
41	39, 40	ffvelcdmd 7105	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑋) ∈ ℤ)
42		simp12r 1286	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑌 ∈ (ℤ ↑_m 𝑉))
43	39, 42	ffvelcdmd 7105	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑌) ∈ ℤ)
44		simp3l 1200	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐:(ℤ ↑_m 𝑉)⟶ℤ)
45	44, 40	ffvelcdmd 7105	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑋) ∈ ℤ)
46	44, 42	ffvelcdmd 7105	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑌) ∈ ℤ)
47		simp2r 1199	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)))
48		simp3r 1201	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))
49		congadd 42955	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
50	38, 41, 43, 45, 46, 47, 48, 49	syl322anc 1397	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
51	39	ffnd 6738	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏 Fn (ℤ ↑_m 𝑉))
52	44	ffnd 6738	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐 Fn (ℤ ↑_m 𝑉))
53		ovexd 7466	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (ℤ ↑_m 𝑉) ∈ V)
54		fnfvof 7714	. . . . . 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 7714	. . . . . 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 7449	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)) = (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
59	50, 58	breqtrrd 5176	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
60		congmul 42956	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
61	38, 41, 43, 45, 46, 47, 48, 60	syl322anc 1397	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
62		fnfvof 7714	. . . . . 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 7714	. . . . . 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 7449	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)) = (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
67	61, 66	breqtrrd 5176	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
68		fveq1 6906	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑋) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋))
69		fveq1 6906	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑌) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))
70	68, 69	oveq12d 7449	. . . 4 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
71	70	breq2d 5160	. . 3 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))))
72		fveq1 6906	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑋) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋))
73		fveq1 6906	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑌) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))
74	72, 73	oveq12d 7449	. . . 4 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
75	74	breq2d 5160	. . 3 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))))
76		fveq1 6906	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑋) = (𝑏‘𝑋))
77		fveq1 6906	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑌) = (𝑏‘𝑌))
78	76, 77	oveq12d 7449	. . . 4 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑏‘𝑋) − (𝑏‘𝑌)))
79	78	breq2d 5160	. . 3 ⊢ (𝑎 = 𝑏 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))))
80		fveq1 6906	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑋) = (𝑐‘𝑋))
81		fveq1 6906	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑌) = (𝑐‘𝑌))
82	80, 81	oveq12d 7449	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑐‘𝑋) − (𝑐‘𝑌)))
83	82	breq2d 5160	. . 3 ⊢ (𝑎 = 𝑐 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌))))
84		fveq1 6906	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f + 𝑐)‘𝑋))
85		fveq1 6906	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f + 𝑐)‘𝑌))
86	84, 85	oveq12d 7449	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
87	86	breq2d 5160	. . 3 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌))))
88		fveq1 6906	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f · 𝑐)‘𝑋))
89		fveq1 6906	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f · 𝑐)‘𝑌))
90	88, 89	oveq12d 7449	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
91	90	breq2d 5160	. . 3 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌))))
92		fveq1 6906	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑋) = (𝐹‘𝑋))
93		fveq1 6906	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑌) = (𝐹‘𝑌))
94	92, 93	oveq12d 7449	. . . 4 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝐹‘𝑋) − (𝐹‘𝑌)))
95	94	breq2d 5160	. . 3 ⊢ (𝑎 = 𝐹 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))))
96	16, 37, 59, 67, 71, 75, 79, 83, 87, 91, 95	mzpindd 42734	. 2 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝐹 ∈ (mzPoly‘𝑉)) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))
97	2, 3, 96	syl2anc 584	1 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ∀wral 3059 Vcvv 3478 {csn 4631 class class class wbr 5148 ↦ cmpt 5231 × cxp 5687 Fn wfn 6558 ⟶wf 6559 ‘cfv 6563 (class class class)co 7431 ∘_f cof 7695 ↑_m cmap 8865 + caddc 11156 · cmul 11158 − cmin 11490 ℤcz 12611 ∥ cdvds 16287 mzPolycmzp 42710

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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-er 8744 df-map 8867 df-en 8985 df-dom 8986 df-sdom 8987 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-nn 12265 df-n0 12525 df-z 12612 df-dvds 16288 df-mzpcl 42711 df-mzp 42712

This theorem is referenced by: (None)

W3C validator