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	⊢ ( ( 𝑃 ∈ ( 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		simprlr	⊢ ( ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) → ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 )
9	7 8	syl	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ 𝑉 ) → ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 )
10		fveq2	⊢ ( 𝑓 = 𝐹 → ( 𝑔 ‘ 𝑓 ) = ( 𝑔 ‘ 𝐹 ) )
11	10	mpteq2dv	⊢ ( 𝑓 = 𝐹 → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) = ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝐹 ) ) )
12	11	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 ↔ ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝐹 ) ) ∈ 𝑃 ) )
13	12	rspcva	⊢ ( ( 𝐹 ∈ 𝑉 ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 ) → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝐹 ) ) ∈ 𝑃 )
14	1 9 13	syl2anc	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ 𝑉 ) → ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝐹 ) ) ∈ 𝑃 )