This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coef2

Description: The domain and codomain 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 ⟶ 𝑆 )