Theorem mzpcl34

Description: Defining properties 3 and 4 of a polynomially closed function set P : it is closed under pointwise addition and multiplication. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	mzpcl34	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( ( 𝐹 ∘f + 𝐺 ) ∈ 𝑃 ∧ ( 𝐹 ∘f · 𝐺 ) ∈ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → 𝐹 ∈ 𝑃 )
2		simp3	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → 𝐺 ∈ 𝑃 )
3		simp1	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) )
4	3	elfvexd	⊢ ( ( 𝑃 ∈ ( 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	3 6	mpbid	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑓 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑓 } ) ∈ 𝑃 ∧ ∀ 𝑓 ∈ 𝑉 ( 𝑔 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑔 ‘ 𝑓 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) )
8	7	simprrd	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) )
9		oveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∘f + 𝑔 ) = ( 𝐹 ∘f + 𝑔 ) )
10	9	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ↔ ( 𝐹 ∘f + 𝑔 ) ∈ 𝑃 ) )
11		oveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∘f · 𝑔 ) = ( 𝐹 ∘f · 𝑔 ) )
12	11	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ↔ ( 𝐹 ∘f · 𝑔 ) ∈ 𝑃 ) )
13	10 12	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ↔ ( ( 𝐹 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝐹 ∘f · 𝑔 ) ∈ 𝑃 ) ) )
14		oveq2	⊢ ( 𝑔 = 𝐺 → ( 𝐹 ∘f + 𝑔 ) = ( 𝐹 ∘f + 𝐺 ) )
15	14	eleq1d	⊢ ( 𝑔 = 𝐺 → ( ( 𝐹 ∘f + 𝑔 ) ∈ 𝑃 ↔ ( 𝐹 ∘f + 𝐺 ) ∈ 𝑃 ) )
16		oveq2	⊢ ( 𝑔 = 𝐺 → ( 𝐹 ∘f · 𝑔 ) = ( 𝐹 ∘f · 𝐺 ) )
17	16	eleq1d	⊢ ( 𝑔 = 𝐺 → ( ( 𝐹 ∘f · 𝑔 ) ∈ 𝑃 ↔ ( 𝐹 ∘f · 𝐺 ) ∈ 𝑃 ) )
18	15 17	anbi12d	⊢ ( 𝑔 = 𝐺 → ( ( ( 𝐹 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝐹 ∘f · 𝑔 ) ∈ 𝑃 ) ↔ ( ( 𝐹 ∘f + 𝐺 ) ∈ 𝑃 ∧ ( 𝐹 ∘f · 𝐺 ) ∈ 𝑃 ) ) )
19	13 18	rspc2va	⊢ ( ( ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) → ( ( 𝐹 ∘f + 𝐺 ) ∈ 𝑃 ∧ ( 𝐹 ∘f · 𝐺 ) ∈ 𝑃 ) )
20	1 2 8 19	syl21anc	⊢ ( ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( ( 𝐹 ∘f + 𝐺 ) ∈ 𝑃 ∧ ( 𝐹 ∘f · 𝐺 ) ∈ 𝑃 ) )