Step |
Hyp |
Ref |
Expression |
1 |
|
elfvex |
⊢ ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) → 𝑉 ∈ V ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → 𝑉 ∈ V ) |
3 |
|
mzpincl |
⊢ ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) ) |
4 |
2 3
|
syl |
⊢ ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) ) |
5 |
|
mzpcl34 |
⊢ ( ( ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝐴 ∘f + 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝐴 ∘f · 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ) |
6 |
5
|
3expib |
⊢ ( ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) → ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝐴 ∘f + 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝐴 ∘f · 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ) ) |
7 |
4 6
|
mpcom |
⊢ ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝐴 ∘f + 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝐴 ∘f · 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ) |
8 |
7
|
simpld |
⊢ ( ( 𝐴 ∈ ( mzPoly ‘ 𝑉 ) ∧ 𝐵 ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝐴 ∘f + 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) |