Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . . . 8
⊢ (((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑥 ∈ (ℤ
↑𝑚 𝑊)) |
2 | | zex 11386 |
. . . . . . . . 9
⊢ ℤ
∈ V |
3 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑊 ∈ V) |
4 | | elmapg 7870 |
. . . . . . . . 9
⊢ ((ℤ
∈ V ∧ 𝑊 ∈ V)
→ (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↔ 𝑥:𝑊⟶ℤ)) |
5 | 2, 3, 4 | sylancr 695 |
. . . . . . . 8
⊢ (((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝑥 ∈ (ℤ
↑𝑚 𝑊) ↔ 𝑥:𝑊⟶ℤ)) |
6 | 1, 5 | mpbid 222 |
. . . . . . 7
⊢ (((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑥:𝑊⟶ℤ) |
7 | | simplr 792 |
. . . . . . 7
⊢ (((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → 𝑅:𝑉⟶𝑊) |
8 | | fcompt 6400 |
. . . . . . 7
⊢ ((𝑥:𝑊⟶ℤ ∧ 𝑅:𝑉⟶𝑊) → (𝑥 ∘ 𝑅) = (𝑎 ∈ 𝑉 ↦ (𝑥‘(𝑅‘𝑎)))) |
9 | 6, 7, 8 | syl2anc 693 |
. . . . . 6
⊢ (((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝑥 ∘ 𝑅) = (𝑎 ∈ 𝑉 ↦ (𝑥‘(𝑅‘𝑎)))) |
10 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑥 → (𝑏‘(𝑅‘𝑎)) = (𝑥‘(𝑅‘𝑎))) |
11 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℤ
↑𝑚 𝑊) ↦ (𝑏‘(𝑅‘𝑎))) = (𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎))) |
12 | | fvex 6201 |
. . . . . . . . . 10
⊢ (𝑥‘(𝑅‘𝑎)) ∈ V |
13 | 10, 11, 12 | fvmpt 6282 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℤ
↑𝑚 𝑊) → ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥) = (𝑥‘(𝑅‘𝑎))) |
14 | 13 | ad2antlr 763 |
. . . . . . . 8
⊢ ((((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥) = (𝑥‘(𝑅‘𝑎))) |
15 | 14 | eqcomd 2628 |
. . . . . . 7
⊢ ((((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) ∧ 𝑎 ∈ 𝑉) → (𝑥‘(𝑅‘𝑎)) = ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥)) |
16 | 15 | mpteq2dva 4744 |
. . . . . 6
⊢ (((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝑎 ∈ 𝑉 ↦ (𝑥‘(𝑅‘𝑎))) = (𝑎 ∈ 𝑉 ↦ ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥))) |
17 | 9, 16 | eqtrd 2656 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝑥 ∘ 𝑅) = (𝑎 ∈ 𝑉 ↦ ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥))) |
18 | 17 | fveq2d 6195 |
. . . 4
⊢ (((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑊)) → (𝐹‘(𝑥 ∘ 𝑅)) = (𝐹‘(𝑎 ∈ 𝑉 ↦ ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥)))) |
19 | 18 | mpteq2dva 4744 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝑅:𝑉⟶𝑊) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑥 ∘ 𝑅))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑎 ∈ 𝑉 ↦ ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥))))) |
20 | 19 | 3adant2 1080 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑥 ∘ 𝑅))) = (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑎 ∈ 𝑉 ↦ ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥))))) |
21 | | simpl1 1064 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑎 ∈ 𝑉) → 𝑊 ∈ V) |
22 | | ffvelrn 6357 |
. . . . . 6
⊢ ((𝑅:𝑉⟶𝑊 ∧ 𝑎 ∈ 𝑉) → (𝑅‘𝑎) ∈ 𝑊) |
23 | 22 | 3ad2antl3 1225 |
. . . . 5
⊢ (((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑎 ∈ 𝑉) → (𝑅‘𝑎) ∈ 𝑊) |
24 | | mzpproj 37300 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ (𝑅‘𝑎) ∈ 𝑊) → (𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎))) ∈ (mzPoly‘𝑊)) |
25 | 21, 23, 24 | syl2anc 693 |
. . . 4
⊢ (((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) ∧ 𝑎 ∈ 𝑉) → (𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎))) ∈ (mzPoly‘𝑊)) |
26 | 25 | ralrimiva 2966 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) → ∀𝑎 ∈ 𝑉 (𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎))) ∈ (mzPoly‘𝑊)) |
27 | | mzpsubst 37311 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ ∀𝑎 ∈ 𝑉 (𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎))) ∈ (mzPoly‘𝑊)) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑎 ∈ 𝑉 ↦ ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥)))) ∈ (mzPoly‘𝑊)) |
28 | 26, 27 | syld3an3 1371 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑎 ∈ 𝑉 ↦ ((𝑏 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝑏‘(𝑅‘𝑎)))‘𝑥)))) ∈ (mzPoly‘𝑊)) |
29 | 20, 28 | eqeltrd 2701 |
1
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) → (𝑥 ∈ (ℤ ↑𝑚
𝑊) ↦ (𝐹‘(𝑥 ∘ 𝑅))) ∈ (mzPoly‘𝑊)) |