coef2

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

		Ref	Expression
	Hypothesis	dgrval.1	$⊢ A = coeff (F)$
	Assertion	coef2	$⊢ (F \in Poly (S) \land 0 \in S) \to A : ℕ_{0} ⟶ S$

Step	Hyp	Ref	Expression
1		dgrval.1	$⊢ A = coeff (F)$
2	1	coef	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ S \cup \{0\}$
3	2	adantr	$⊢ (F \in Poly (S) \land 0 \in S) \to A : ℕ_{0} ⟶ S \cup \{0\}$
4		simpr	$⊢ (F \in Poly (S) \land 0 \in S) \to 0 \in S$
5	4	snssd	$⊢ (F \in Poly (S) \land 0 \in S) \to \{0\} \subseteq S$
6		ssequn2	$⊢ \{0\} \subseteq S \leftrightarrow S \cup \{0\} = S$
7	5 6	sylib	$⊢ (F \in Poly (S) \land 0 \in S) \to S \cup \{0\} = S$
8	7	feq3d	$⊢ (F \in Poly (S) \land 0 \in S) \to (A : ℕ_{0} ⟶ S \cup \{0\} \leftrightarrow A : ℕ_{0} ⟶ S)$
9	3 8	mpbid	$⊢ (F \in Poly (S) \land 0 \in S) \to A : ℕ_{0} ⟶ S$

Metamath Proof Explorer