Step | Hyp | Ref
| Expression |
1 | | mzpval 36313 |
. 2
⊢ (𝑉 ∈ V →
(mzPoly‘𝑉) = ∩ (mzPolyCld‘𝑉)) |
2 | | mzpclall 36308 |
. . . . 5
⊢ (𝑉 ∈ V → (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∈ (mzPolyCld‘𝑉)) |
3 | | intss1 4427 |
. . . . 5
⊢ ((ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∈ (mzPolyCld‘𝑉) → ∩ (mzPolyCld‘𝑉) ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉))) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝑉 ∈ V → ∩ (mzPolyCld‘𝑉) ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉))) |
5 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝑓 ∈ ℤ) ∧ 𝑎 ∈ (mzPolyCld‘𝑉)) → 𝑎 ∈ (mzPolyCld‘𝑉)) |
6 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝑓 ∈ ℤ) ∧ 𝑎 ∈ (mzPolyCld‘𝑉)) → 𝑓 ∈ ℤ) |
7 | | mzpcl1 36310 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (mzPolyCld‘𝑉) ∧ 𝑓 ∈ ℤ) → ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ 𝑎) |
8 | 5, 6, 7 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝑓 ∈ ℤ) ∧ 𝑎 ∈ (mzPolyCld‘𝑉)) → ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ 𝑎) |
9 | 8 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝑓 ∈ ℤ) →
∀𝑎 ∈
(mzPolyCld‘𝑉)((ℤ ↑𝑚 𝑉) × {𝑓}) ∈ 𝑎) |
10 | | ovex 6577 |
. . . . . . . . 9
⊢ (ℤ
↑𝑚 𝑉) ∈ V |
11 | | snex 4835 |
. . . . . . . . 9
⊢ {𝑓} ∈ V |
12 | 10, 11 | xpex 6860 |
. . . . . . . 8
⊢ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ V |
13 | 12 | elint2 4417 |
. . . . . . 7
⊢
(((ℤ ↑𝑚 𝑉) × {𝑓}) ∈ ∩
(mzPolyCld‘𝑉) ↔
∀𝑎 ∈
(mzPolyCld‘𝑉)((ℤ ↑𝑚 𝑉) × {𝑓}) ∈ 𝑎) |
14 | 9, 13 | sylibr 223 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝑓 ∈ ℤ) →
((ℤ ↑𝑚 𝑉) × {𝑓}) ∈ ∩
(mzPolyCld‘𝑉)) |
15 | 14 | ralrimiva 2949 |
. . . . 5
⊢ (𝑉 ∈ V → ∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ ∩
(mzPolyCld‘𝑉)) |
16 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝑓 ∈ 𝑉) ∧ 𝑎 ∈ (mzPolyCld‘𝑉)) → 𝑎 ∈ (mzPolyCld‘𝑉)) |
17 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝑓 ∈ 𝑉) ∧ 𝑎 ∈ (mzPolyCld‘𝑉)) → 𝑓 ∈ 𝑉) |
18 | | mzpcl2 36311 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (mzPolyCld‘𝑉) ∧ 𝑓 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ 𝑎) |
19 | 16, 17, 18 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝑓 ∈ 𝑉) ∧ 𝑎 ∈ (mzPolyCld‘𝑉)) → (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ 𝑎) |
20 | 19 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝑓 ∈ 𝑉) → ∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ 𝑎) |
21 | 10 | mptex 6390 |
. . . . . . . 8
⊢ (𝑔 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑔‘𝑓)) ∈ V |
22 | 21 | elint2 4417 |
. . . . . . 7
⊢ ((𝑔 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑔‘𝑓)) ∈ ∩
(mzPolyCld‘𝑉) ↔
∀𝑎 ∈
(mzPolyCld‘𝑉)(𝑔 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑔‘𝑓)) ∈ 𝑎) |
23 | 20, 22 | sylibr 223 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝑓 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ ∩
(mzPolyCld‘𝑉)) |
24 | 23 | ralrimiva 2949 |
. . . . 5
⊢ (𝑉 ∈ V → ∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ ∩
(mzPolyCld‘𝑉)) |
25 | 15, 24 | jca 553 |
. . . 4
⊢ (𝑉 ∈ V → (∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ ∩
(mzPolyCld‘𝑉) ∧
∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ ∩
(mzPolyCld‘𝑉))) |
26 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
27 | 26 | elint2 4417 |
. . . . . . . 8
⊢ (𝑓 ∈ ∩ (mzPolyCld‘𝑉) ↔ ∀𝑎 ∈ (mzPolyCld‘𝑉)𝑓 ∈ 𝑎) |
28 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
29 | 28 | elint2 4417 |
. . . . . . . 8
⊢ (𝑔 ∈ ∩ (mzPolyCld‘𝑉) ↔ ∀𝑎 ∈ (mzPolyCld‘𝑉)𝑔 ∈ 𝑎) |
30 | | mzpcl34 36312 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (mzPolyCld‘𝑉) ∧ 𝑓 ∈ 𝑎 ∧ 𝑔 ∈ 𝑎) → ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑎 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑎)) |
31 | 30 | 3expib 1260 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (mzPolyCld‘𝑉) → ((𝑓 ∈ 𝑎 ∧ 𝑔 ∈ 𝑎) → ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑎 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑎))) |
32 | 31 | ralimia 2934 |
. . . . . . . . 9
⊢
(∀𝑎 ∈
(mzPolyCld‘𝑉)(𝑓 ∈ 𝑎 ∧ 𝑔 ∈ 𝑎) → ∀𝑎 ∈ (mzPolyCld‘𝑉)((𝑓 ∘𝑓 + 𝑔) ∈ 𝑎 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑎)) |
33 | | r19.26 3046 |
. . . . . . . . 9
⊢
(∀𝑎 ∈
(mzPolyCld‘𝑉)(𝑓 ∈ 𝑎 ∧ 𝑔 ∈ 𝑎) ↔ (∀𝑎 ∈ (mzPolyCld‘𝑉)𝑓 ∈ 𝑎 ∧ ∀𝑎 ∈ (mzPolyCld‘𝑉)𝑔 ∈ 𝑎)) |
34 | | r19.26 3046 |
. . . . . . . . 9
⊢
(∀𝑎 ∈
(mzPolyCld‘𝑉)((𝑓 ∘𝑓 +
𝑔) ∈ 𝑎 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑎) ↔ (∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑓 ∘𝑓 + 𝑔) ∈ 𝑎 ∧ ∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑓 ∘𝑓 · 𝑔) ∈ 𝑎)) |
35 | 32, 33, 34 | 3imtr3i 279 |
. . . . . . . 8
⊢
((∀𝑎 ∈
(mzPolyCld‘𝑉)𝑓 ∈ 𝑎 ∧ ∀𝑎 ∈ (mzPolyCld‘𝑉)𝑔 ∈ 𝑎) → (∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑓 ∘𝑓 + 𝑔) ∈ 𝑎 ∧ ∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑓 ∘𝑓 · 𝑔) ∈ 𝑎)) |
36 | 27, 29, 35 | syl2anb 495 |
. . . . . . 7
⊢ ((𝑓 ∈ ∩ (mzPolyCld‘𝑉) ∧ 𝑔 ∈ ∩
(mzPolyCld‘𝑉)) →
(∀𝑎 ∈
(mzPolyCld‘𝑉)(𝑓 ∘𝑓 +
𝑔) ∈ 𝑎 ∧ ∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑓 ∘𝑓 · 𝑔) ∈ 𝑎)) |
37 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑓 ∘𝑓 +
𝑔) ∈
V |
38 | 37 | elint2 4417 |
. . . . . . . 8
⊢ ((𝑓 ∘𝑓 +
𝑔) ∈ ∩ (mzPolyCld‘𝑉) ↔ ∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑓 ∘𝑓 + 𝑔) ∈ 𝑎) |
39 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑓 ∘𝑓
· 𝑔) ∈
V |
40 | 39 | elint2 4417 |
. . . . . . . 8
⊢ ((𝑓 ∘𝑓
· 𝑔) ∈ ∩ (mzPolyCld‘𝑉) ↔ ∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑓 ∘𝑓 · 𝑔) ∈ 𝑎) |
41 | 38, 40 | anbi12i 729 |
. . . . . . 7
⊢ (((𝑓 ∘𝑓 +
𝑔) ∈ ∩ (mzPolyCld‘𝑉) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ ∩ (mzPolyCld‘𝑉)) ↔ (∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑓 ∘𝑓 + 𝑔) ∈ 𝑎 ∧ ∀𝑎 ∈ (mzPolyCld‘𝑉)(𝑓 ∘𝑓 · 𝑔) ∈ 𝑎)) |
42 | 36, 41 | sylibr 223 |
. . . . . 6
⊢ ((𝑓 ∈ ∩ (mzPolyCld‘𝑉) ∧ 𝑔 ∈ ∩
(mzPolyCld‘𝑉)) →
((𝑓
∘𝑓 + 𝑔) ∈ ∩
(mzPolyCld‘𝑉) ∧
(𝑓
∘𝑓 · 𝑔) ∈ ∩
(mzPolyCld‘𝑉))) |
43 | 42 | a1i 11 |
. . . . 5
⊢ (𝑉 ∈ V → ((𝑓 ∈ ∩ (mzPolyCld‘𝑉) ∧ 𝑔 ∈ ∩
(mzPolyCld‘𝑉)) →
((𝑓
∘𝑓 + 𝑔) ∈ ∩
(mzPolyCld‘𝑉) ∧
(𝑓
∘𝑓 · 𝑔) ∈ ∩
(mzPolyCld‘𝑉)))) |
44 | 43 | ralrimivv 2953 |
. . . 4
⊢ (𝑉 ∈ V → ∀𝑓 ∈ ∩ (mzPolyCld‘𝑉)∀𝑔 ∈ ∩
(mzPolyCld‘𝑉)((𝑓 ∘𝑓 +
𝑔) ∈ ∩ (mzPolyCld‘𝑉) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ ∩ (mzPolyCld‘𝑉))) |
45 | 4, 25, 44 | jca32 556 |
. . 3
⊢ (𝑉 ∈ V → (∩ (mzPolyCld‘𝑉) ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ ∩
(mzPolyCld‘𝑉) ∧
∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ ∩
(mzPolyCld‘𝑉)) ∧
∀𝑓 ∈ ∩ (mzPolyCld‘𝑉)∀𝑔 ∈ ∩
(mzPolyCld‘𝑉)((𝑓 ∘𝑓 +
𝑔) ∈ ∩ (mzPolyCld‘𝑉) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ ∩ (mzPolyCld‘𝑉))))) |
46 | | elmzpcl 36307 |
. . 3
⊢ (𝑉 ∈ V → (∩ (mzPolyCld‘𝑉) ∈ (mzPolyCld‘𝑉) ↔ (∩
(mzPolyCld‘𝑉) ⊆
(ℤ ↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ ∩
(mzPolyCld‘𝑉) ∧
∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ ∩
(mzPolyCld‘𝑉)) ∧
∀𝑓 ∈ ∩ (mzPolyCld‘𝑉)∀𝑔 ∈ ∩
(mzPolyCld‘𝑉)((𝑓 ∘𝑓 +
𝑔) ∈ ∩ (mzPolyCld‘𝑉) ∧ (𝑓 ∘𝑓 · 𝑔) ∈ ∩ (mzPolyCld‘𝑉)))))) |
47 | 45, 46 | mpbird 246 |
. 2
⊢ (𝑉 ∈ V → ∩ (mzPolyCld‘𝑉) ∈ (mzPolyCld‘𝑉)) |
48 | 1, 47 | eqeltrd 2688 |
1
⊢ (𝑉 ∈ V →
(mzPoly‘𝑉) ∈
(mzPolyCld‘𝑉)) |