Metamath Proof Explorer

Theorem mzpcl1

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

Ref Expression
Assertion mzpcl1 ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ ℤ → ℤ V × F ∈ P

Proof

Step Hyp Ref Expression
1 simpr ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ ℤ → F ∈ ℤ
2 simpl ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ ℤ → P ∈ mzPolyCld ⁡ V
3 elfvex ⊢ P ∈ mzPolyCld ⁡ V → V ∈ V
4 3 adantr ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ ℤ → 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 ∈ ℤ → 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 ∈ ℤ → 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 simprll ⊢ 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 × f ∈ P
9 7 8 syl ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ ℤ → ∀ f ∈ ℤ ℤ V × f ∈ P
10 sneq ⊢ f = F → f = F
11 10 xpeq2d ⊢ f = F → ℤ V × f = ℤ V × F
12 11 eleq1d ⊢ f = F → ℤ V × f ∈ P ↔ ℤ V × F ∈ P
13 12 rspcva ⊢ F ∈ ℤ ∧ ∀ f ∈ ℤ ℤ V × f ∈ P → ℤ V × F ∈ P
14 1 9 13 syl2anc ⊢ P ∈ mzPolyCld ⁡ V ∧ F ∈ ℤ → ℤ V × F ∈ P