Metamath Proof Explorer

Theorem mzpcl2

Description: Defining property 2 of a polynomially closed function set P : it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpcl2 ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ V → g ∈ ℤ V ⟼ g ⁡ F ∈ P

Proof

Step Hyp Ref Expression
1 simpr ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ V → F ∈ V
2 simpl ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ V → P ∈ mzPolyCld ⁡ V
3 elfvex ⊢ P ∈ mzPolyCld ⁡ V → V ∈ V
4 3 adantr ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ V → V ∈ V
5 elmzpcl ⊢ V ∈ V → P ∈ mzPolyCld ⁡ V ↔ P ⊆ ℤ ℤ V ∧ ∀ f ∈ ℤ ℤ V × f ∈ P ∧ ∀ f ∈ V g ∈ ℤ V ⟼ g ⁡ f ∈ P ∧ ∀ f ∈ P ∀ g ∈ P f + f g ∈ P ∧ f × f g ∈ P
6 4 5 syl ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ V → P ∈ mzPolyCld ⁡ V ↔ P ⊆ ℤ ℤ V ∧ ∀ f ∈ ℤ ℤ V × f ∈ P ∧ ∀ f ∈ V g ∈ ℤ V ⟼ g ⁡ f ∈ P ∧ ∀ f ∈ P ∀ g ∈ P f + f g ∈ P ∧ f × f g ∈ P
7 2 6 mpbid ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ V → P ⊆ ℤ ℤ V ∧ ∀ f ∈ ℤ ℤ V × f ∈ P ∧ ∀ f ∈ V g ∈ ℤ V ⟼ g ⁡ f ∈ P ∧ ∀ f ∈ P ∀ g ∈ P f + f g ∈ P ∧ f × f g ∈ P
8 simprlr ⊢ P ⊆ ℤ ℤ V ∧ ∀ f ∈ ℤ ℤ V × f ∈ P ∧ ∀ f ∈ V g ∈ ℤ V ⟼ g ⁡ f ∈ P ∧ ∀ f ∈ P ∀ g ∈ P f + f g ∈ P ∧ f × f g ∈ P → ∀ f ∈ V g ∈ ℤ V ⟼ g ⁡ f ∈ P
9 7 8 syl ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ V → ∀ f ∈ V g ∈ ℤ V ⟼ g ⁡ f ∈ P
10 fveq2 ⊢ f = F → g ⁡ f = g ⁡ F
11 10 mpteq2dv ⊢ f = F → g ∈ ℤ V ⟼ g ⁡ f = g ∈ ℤ V ⟼ g ⁡ F
12 11 eleq1d ⊢ f = F → g ∈ ℤ V ⟼ g ⁡ f ∈ P ↔ g ∈ ℤ V ⟼ g ⁡ F ∈ P
13 12 rspcva ⊢ F ∈ V ∧ ∀ f ∈ V g ∈ ℤ V ⟼ g ⁡ f ∈ P → g ∈ ℤ V ⟼ g ⁡ F ∈ P
14 1 9 13 syl2anc ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ V → g ∈ ℤ V ⟼ g ⁡ F ∈ P