Theorem plyconst

Description: A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	plyconst	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		exp0	⊢ ( 𝑧 ∈ ℂ → ( 𝑧 ↑ 0 ) = 1 )
2	1	adantl	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ↑ 0 ) = 1 )
3	2	oveq2d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · ( 𝑧 ↑ 0 ) ) = ( 𝐴 · 1 ) )
4		ssel2	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ ℂ )
5	4	adantr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → 𝐴 ∈ ℂ )
6	5	mulridd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · 1 ) = 𝐴 )
7	3 6	eqtrd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · ( 𝑧 ↑ 0 ) ) = 𝐴 )
8	7	mpteq2dva	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 0 ) ) ) = ( 𝑧 ∈ ℂ ↦ 𝐴 ) )
9		fconstmpt	⊢ ( ℂ × { 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ 𝐴 )
10	8 9	eqtr4di	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 0 ) ) ) = ( ℂ × { 𝐴 } ) )
11		0nn0	⊢ 0 ∈ ℕ0
12		eqid	⊢ ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 0 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
13	12	ply1term	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 0 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 0 ) ) ) ∈ ( Poly ‘ 𝑆 ) )
14	11 13	mp3an3	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 0 ) ) ) ∈ ( Poly ‘ 𝑆 ) )
15	10 14	eqeltrrd	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ 𝑆 ) )