Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) → 𝑊 ∈ V) |
2 | | elfvex 6131 |
. . 3
⊢ (𝐹 ∈ (mzPoly‘𝑉) → 𝑉 ∈ V) |
3 | 2 | 3ad2ant2 1076 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) → 𝑉 ∈ V) |
4 | | simp3 1056 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) → ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) |
5 | | simp2 1055 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) → 𝐹 ∈ (mzPoly‘𝑉)) |
6 | | simpr 476 |
. . . . . . 7
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ ℤ) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑥 ∈ (ℤ
↑𝑚 𝑊)) |
7 | | simpll3 1095 |
. . . . . . 7
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ ℤ) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) |
8 | | simpll2 1094 |
. . . . . . 7
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ ℤ) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑉 ∈ V) |
9 | | mzpf 36317 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ (mzPoly‘𝑊) → 𝐺:(ℤ ↑𝑚 𝑊)⟶ℤ) |
10 | 9 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝐺‘𝑥) ∈ ℤ) |
11 | 10 | expcom 450 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (ℤ
↑𝑚 𝑊) → (𝐺 ∈ (mzPoly‘𝑊) → (𝐺‘𝑥) ∈ ℤ)) |
12 | 11 | ralimdv 2946 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ℤ
↑𝑚 𝑊) → (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) → ∀𝑦 ∈ 𝑉 (𝐺‘𝑥) ∈ ℤ)) |
13 | 12 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑊) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) → ∀𝑦 ∈ 𝑉 (𝐺‘𝑥) ∈ ℤ) |
14 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) = (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) |
15 | 14 | fmpt 6289 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑉 (𝐺‘𝑥) ∈ ℤ ↔ (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)):𝑉⟶ℤ) |
16 | 13, 15 | sylib 207 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑊) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) → (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)):𝑉⟶ℤ) |
17 | 16 | adantr 480 |
. . . . . . . 8
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑊) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑉 ∈ V) → (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)):𝑉⟶ℤ) |
18 | | zex 11263 |
. . . . . . . . 9
⊢ ℤ
∈ V |
19 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑊) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑉 ∈ V) → 𝑉 ∈ V) |
20 | | elmapg 7757 |
. . . . . . . . 9
⊢ ((ℤ
∈ V ∧ 𝑉 ∈ V)
→ ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉) ↔ (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)):𝑉⟶ℤ)) |
21 | 18, 19, 20 | sylancr 694 |
. . . . . . . 8
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑊) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑉 ∈ V) → ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉) ↔ (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)):𝑉⟶ℤ)) |
22 | 17, 21 | mpbird 246 |
. . . . . . 7
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑊) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑉 ∈ V) → (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉)) |
23 | 6, 7, 8, 22 | syl21anc 1317 |
. . . . . 6
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ ℤ) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉)) |
24 | | vex 3176 |
. . . . . . 7
⊢ 𝑏 ∈ V |
25 | 24 | fvconst2 6374 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉) → (((ℤ
↑𝑚 𝑉) × {𝑏})‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = 𝑏) |
26 | 23, 25 | syl 17 |
. . . . 5
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ ℤ) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (((ℤ
↑𝑚 𝑉) × {𝑏})‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = 𝑏) |
27 | 26 | mpteq2dva 4672 |
. . . 4
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ ℤ) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (((ℤ
↑𝑚 𝑉) × {𝑏})‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ 𝑏)) |
28 | | mzpconstmpt 36321 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝑏 ∈ ℤ) → (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ 𝑏) ∈ (mzPoly‘𝑊)) |
29 | 28 | 3ad2antl1 1216 |
. . . 4
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ ℤ) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ 𝑏) ∈ (mzPoly‘𝑊)) |
30 | 27, 29 | eqeltrd 2688 |
. . 3
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ ℤ) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (((ℤ
↑𝑚 𝑉) × {𝑏})‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) |
31 | | simpr 476 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑥 ∈ (ℤ
↑𝑚 𝑊)) |
32 | | simpll3 1095 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) |
33 | | simpll2 1094 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑉 ∈ V) |
34 | 31, 32, 33, 22 | syl21anc 1317 |
. . . . . . . 8
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉)) |
35 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑐 = (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) → (𝑐‘𝑏) = ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))‘𝑏)) |
36 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏)) = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) |
37 | | fvex 6113 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))‘𝑏) ∈ V |
38 | 35, 36, 37 | fvmpt 6191 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉) → ((𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏))‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))‘𝑏)) |
39 | 34, 38 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ((𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏))‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))‘𝑏)) |
40 | | simplr 788 |
. . . . . . . 8
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑏 ∈ 𝑉) |
41 | | fvex 6113 |
. . . . . . . 8
⊢
(⦋𝑏 /
𝑦⦌𝐺‘𝑥) ∈ V |
42 | | csbeq1 3502 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → ⦋𝑎 / 𝑦⦌𝐺 = ⦋𝑏 / 𝑦⦌𝐺) |
43 | 42 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (⦋𝑎 / 𝑦⦌𝐺‘𝑥) = (⦋𝑏 / 𝑦⦌𝐺‘𝑥)) |
44 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑎(𝐺‘𝑥) |
45 | | nfcsb1v 3515 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦⦋𝑎 / 𝑦⦌𝐺 |
46 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝑥 |
47 | 45, 46 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(⦋𝑎 / 𝑦⦌𝐺‘𝑥) |
48 | | csbeq1a 3508 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑎 → 𝐺 = ⦋𝑎 / 𝑦⦌𝐺) |
49 | 48 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → (𝐺‘𝑥) = (⦋𝑎 / 𝑦⦌𝐺‘𝑥)) |
50 | 44, 47, 49 | cbvmpt 4677 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) = (𝑎 ∈ 𝑉 ↦ (⦋𝑎 / 𝑦⦌𝐺‘𝑥)) |
51 | 43, 50 | fvmptg 6189 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝑉 ∧ (⦋𝑏 / 𝑦⦌𝐺‘𝑥) ∈ V) → ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))‘𝑏) = (⦋𝑏 / 𝑦⦌𝐺‘𝑥)) |
52 | 40, 41, 51 | sylancl 693 |
. . . . . . 7
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))‘𝑏) = (⦋𝑏 / 𝑦⦌𝐺‘𝑥)) |
53 | 39, 52 | eqtrd 2644 |
. . . . . 6
⊢ ((((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ((𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏))‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = (⦋𝑏 / 𝑦⦌𝐺‘𝑥)) |
54 | 53 | mpteq2dva 4672 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏))‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦
(⦋𝑏 / 𝑦⦌𝐺‘𝑥))) |
55 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉) |
56 | | simpl3 1059 |
. . . . . . . 8
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) → ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) |
57 | | nfcsb1v 3515 |
. . . . . . . . . 10
⊢
Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐺 |
58 | 57 | nfel1 2765 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋𝑏 / 𝑦⦌𝐺 ∈ (mzPoly‘𝑊) |
59 | | csbeq1a 3508 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑏 → 𝐺 = ⦋𝑏 / 𝑦⦌𝐺) |
60 | 59 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → (𝐺 ∈ (mzPoly‘𝑊) ↔ ⦋𝑏 / 𝑦⦌𝐺 ∈ (mzPoly‘𝑊))) |
61 | 58, 60 | rspc 3276 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝑉 → (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) → ⦋𝑏 / 𝑦⦌𝐺 ∈ (mzPoly‘𝑊))) |
62 | 55, 56, 61 | sylc 63 |
. . . . . . 7
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) → ⦋𝑏 / 𝑦⦌𝐺 ∈ (mzPoly‘𝑊)) |
63 | | mzpf 36317 |
. . . . . . 7
⊢
(⦋𝑏 /
𝑦⦌𝐺 ∈ (mzPoly‘𝑊) → ⦋𝑏 / 𝑦⦌𝐺:(ℤ ↑𝑚 𝑊)⟶ℤ) |
64 | 62, 63 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) → ⦋𝑏 / 𝑦⦌𝐺:(ℤ ↑𝑚 𝑊)⟶ℤ) |
65 | 64 | feqmptd 6159 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) → ⦋𝑏 / 𝑦⦌𝐺 = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦
(⦋𝑏 / 𝑦⦌𝐺‘𝑥))) |
66 | 54, 65 | eqtr4d 2647 |
. . . 4
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏))‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = ⦋𝑏 / 𝑦⦌𝐺) |
67 | 66, 62 | eqeltrd 2688 |
. . 3
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝑏 ∈ 𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏))‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) |
68 | | simp2l 1080 |
. . . . . 6
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → 𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ) |
69 | | ffn 5958 |
. . . . . 6
⊢ (𝑏:(ℤ
↑𝑚 𝑉)⟶ℤ → 𝑏 Fn (ℤ ↑𝑚 𝑉)) |
70 | 68, 69 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → 𝑏 Fn (ℤ ↑𝑚 𝑉)) |
71 | | simp3l 1082 |
. . . . . 6
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → 𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ) |
72 | | ffn 5958 |
. . . . . 6
⊢ (𝑐:(ℤ
↑𝑚 𝑉)⟶ℤ → 𝑐 Fn (ℤ ↑𝑚 𝑉)) |
73 | 71, 72 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → 𝑐 Fn (ℤ ↑𝑚 𝑉)) |
74 | | simp13 1086 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) |
75 | | simp12 1085 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → 𝑉 ∈ V) |
76 | | simplll 794 |
. . . . . . 7
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑏 Fn (ℤ
↑𝑚 𝑉)) |
77 | | simpllr 795 |
. . . . . . 7
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑐 Fn (ℤ
↑𝑚 𝑉)) |
78 | | ovex 6577 |
. . . . . . . 8
⊢ (ℤ
↑𝑚 𝑉) ∈ V |
79 | 78 | a1i 11 |
. . . . . . 7
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (ℤ
↑𝑚 𝑉) ∈ V) |
80 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑥 ∈ (ℤ
↑𝑚 𝑊)) |
81 | | simplrl 796 |
. . . . . . . . . 10
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) |
82 | 80, 81, 12 | sylc 63 |
. . . . . . . . 9
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ∀𝑦 ∈ 𝑉 (𝐺‘𝑥) ∈ ℤ) |
83 | 82, 15 | sylib 207 |
. . . . . . . 8
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)):𝑉⟶ℤ) |
84 | | simplrr 797 |
. . . . . . . . 9
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑉 ∈ V) |
85 | 18, 84, 20 | sylancr 694 |
. . . . . . . 8
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ((𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉) ↔ (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)):𝑉⟶ℤ)) |
86 | 83, 85 | mpbird 246 |
. . . . . . 7
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉)) |
87 | | fnfvof 6809 |
. . . . . . 7
⊢ (((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ ((ℤ
↑𝑚 𝑉) ∈ V ∧ (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉))) → ((𝑏 ∘𝑓 +
𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) + (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
88 | 76, 77, 79, 86, 87 | syl22anc 1319 |
. . . . . 6
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ((𝑏 ∘𝑓 +
𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) + (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
89 | 88 | mpteq2dva 4672 |
. . . . 5
⊢ (((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓 +
𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) + (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))))) |
90 | 70, 73, 74, 75, 89 | syl22anc 1319 |
. . . 4
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓 +
𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) + (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))))) |
91 | | simp2r 1081 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) |
92 | | simp3r 1083 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) |
93 | | mzpaddmpt 36322 |
. . . . 5
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) + (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) ∈ (mzPoly‘𝑊)) |
94 | 91, 92, 93 | syl2anc 691 |
. . . 4
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) + (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) ∈ (mzPoly‘𝑊)) |
95 | 90, 94 | eqeltrd 2688 |
. . 3
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓 +
𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) |
96 | | fnfvof 6809 |
. . . . . . 7
⊢ (((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ ((ℤ
↑𝑚 𝑉) ∈ V ∧ (𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)) ∈ (ℤ ↑𝑚
𝑉))) → ((𝑏 ∘𝑓
· 𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) · (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
97 | 76, 77, 79, 86, 96 | syl22anc 1319 |
. . . . . 6
⊢ ((((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → ((𝑏 ∘𝑓
· 𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) · (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
98 | 97 | mpteq2dva 4672 |
. . . . 5
⊢ (((𝑏 Fn (ℤ
↑𝑚 𝑉) ∧ 𝑐 Fn (ℤ ↑𝑚 𝑉)) ∧ (∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊) ∧ 𝑉 ∈ V)) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓
· 𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) · (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))))) |
99 | 70, 73, 74, 75, 98 | syl22anc 1319 |
. . . 4
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓
· 𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) · (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))))) |
100 | | mzpmulmpt 36323 |
. . . . 5
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) · (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) ∈ (mzPoly‘𝑊)) |
101 | 91, 92, 100 | syl2anc 691 |
. . . 4
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) · (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) ∈ (mzPoly‘𝑊)) |
102 | 99, 101 | eqeltrd 2688 |
. . 3
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ (𝑏:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) ∧ (𝑐:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓
· 𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) |
103 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = ((ℤ
↑𝑚 𝑉) × {𝑏}) → (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = (((ℤ ↑𝑚
𝑉) × {𝑏})‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) |
104 | 103 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = ((ℤ
↑𝑚 𝑉) × {𝑏}) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (((ℤ
↑𝑚 𝑉) × {𝑏})‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
105 | 104 | eleq1d 2672 |
. . 3
⊢ (𝑎 = ((ℤ
↑𝑚 𝑉) × {𝑏}) → ((𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (((ℤ
↑𝑚 𝑉) × {𝑏})‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) |
106 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) → (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = ((𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏))‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) |
107 | 106 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏))‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
108 | 107 | eleq1d 2672 |
. . 3
⊢ (𝑎 = (𝑐 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑐‘𝑏)) → ((𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑐 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑐‘𝑏))‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) |
109 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = 𝑏 → (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) |
110 | 109 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = 𝑏 → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
111 | 110 | eleq1d 2672 |
. . 3
⊢ (𝑎 = 𝑏 → ((𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) |
112 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = 𝑐 → (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) |
113 | 112 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = 𝑐 → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
114 | 113 | eleq1d 2672 |
. . 3
⊢ (𝑎 = 𝑐 → ((𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑐‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) |
115 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑏 ∘𝑓 + 𝑐) → (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = ((𝑏 ∘𝑓 + 𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) |
116 | 115 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = (𝑏 ∘𝑓 + 𝑐) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓 +
𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
117 | 116 | eleq1d 2672 |
. . 3
⊢ (𝑎 = (𝑏 ∘𝑓 + 𝑐) → ((𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓 +
𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) |
118 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑏 ∘𝑓 · 𝑐) → (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = ((𝑏 ∘𝑓 · 𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) |
119 | 118 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = (𝑏 ∘𝑓 · 𝑐) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓
· 𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
120 | 119 | eleq1d 2672 |
. . 3
⊢ (𝑎 = (𝑏 ∘𝑓 · 𝑐) → ((𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ ((𝑏 ∘𝑓
· 𝑐)‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) |
121 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = 𝐹 → (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))) = (𝐹‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) |
122 | 121 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = 𝐹 → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥))))) |
123 | 122 | eleq1d 2672 |
. . 3
⊢ (𝑎 = 𝐹 → ((𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑎‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))) |
124 | 30, 67, 95, 102, 105, 108, 111, 114, 117, 120, 123 | mzpindd 36327 |
. 2
⊢ (((𝑊 ∈ V ∧ 𝑉 ∈ V ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) ∧ 𝐹 ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) |
125 | 1, 3, 4, 5, 124 | syl31anc 1321 |
1
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) |