Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . 4
⊢ (𝑣 = 𝑉 → (ℤ ↑𝑚
𝑣) = (ℤ
↑𝑚 𝑉)) |
2 | 1 | oveq2d 6666 |
. . 3
⊢ (𝑣 = 𝑉 → (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) = (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉))) |
3 | | fveq2 6191 |
. . 3
⊢ (𝑣 = 𝑉 → (mzPolyCld‘𝑣) = (mzPolyCld‘𝑉)) |
4 | 2, 3 | eleq12d 2695 |
. 2
⊢ (𝑣 = 𝑉 → ((ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) ∈ (mzPolyCld‘𝑣) ↔ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∈ (mzPolyCld‘𝑉))) |
5 | | ssid 3624 |
. . 3
⊢ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) |
6 | | ovex 6678 |
. . . . . . 7
⊢ (ℤ
↑𝑚 𝑣) ∈ V |
7 | | zex 11386 |
. . . . . . 7
⊢ ℤ
∈ V |
8 | 6, 7 | constmap 37276 |
. . . . . 6
⊢ (𝑓 ∈ ℤ → ((ℤ
↑𝑚 𝑣) × {𝑓}) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))) |
9 | 8 | rgen 2922 |
. . . . 5
⊢
∀𝑓 ∈
ℤ ((ℤ ↑𝑚 𝑣) × {𝑓}) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) |
10 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑣 ∈ V |
11 | 7, 10 | elmap 7886 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (ℤ
↑𝑚 𝑣) ↔ 𝑔:𝑣⟶ℤ) |
12 | | ffvelrn 6357 |
. . . . . . . . . 10
⊢ ((𝑔:𝑣⟶ℤ ∧ 𝑓 ∈ 𝑣) → (𝑔‘𝑓) ∈ ℤ) |
13 | 11, 12 | sylanb 489 |
. . . . . . . . 9
⊢ ((𝑔 ∈ (ℤ
↑𝑚 𝑣) ∧ 𝑓 ∈ 𝑣) → (𝑔‘𝑓) ∈ ℤ) |
14 | 13 | ancoms 469 |
. . . . . . . 8
⊢ ((𝑓 ∈ 𝑣 ∧ 𝑔 ∈ (ℤ ↑𝑚
𝑣)) → (𝑔‘𝑓) ∈ ℤ) |
15 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑔 ∈ (ℤ
↑𝑚 𝑣) ↦ (𝑔‘𝑓)) = (𝑔 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑔‘𝑓)) |
16 | 14, 15 | fmptd 6385 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑣 → (𝑔 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑔‘𝑓)):(ℤ ↑𝑚 𝑣)⟶ℤ) |
17 | 7, 6 | elmap 7886 |
. . . . . . 7
⊢ ((𝑔 ∈ (ℤ
↑𝑚 𝑣) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) ↔ (𝑔 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑔‘𝑓)):(ℤ ↑𝑚 𝑣)⟶ℤ) |
18 | 16, 17 | sylibr 224 |
. . . . . 6
⊢ (𝑓 ∈ 𝑣 → (𝑔 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))) |
19 | 18 | rgen 2922 |
. . . . 5
⊢
∀𝑓 ∈
𝑣 (𝑔 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) |
20 | 9, 19 | pm3.2i 471 |
. . . 4
⊢
(∀𝑓 ∈
ℤ ((ℤ ↑𝑚 𝑣) × {𝑓}) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) ∧ ∀𝑓 ∈ 𝑣 (𝑔 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))) |
21 | | zaddcl 11417 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ) |
22 | 21 | adantl 482 |
. . . . . . . 8
⊢ (((𝑓:(ℤ
↑𝑚 𝑣)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑣)⟶ℤ) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 + 𝑏) ∈ ℤ) |
23 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑓:(ℤ
↑𝑚 𝑣)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑣)⟶ℤ) → 𝑓:(ℤ
↑𝑚 𝑣)⟶ℤ) |
24 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑓:(ℤ
↑𝑚 𝑣)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑣)⟶ℤ) → 𝑔:(ℤ
↑𝑚 𝑣)⟶ℤ) |
25 | | ovexd 6680 |
. . . . . . . 8
⊢ ((𝑓:(ℤ
↑𝑚 𝑣)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑣)⟶ℤ) →
(ℤ ↑𝑚 𝑣) ∈ V) |
26 | | inidm 3822 |
. . . . . . . 8
⊢ ((ℤ
↑𝑚 𝑣) ∩ (ℤ ↑𝑚
𝑣)) = (ℤ
↑𝑚 𝑣) |
27 | 22, 23, 24, 25, 25, 26 | off 6912 |
. . . . . . 7
⊢ ((𝑓:(ℤ
↑𝑚 𝑣)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑣)⟶ℤ) → (𝑓 ∘𝑓 +
𝑔):(ℤ
↑𝑚 𝑣)⟶ℤ) |
28 | | zmulcl 11426 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 · 𝑏) ∈ ℤ) |
29 | 28 | adantl 482 |
. . . . . . . 8
⊢ (((𝑓:(ℤ
↑𝑚 𝑣)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑣)⟶ℤ) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 · 𝑏) ∈ ℤ) |
30 | 29, 23, 24, 25, 25, 26 | off 6912 |
. . . . . . 7
⊢ ((𝑓:(ℤ
↑𝑚 𝑣)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑣)⟶ℤ) → (𝑓 ∘𝑓
· 𝑔):(ℤ
↑𝑚 𝑣)⟶ℤ) |
31 | 27, 30 | jca 554 |
. . . . . 6
⊢ ((𝑓:(ℤ
↑𝑚 𝑣)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑣)⟶ℤ) → ((𝑓 ∘𝑓 +
𝑔):(ℤ
↑𝑚 𝑣)⟶ℤ ∧ (𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑣)⟶ℤ)) |
32 | 7, 6 | elmap 7886 |
. . . . . . 7
⊢ (𝑓 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ↔ 𝑓:(ℤ ↑𝑚 𝑣)⟶ℤ) |
33 | 7, 6 | elmap 7886 |
. . . . . . 7
⊢ (𝑔 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ↔ 𝑔:(ℤ ↑𝑚 𝑣)⟶ℤ) |
34 | 32, 33 | anbi12i 733 |
. . . . . 6
⊢ ((𝑓 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ 𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))) ↔ (𝑓:(ℤ ↑𝑚 𝑣)⟶ℤ ∧ 𝑔:(ℤ
↑𝑚 𝑣)⟶ℤ)) |
35 | 7, 6 | elmap 7886 |
. . . . . . 7
⊢ ((𝑓 ∘𝑓 +
𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ↔ (𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑣)⟶ℤ) |
36 | 7, 6 | elmap 7886 |
. . . . . . 7
⊢ ((𝑓 ∘𝑓
· 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ↔ (𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑣)⟶ℤ) |
37 | 35, 36 | anbi12i 733 |
. . . . . 6
⊢ (((𝑓 ∘𝑓 +
𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣))) ↔ ((𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑣)⟶ℤ ∧ (𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑣)⟶ℤ)) |
38 | 31, 34, 37 | 3imtr4i 281 |
. . . . 5
⊢ ((𝑓 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ 𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))) → ((𝑓 ∘𝑓 + 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)))) |
39 | 38 | rgen2a 2977 |
. . . 4
⊢
∀𝑓 ∈
(ℤ ↑𝑚 (ℤ ↑𝑚 𝑣))∀𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))((𝑓 ∘𝑓 + 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣))) |
40 | 20, 39 | pm3.2i 471 |
. . 3
⊢
((∀𝑓 ∈
ℤ ((ℤ ↑𝑚 𝑣) × {𝑓}) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) ∧ ∀𝑓 ∈ 𝑣 (𝑔 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))) ∧ ∀𝑓 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))∀𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))((𝑓 ∘𝑓 + 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)))) |
41 | | elmzpcl 37289 |
. . . 4
⊢ (𝑣 ∈ V → ((ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∈ (mzPolyCld‘𝑣) ↔ ((ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑣) × {𝑓}) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) ∧ ∀𝑓 ∈ 𝑣 (𝑔 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))) ∧ ∀𝑓 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))∀𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))((𝑓 ∘𝑓 + 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣))))))) |
42 | 10, 41 | ax-mp 5 |
. . 3
⊢ ((ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∈ (mzPolyCld‘𝑣) ↔ ((ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑣) × {𝑓}) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣)) ∧ ∀𝑓 ∈ 𝑣 (𝑔 ∈ (ℤ ↑𝑚
𝑣) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))) ∧ ∀𝑓 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))∀𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑣))((𝑓 ∘𝑓 + 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)))))) |
43 | 5, 40, 42 | mpbir2an 955 |
. 2
⊢ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑣)) ∈ (mzPolyCld‘𝑣) |
44 | 4, 43 | vtoclg 3266 |
1
⊢ (𝑉 ∈ V → (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∈ (mzPolyCld‘𝑉)) |