Step | Hyp | Ref
| Expression |
1 | | simp2 1062 |
. 2
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → 𝐹 ∈ 𝑃) |
2 | | simp3 1063 |
. 2
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → 𝐺 ∈ 𝑃) |
3 | | simp1 1061 |
. . . 4
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → 𝑃 ∈ (mzPolyCld‘𝑉)) |
4 | 3 | elfvexd 6222 |
. . . . 5
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → 𝑉 ∈ V) |
5 | | elmzpcl 37289 |
. . . . 5
⊢ (𝑉 ∈ V → (𝑃 ∈ (mzPolyCld‘𝑉) ↔ (𝑃 ⊆ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ 𝑃 ∧ ∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ 𝑃) ∧ ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑃))))) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → (𝑃 ∈ (mzPolyCld‘𝑉) ↔ (𝑃 ⊆ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ 𝑃 ∧ ∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ 𝑃) ∧ ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑃))))) |
7 | 3, 6 | mpbid 222 |
. . 3
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → (𝑃 ⊆ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ 𝑃 ∧ ∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ 𝑃) ∧ ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑃)))) |
8 | 7 | simprrd 797 |
. 2
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑃)) |
9 | | oveq1 6657 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓 ∘𝑓 + 𝑔) = (𝐹 ∘𝑓 + 𝑔)) |
10 | 9 | eleq1d 2686 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑃 ↔ (𝐹 ∘𝑓 + 𝑔) ∈ 𝑃)) |
11 | | oveq1 6657 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓 ∘𝑓 · 𝑔) = (𝐹 ∘𝑓 · 𝑔)) |
12 | 11 | eleq1d 2686 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝑓 ∘𝑓 · 𝑔) ∈ 𝑃 ↔ (𝐹 ∘𝑓 · 𝑔) ∈ 𝑃)) |
13 | 10, 12 | anbi12d 747 |
. . 3
⊢ (𝑓 = 𝐹 → (((𝑓 ∘𝑓 + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑃) ↔ ((𝐹 ∘𝑓 + 𝑔) ∈ 𝑃 ∧ (𝐹 ∘𝑓 · 𝑔) ∈ 𝑃))) |
14 | | oveq2 6658 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝐹 ∘𝑓 + 𝑔) = (𝐹 ∘𝑓 + 𝐺)) |
15 | 14 | eleq1d 2686 |
. . . 4
⊢ (𝑔 = 𝐺 → ((𝐹 ∘𝑓 + 𝑔) ∈ 𝑃 ↔ (𝐹 ∘𝑓 + 𝐺) ∈ 𝑃)) |
16 | | oveq2 6658 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝐹 ∘𝑓 · 𝑔) = (𝐹 ∘𝑓 · 𝐺)) |
17 | 16 | eleq1d 2686 |
. . . 4
⊢ (𝑔 = 𝐺 → ((𝐹 ∘𝑓 · 𝑔) ∈ 𝑃 ↔ (𝐹 ∘𝑓 · 𝐺) ∈ 𝑃)) |
18 | 15, 17 | anbi12d 747 |
. . 3
⊢ (𝑔 = 𝐺 → (((𝐹 ∘𝑓 + 𝑔) ∈ 𝑃 ∧ (𝐹 ∘𝑓 · 𝑔) ∈ 𝑃) ↔ ((𝐹 ∘𝑓 + 𝐺) ∈ 𝑃 ∧ (𝐹 ∘𝑓 · 𝐺) ∈ 𝑃))) |
19 | 13, 18 | rspc2va 3323 |
. 2
⊢ (((𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) ∧ ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑃)) → ((𝐹 ∘𝑓 + 𝐺) ∈ 𝑃 ∧ (𝐹 ∘𝑓 · 𝐺) ∈ 𝑃)) |
20 | 1, 2, 8, 19 | syl21anc 1325 |
1
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → ((𝐹 ∘𝑓 + 𝐺) ∈ 𝑃 ∧ (𝐹 ∘𝑓 · 𝐺) ∈ 𝑃)) |