Step | Hyp | Ref
| Expression |
1 | | elfvex 6131 |
. . 3
⊢ (𝐹 ∈ (mzPoly‘𝑉) → 𝑉 ∈ V) |
2 | 1 | 3anim1i 1241 |
. 2
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑𝑚
𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → (𝑉 ∈ V ∧ (𝑋 ∈ (ℤ ↑𝑚
𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘))))) |
3 | | simp1 1054 |
. 2
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑𝑚
𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝐹 ∈ (mzPoly‘𝑉)) |
4 | | simpl3l 1109 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ) |
5 | | simpr 476 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ) |
6 | | congid 36556 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏)) |
7 | 4, 5, 6 | syl2anc 691 |
. . . 4
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ (𝑏 − 𝑏)) |
8 | | simpl2l 1107 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈ (ℤ ↑𝑚
𝑉)) |
9 | | vex 3176 |
. . . . . . 7
⊢ 𝑏 ∈ V |
10 | 9 | fvconst2 6374 |
. . . . . 6
⊢ (𝑋 ∈ (ℤ
↑𝑚 𝑉) → (((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑋) = 𝑏) |
11 | 8, 10 | syl 17 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑋) = 𝑏) |
12 | | simpl2r 1108 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑌 ∈ (ℤ ↑𝑚
𝑉)) |
13 | 9 | fvconst2 6374 |
. . . . . 6
⊢ (𝑌 ∈ (ℤ
↑𝑚 𝑉) → (((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑌) = 𝑏) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → (((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑌) = 𝑏) |
15 | 11, 14 | oveq12d 6567 |
. . . 4
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → ((((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑋) − (((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑌)) = (𝑏 − 𝑏)) |
16 | 7, 15 | breqtrrd 4611 |
. . 3
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ ℤ) → 𝑁 ∥ ((((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑋) − (((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑌))) |
17 | | simpr 476 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉) |
18 | | simpl3r 1110 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘))) |
19 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝑏 → (𝑋‘𝑘) = (𝑋‘𝑏)) |
20 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝑏 → (𝑌‘𝑘) = (𝑌‘𝑏)) |
21 | 19, 20 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = 𝑏 → ((𝑋‘𝑘) − (𝑌‘𝑘)) = ((𝑋‘𝑏) − (𝑌‘𝑏))) |
22 | 21 | breq2d 4595 |
. . . . . 6
⊢ (𝑘 = 𝑏 → (𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)) ↔ 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏)))) |
23 | 22 | rspcva 3280 |
. . . . 5
⊢ ((𝑏 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘))) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏))) |
24 | 17, 18, 23 | syl2anc 691 |
. . . 4
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ ((𝑋‘𝑏) − (𝑌‘𝑏))) |
25 | | simpl2l 1107 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑋 ∈ (ℤ ↑𝑚
𝑉)) |
26 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑐 = 𝑋 → (𝑐‘𝑏) = (𝑋‘𝑏)) |
27 | | eqid 2610 |
. . . . . . 7
⊢ (𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) |
28 | | fvex 6113 |
. . . . . . 7
⊢ (𝑋‘𝑏) ∈ V |
29 | 26, 27, 28 | fvmpt 6191 |
. . . . . 6
⊢ (𝑋 ∈ (ℤ
↑𝑚 𝑉) → ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏)) |
30 | 25, 29 | syl 17 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑋) = (𝑋‘𝑏)) |
31 | | simpl2r 1108 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑌 ∈ (ℤ ↑𝑚
𝑉)) |
32 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑐 = 𝑌 → (𝑐‘𝑏) = (𝑌‘𝑏)) |
33 | | fvex 6113 |
. . . . . . 7
⊢ (𝑌‘𝑏) ∈ V |
34 | 32, 27, 33 | fvmpt 6191 |
. . . . . 6
⊢ (𝑌 ∈ (ℤ
↑𝑚 𝑉) → ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏)) |
35 | 31, 34 | syl 17 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑌) = (𝑌‘𝑏)) |
36 | 30, 35 | oveq12d 6567 |
. . . 4
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → (((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑌)) = ((𝑋‘𝑏) − (𝑌‘𝑏))) |
37 | 24, 36 | breqtrrd 4611 |
. . 3
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝑏 ∈ 𝑉) → 𝑁 ∥ (((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑌))) |
38 | | simp13l 1169 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∈ ℤ) |
39 | | simp2l 1080 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ) |
40 | | simp12l 1167 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑋 ∈ (ℤ ↑𝑚
𝑉)) |
41 | 39, 40 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑋) ∈ ℤ) |
42 | | simp12r 1168 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑌 ∈ (ℤ ↑𝑚
𝑉)) |
43 | 39, 42 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑏‘𝑌) ∈ ℤ) |
44 | | simp3l 1082 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ) |
45 | 44, 40 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑋) ∈ ℤ) |
46 | 44, 42 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (𝑐‘𝑌) ∈ ℤ) |
47 | | simp2r 1081 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) |
48 | | simp3r 1083 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌))) |
49 | | congadd 36551 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌)))) |
50 | 38, 41, 43, 45, 46, 47, 48, 49 | syl322anc 1346 |
. . . 4
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌)))) |
51 | | ffn 5958 |
. . . . . . 7
⊢ (𝑏:(ℤ
↑𝑚 𝑉)⟶ℤ → 𝑏 Fn (ℤ ↑𝑚 𝑉)) |
52 | 39, 51 | syl 17 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑏 Fn (ℤ ↑𝑚 𝑉)) |
53 | | ffn 5958 |
. . . . . . 7
⊢ (𝑐:(ℤ
↑𝑚 𝑉)⟶ℤ → 𝑐 Fn (ℤ ↑𝑚 𝑉)) |
54 | 44, 53 | syl 17 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑐 Fn (ℤ ↑𝑚 𝑉)) |
55 | | ovex 6577 |
. . . . . . 7
⊢ (ℤ
↑𝑚 𝑉) ∈ V |
56 | 55 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (ℤ
↑𝑚 𝑉) ∈ V) |
57 | | fnfvof 6809 |
. . . . . 6
⊢ (((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ ((ℤ
↑𝑚 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑𝑚
𝑉))) → ((𝑏 ∘𝑓 +
𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋))) |
58 | 52, 54, 56, 40, 57 | syl22anc 1319 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘𝑓 + 𝑐)‘𝑋) = ((𝑏‘𝑋) + (𝑐‘𝑋))) |
59 | | fnfvof 6809 |
. . . . . 6
⊢ (((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ ((ℤ
↑𝑚 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉))) → ((𝑏 ∘𝑓 +
𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌))) |
60 | 52, 54, 56, 42, 59 | syl22anc 1319 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘𝑓 + 𝑐)‘𝑌) = ((𝑏‘𝑌) + (𝑐‘𝑌))) |
61 | 58, 60 | oveq12d 6567 |
. . . 4
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘𝑓 + 𝑐)‘𝑋) − ((𝑏 ∘𝑓 + 𝑐)‘𝑌)) = (((𝑏‘𝑋) + (𝑐‘𝑋)) − ((𝑏‘𝑌) + (𝑐‘𝑌)))) |
62 | 50, 61 | breqtrrd 4611 |
. . 3
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘𝑓 + 𝑐)‘𝑋) − ((𝑏 ∘𝑓 + 𝑐)‘𝑌))) |
63 | | congmul 36552 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ (𝑏‘𝑋) ∈ ℤ ∧ (𝑏‘𝑌) ∈ ℤ) ∧ ((𝑐‘𝑋) ∈ ℤ ∧ (𝑐‘𝑌) ∈ ℤ) ∧ (𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)) ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌)))) |
64 | 38, 41, 43, 45, 46, 47, 48, 63 | syl322anc 1346 |
. . . 4
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌)))) |
65 | | fnfvof 6809 |
. . . . . 6
⊢ (((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ ((ℤ
↑𝑚 𝑉) ∈ V ∧ 𝑋 ∈ (ℤ ↑𝑚
𝑉))) → ((𝑏 ∘𝑓
· 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋))) |
66 | 52, 54, 56, 40, 65 | syl22anc 1319 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘𝑓 · 𝑐)‘𝑋) = ((𝑏‘𝑋) · (𝑐‘𝑋))) |
67 | | fnfvof 6809 |
. . . . . 6
⊢ (((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ ((ℤ
↑𝑚 𝑉) ∈ V ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉))) → ((𝑏 ∘𝑓
· 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌))) |
68 | 52, 54, 56, 42, 67 | syl22anc 1319 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → ((𝑏 ∘𝑓 · 𝑐)‘𝑌) = ((𝑏‘𝑌) · (𝑐‘𝑌))) |
69 | 66, 68 | oveq12d 6567 |
. . . 4
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → (((𝑏 ∘𝑓 · 𝑐)‘𝑋) − ((𝑏 ∘𝑓 · 𝑐)‘𝑌)) = (((𝑏‘𝑋) · (𝑐‘𝑋)) − ((𝑏‘𝑌) · (𝑐‘𝑌)))) |
70 | 64, 69 | breqtrrd 4611 |
. . 3
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌))) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) → 𝑁 ∥ (((𝑏 ∘𝑓 · 𝑐)‘𝑋) − ((𝑏 ∘𝑓 · 𝑐)‘𝑌))) |
71 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = ((ℤ
↑𝑚 𝑉) × {𝑏}) → (𝑎‘𝑋) = (((ℤ ↑𝑚
𝑉) × {𝑏})‘𝑋)) |
72 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = ((ℤ
↑𝑚 𝑉) × {𝑏}) → (𝑎‘𝑌) = (((ℤ ↑𝑚
𝑉) × {𝑏})‘𝑌)) |
73 | 71, 72 | oveq12d 6567 |
. . . 4
⊢ (𝑎 = ((ℤ
↑𝑚 𝑉) × {𝑏}) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((((ℤ ↑𝑚
𝑉) × {𝑏})‘𝑋) − (((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑌))) |
74 | 73 | breq2d 4595 |
. . 3
⊢ (𝑎 = ((ℤ
↑𝑚 𝑉) × {𝑏}) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑋) − (((ℤ
↑𝑚 𝑉) × {𝑏})‘𝑌)))) |
75 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑋) = ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑋)) |
76 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘𝑌) = ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑌)) |
77 | 75, 76 | oveq12d 6567 |
. . . 4
⊢ (𝑎 = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑌))) |
78 | 77 | breq2d 4595 |
. . 3
⊢ (𝑎 = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑋) − ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘𝑌)))) |
79 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = 𝑏 → (𝑎‘𝑋) = (𝑏‘𝑋)) |
80 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = 𝑏 → (𝑎‘𝑌) = (𝑏‘𝑌)) |
81 | 79, 80 | oveq12d 6567 |
. . . 4
⊢ (𝑎 = 𝑏 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑏‘𝑋) − (𝑏‘𝑌))) |
82 | 81 | breq2d 4595 |
. . 3
⊢ (𝑎 = 𝑏 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑏‘𝑋) − (𝑏‘𝑌)))) |
83 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = 𝑐 → (𝑎‘𝑋) = (𝑐‘𝑋)) |
84 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = 𝑐 → (𝑎‘𝑌) = (𝑐‘𝑌)) |
85 | 83, 84 | oveq12d 6567 |
. . . 4
⊢ (𝑎 = 𝑐 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝑐‘𝑋) − (𝑐‘𝑌))) |
86 | 85 | breq2d 4595 |
. . 3
⊢ (𝑎 = 𝑐 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝑐‘𝑋) − (𝑐‘𝑌)))) |
87 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑏 ∘𝑓 + 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘𝑓 + 𝑐)‘𝑋)) |
88 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑏 ∘𝑓 + 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘𝑓 + 𝑐)‘𝑌)) |
89 | 87, 88 | oveq12d 6567 |
. . . 4
⊢ (𝑎 = (𝑏 ∘𝑓 + 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘𝑓 + 𝑐)‘𝑋) − ((𝑏 ∘𝑓 + 𝑐)‘𝑌))) |
90 | 89 | breq2d 4595 |
. . 3
⊢ (𝑎 = (𝑏 ∘𝑓 + 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘𝑓 + 𝑐)‘𝑋) − ((𝑏 ∘𝑓 + 𝑐)‘𝑌)))) |
91 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑏 ∘𝑓 · 𝑐) → (𝑎‘𝑋) = ((𝑏 ∘𝑓 · 𝑐)‘𝑋)) |
92 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑏 ∘𝑓 · 𝑐) → (𝑎‘𝑌) = ((𝑏 ∘𝑓 · 𝑐)‘𝑌)) |
93 | 91, 92 | oveq12d 6567 |
. . . 4
⊢ (𝑎 = (𝑏 ∘𝑓 · 𝑐) → ((𝑎‘𝑋) − (𝑎‘𝑌)) = (((𝑏 ∘𝑓 · 𝑐)‘𝑋) − ((𝑏 ∘𝑓 · 𝑐)‘𝑌))) |
94 | 93 | breq2d 4595 |
. . 3
⊢ (𝑎 = (𝑏 ∘𝑓 · 𝑐) → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ (((𝑏 ∘𝑓 · 𝑐)‘𝑋) − ((𝑏 ∘𝑓 · 𝑐)‘𝑌)))) |
95 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = 𝐹 → (𝑎‘𝑋) = (𝐹‘𝑋)) |
96 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = 𝐹 → (𝑎‘𝑌) = (𝐹‘𝑌)) |
97 | 95, 96 | oveq12d 6567 |
. . . 4
⊢ (𝑎 = 𝐹 → ((𝑎‘𝑋) − (𝑎‘𝑌)) = ((𝐹‘𝑋) − (𝐹‘𝑌))) |
98 | 97 | breq2d 4595 |
. . 3
⊢ (𝑎 = 𝐹 → (𝑁 ∥ ((𝑎‘𝑋) − (𝑎‘𝑌)) ↔ 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))) |
99 | 16, 37, 62, 70, 74, 78, 82, 86, 90, 94, 98 | mzpindd 36327 |
. 2
⊢ (((𝑉 ∈ V ∧ (𝑋 ∈ (ℤ
↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) ∧ 𝐹 ∈ (mzPoly‘𝑉)) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))) |
100 | 2, 3, 99 | syl2anc 691 |
1
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑𝑚
𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚
𝑉)) ∧ (𝑁 ∈ ℤ ∧
∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))) |