Metamath Proof Explorer

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 · 𝐺 ) ∈ 𝑃 ) )