Theorem coef2

Description: The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypothesis	dgrval.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
Assertion	coef2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2	1	coef	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
3	2	adantr	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
4		simpr	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → 0 ∈ 𝑆 )
5	4	snssd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → { 0 } ⊆ 𝑆 )
6		ssequn2	⊢ ( { 0 } ⊆ 𝑆 ↔ ( 𝑆 ∪ { 0 } ) = 𝑆 )
7	5 6	sylib	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → ( 𝑆 ∪ { 0 } ) = 𝑆 )
8	7	feq3d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ↔ 𝐴 : ℕ0 ⟶ 𝑆 ) )
9	3 8	mpbid	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ 𝑆 )