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 42989

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 6943	. . 3 ⊢ (𝐹 ∈ (mzPoly‘𝑉) → 𝑉 ∈ V)
2	1	3anim1i 1152	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → (𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))))
3		simp1 1136	. 2 ⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝐹 ∈ (mzPoly‘𝑉))
4		simpl3l 1228	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
5		simpr 484	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
6		congid 42988	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
7	4, 5, 6	syl2anc 584	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏))
8		simpl2l 1226	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈ (ℤ ↑_m 𝑉))
9		vex 3483	. . . . . . 7 ⊢ 𝑏 ∈ V
10	9	fvconst2 7225	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
11	8, 10	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) = 𝑏)
12		simpl2r 1227	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑌 ∈ (ℤ ↑_m 𝑉))
13	9	fvconst2 7225	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
14	12, 13	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌) = 𝑏)
15	11, 14	oveq12d 7450	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)) = (𝑏 − 𝑏))
16	7, 15	breqtrrd 5170	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
17		simpr 484	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉)
18		simpl3r 1229	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))
19		fveq2 6905	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑋‘𝑘) = (𝑋‘𝑏))
20		fveq2 6905	. . . . . . . 8 ⊢ (𝑘 = 𝑏 → (𝑌‘𝑘) = (𝑌‘𝑏))
21	19, 20	oveq12d 7450	. . . . . . 7 ⊢ (𝑘 = 𝑏 → ((𝑋‘𝑘) − (𝑌‘𝑘)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
22	21	breq2d 5154	. . . . . 6 ⊢ (𝑘 = 𝑏 → (𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)) ↔ 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏))))
23	22	rspcva 3619	. . . . 5 ⊢ ((𝑏 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘))) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
24	17, 18, 23	syl2anc 584	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))
25		simpl2l 1226	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑋 ∈ (ℤ ↑_m 𝑉))
26		fveq1 6904	. . . . . . 7 ⊢ (𝑐 = 𝑋 → (𝑐‘𝑏) = (𝑋‘𝑏))
27		eqid 2736	. . . . . . 7 ⊢ (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))
28		fvex 6918	. . . . . . 7 ⊢ (𝑋‘𝑏) ∈ V
29	26, 27, 28	fvmpt 7015	. . . . . 6 ⊢ (𝑋 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
30	25, 29	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏))
31		simpl2r 1227	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑌 ∈ (ℤ ↑_m 𝑉))
32		fveq1 6904	. . . . . . 7 ⊢ (𝑐 = 𝑌 → (𝑐‘𝑏) = (𝑌‘𝑏))
33		fvex 6918	. . . . . . 7 ⊢ (𝑌‘𝑏) ∈ V
34	32, 27, 33	fvmpt 7015	. . . . . 6 ⊢ (𝑌 ∈ (ℤ ↑_m 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
35	31, 34	syl 17	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏))
36	30, 35	oveq12d 7450	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)) = ((𝑋‘𝑏) − (𝑌‘𝑏)))
37	24, 36	breqtrrd 5170	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
38		simp13l 1288	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∈ ℤ)
39		simp2l 1199	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏:(ℤ ↑_m 𝑉)⟶ℤ)
40		simp12l 1286	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑋 ∈ (ℤ ↑_m 𝑉))
41	39, 40	ffvelcdmd 7104	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑋) ∈ ℤ)
42		simp12r 1287	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑌 ∈ (ℤ ↑_m 𝑉))
43	39, 42	ffvelcdmd 7104	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑌) ∈ ℤ)
44		simp3l 1201	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐:(ℤ ↑_m 𝑉)⟶ℤ)
45	44, 40	ffvelcdmd 7104	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑋) ∈ ℤ)
46	44, 42	ffvelcdmd 7104	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑌) ∈ ℤ)
47		simp2r 1200	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)))
48		simp3r 1202	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))
49		congadd 42983	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
50	38, 41, 43, 45, 46, 47, 48, 49	syl322anc 1399	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
51	39	ffnd 6736	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏 Fn (ℤ ↑_m 𝑉))
52	44	ffnd 6736	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐 Fn (ℤ ↑_m 𝑉))
53		ovexd 7467	. . . . . 6 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (ℤ ↑_m 𝑉) ∈ V)
54		fnfvof 7715	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f + 𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋)))
55	51, 52, 53, 40, 54	syl22anc 838	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f + 𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋)))
56		fnfvof 7715	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f + 𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌)))
57	51, 52, 53, 42, 56	syl22anc 838	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f + 𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌)))
58	55, 57	oveq12d 7450	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)) = (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌))))
59	50, 58	breqtrrd 5170	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
60		congmul 42984	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
61	38, 41, 43, 45, 46, 47, 48, 60	syl322anc 1399	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
62		fnfvof 7715	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f · 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋)))
63	51, 52, 53, 40, 62	syl22anc 838	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f · 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋)))
64		fnfvof 7715	. . . . . 6 ⊢ (((𝑏 Fn (ℤ ↑_m 𝑉) ∧ 𝑐 Fn (ℤ ↑_m 𝑉)) ∧ ((ℤ ↑_m 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑_m 𝑉))) → ((𝑏 ∘_f · 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌)))
65	51, 52, 53, 42, 64	syl22anc 838	. . . . 5 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘_f · 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌)))
66	63, 65	oveq12d 7450	. . . 4 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)) = (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌))))
67	61, 66	breqtrrd 5170	. . 3 ⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑_m 𝑉) ∧ 𝑌 ∈ (ℤ ↑_m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑_m 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
68		fveq1 6904	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑋) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑋))
69		fveq1 6904	. . . . 5 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑎‘𝑌) = (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))
70	68, 69	oveq12d 7450	. . . 4 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌)))
71	70	breq2d 5154	. . 3 ⊢ (𝑎 = ((ℤ ↑_m 𝑉) × {𝑏}) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((((ℤ ↑_m 𝑉) × {𝑏})‘𝑋) − (((ℤ ↑_m 𝑉) × {𝑏})‘𝑌))))
72		fveq1 6904	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑋) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋))
73		fveq1 6904	. . . . 5 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑌) = ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))
74	72, 73	oveq12d 7450	. . . 4 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌)))
75	74	breq2d 5154	. . 3 ⊢ (𝑎 = (𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏)) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑_m 𝑉) ↦ (𝑐‘𝑏))‘𝑌))))
76		fveq1 6904	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑋) = (𝑏‘𝑋))
77		fveq1 6904	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑌) = (𝑏‘𝑌))
78	76, 77	oveq12d 7450	. . . 4 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑏‘𝑋) − (𝑏‘𝑌)))
79	78	breq2d 5154	. . 3 ⊢ (𝑎 = 𝑏 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))))
80		fveq1 6904	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑋) = (𝑐‘𝑋))
81		fveq1 6904	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝑎‘𝑌) = (𝑐‘𝑌))
82	80, 81	oveq12d 7450	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑐‘𝑋) − (𝑐‘𝑌)))
83	82	breq2d 5154	. . 3 ⊢ (𝑎 = 𝑐 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌))))
84		fveq1 6904	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f + 𝑐)‘𝑋))
85		fveq1 6904	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f + 𝑐)‘𝑌))
86	84, 85	oveq12d 7450	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌)))
87	86	breq2d 5154	. . 3 ⊢ (𝑎 = (𝑏 ∘_f + 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f + 𝑐)‘𝑋) − ((𝑏 ∘_f + 𝑐)‘𝑌))))
88		fveq1 6904	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘_f · 𝑐)‘𝑋))
89		fveq1 6904	. . . . 5 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘_f · 𝑐)‘𝑌))
90	88, 89	oveq12d 7450	. . . 4 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌)))
91	90	breq2d 5154	. . 3 ⊢ (𝑎 = (𝑏 ∘_f · 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘_f · 𝑐)‘𝑋) − ((𝑏 ∘_f · 𝑐)‘𝑌))))
92		fveq1 6904	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑋) = (𝐹‘𝑋))
93		fveq1 6904	. . . . 5 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑌) = (𝐹‘𝑌))
94	92, 93	oveq12d 7450	. . . 4 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝐹‘𝑋) − (𝐹‘𝑌)))
95	94	breq2d 5154	. . 3 ⊢ (𝑎 = 𝐹 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))))
96	16, 37, 59, 67, 71, 75, 79, 83, 87, 91, 95	mzpindd 42762	. 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 1539 ∈ wcel 2107 ∀wral 3060 Vcvv 3479 {csn 4625 class class class wbr 5142 ↦ cmpt 5224 × cxp 5682 Fn wfn 6555 ⟶wf 6556 ‘cfv 6560 (class class class)co 7432 ∘_f cof 7696 ↑_m cmap 8867 + caddc 11159 · cmul 11161 − cmin 11493 ℤcz 12615 ∥ cdvds 16291 mzPolycmzp 42738

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-of 7698 df-om 7889 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-er 8746 df-map 8869 df-en 8987 df-dom 8988 df-sdom 8989 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-nn 12268 df-n0 12529 df-z 12616 df-dvds 16292 df-mzpcl 42739 df-mzp 42740

This theorem is referenced by: (None)

W3C validator