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	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝐹 } ) ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ ℤ ) → 𝐹 ∈ ℤ )
2		simpl	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ ℤ ) → 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) )
3		elfvex	⊢ ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) → 𝑉 ∈ V )
4	3	adantr	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ ℤ ) → 𝑉 ∈ V )
5		elmzpcl	⊢ ( 𝑉 ∈ V → ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ↔ ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) ) )
6	4 5	syl	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ ℤ ) → ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ↔ ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) ) )
7	2 6	mpbid	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ ℤ ) → ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) )
8		simprll	⊢ ( ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) → ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 )
9	7 8	syl	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ ℤ ) → ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 )
10		sneq	⊢ ( 𝑓 = 𝐹 → { 𝑓 } = { 𝐹 } )
11	10	xpeq2d	⊢ ( 𝑓 = 𝐹 → ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) = ( ( ℤ ↑m 𝑉 ) × { 𝐹 } ) )
12	11	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 ↔ ( ( ℤ ↑m 𝑉 ) × { 𝐹 } ) ∈ 𝑃 ) )
13	12	rspcva	⊢ ( ( 𝐹 ∈ ℤ ∧ ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 ) → ( ( ℤ ↑m 𝑉 ) × { 𝐹 } ) ∈ 𝑃 )
14	1 9 13	syl2anc	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝐹 } ) ∈ 𝑃 )