Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
⊢ ( 𝑣 = 𝑉 → ( ℤ ↑m 𝑣 ) = ( ℤ ↑m 𝑉 ) ) |
2 |
1
|
oveq2d |
⊢ ( 𝑣 = 𝑉 → ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) = ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ) |
3 |
|
fveq2 |
⊢ ( 𝑣 = 𝑉 → ( mzPolyCld ‘ 𝑣 ) = ( mzPolyCld ‘ 𝑉 ) ) |
4 |
2 3
|
eleq12d |
⊢ ( 𝑣 = 𝑉 → ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∈ ( mzPolyCld ‘ 𝑣 ) ↔ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) ) ) |
5 |
|
ssid |
⊢ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) |
6 |
|
ovex |
⊢ ( ℤ ↑m 𝑣 ) ∈ V |
7 |
|
zex |
⊢ ℤ ∈ V |
8 |
6 7
|
constmap |
⊢ ( 𝑓 ∈ ℤ → ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) |
9 |
8
|
rgen |
⊢ ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) |
10 |
|
vex |
⊢ 𝑣 ∈ V |
11 |
7 10
|
elmap |
⊢ ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↔ 𝑔 : 𝑣 ⟶ ℤ ) |
12 |
|
ffvelrn |
⊢ ( ( 𝑔 : 𝑣 ⟶ ℤ ∧ 𝑓 ∈ 𝑣 ) → ( 𝑔 ‘ 𝑓 ) ∈ ℤ ) |
13 |
11 12
|
sylanb |
⊢ ( ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ∧ 𝑓 ∈ 𝑣 ) → ( 𝑔 ‘ 𝑓 ) ∈ ℤ ) |
14 |
13
|
ancoms |
⊢ ( ( 𝑓 ∈ 𝑣 ∧ 𝑔 ∈ ( ℤ ↑m 𝑣 ) ) → ( 𝑔 ‘ 𝑓 ) ∈ ℤ ) |
15 |
14
|
fmpttd |
⊢ ( 𝑓 ∈ 𝑣 → ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
16 |
7 6
|
elmap |
⊢ ( ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
17 |
15 16
|
sylibr |
⊢ ( 𝑓 ∈ 𝑣 → ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) |
18 |
17
|
rgen |
⊢ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) |
19 |
9 18
|
pm3.2i |
⊢ ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) |
20 |
|
zaddcl |
⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 + 𝑏 ) ∈ ℤ ) |
21 |
20
|
adantl |
⊢ ( ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 + 𝑏 ) ∈ ℤ ) |
22 |
|
simpl |
⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
23 |
|
simpr |
⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
24 |
|
ovexd |
⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → ( ℤ ↑m 𝑣 ) ∈ V ) |
25 |
|
inidm |
⊢ ( ( ℤ ↑m 𝑣 ) ∩ ( ℤ ↑m 𝑣 ) ) = ( ℤ ↑m 𝑣 ) |
26 |
21 22 23 24 24 25
|
off |
⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
27 |
|
zmulcl |
⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 · 𝑏 ) ∈ ℤ ) |
28 |
27
|
adantl |
⊢ ( ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 · 𝑏 ) ∈ ℤ ) |
29 |
28 22 23 24 24 25
|
off |
⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
30 |
26 29
|
jca |
⊢ ( ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) → ( ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) ) |
31 |
7 6
|
elmap |
⊢ ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
32 |
7 6
|
elmap |
⊢ ( 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
33 |
31 32
|
anbi12i |
⊢ ( ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ↔ ( 𝑓 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ 𝑔 : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) ) |
34 |
7 6
|
elmap |
⊢ ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
35 |
7 6
|
elmap |
⊢ ( ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ↔ ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) |
36 |
34 35
|
anbi12i |
⊢ ( ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ↔ ( ( 𝑓 ∘f + 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ∧ ( 𝑓 ∘f · 𝑔 ) : ( ℤ ↑m 𝑣 ) ⟶ ℤ ) ) |
37 |
30 33 36
|
3imtr4i |
⊢ ( ( 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ) |
38 |
37
|
rgen2 |
⊢ ∀ 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∀ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) |
39 |
19 38
|
pm3.2i |
⊢ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ∧ ∀ 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∀ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ) |
40 |
|
elmzpcl |
⊢ ( 𝑣 ∈ V → ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∈ ( mzPolyCld ‘ 𝑣 ) ↔ ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ∧ ∀ 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∀ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ) ) ) ) |
41 |
10 40
|
ax-mp |
⊢ ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∈ ( mzPolyCld ‘ 𝑣 ) ↔ ( ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ⊆ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑣 ) × { 𝑓 } ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ∀ 𝑓 ∈ 𝑣 ( 𝑔 ∈ ( ℤ ↑m 𝑣 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ∧ ∀ 𝑓 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∀ 𝑔 ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ( ( 𝑓 ∘f + 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∧ ( 𝑓 ∘f · 𝑔 ) ∈ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ) ) ) ) |
42 |
5 39 41
|
mpbir2an |
⊢ ( ℤ ↑m ( ℤ ↑m 𝑣 ) ) ∈ ( mzPolyCld ‘ 𝑣 ) |
43 |
4 42
|
vtoclg |
⊢ ( 𝑉 ∈ V → ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) ) |