plyconst

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

		Ref	Expression
	Assertion	plyconst	$⊢ (S \subseteq ℂ \land A \in S) \to ℂ \times \{A\} \in Poly (S)$

Step	Hyp	Ref	Expression
1		exp0	$⊢ z \in ℂ \to z^{0} = 1$
2	1	adantl	$⊢ ((S \subseteq ℂ \land A \in S) \land z \in ℂ) \to z^{0} = 1$
3	2	oveq2d	$⊢ ((S \subseteq ℂ \land A \in S) \land z \in ℂ) \to A z^{0} = A \cdot 1$
4		ssel2	$⊢ (S \subseteq ℂ \land A \in S) \to A \in ℂ$
5	4	adantr	$⊢ ((S \subseteq ℂ \land A \in S) \land z \in ℂ) \to A \in ℂ$
6	5	mulid1d	$⊢ ((S \subseteq ℂ \land A \in S) \land z \in ℂ) \to A \cdot 1 = A$
7	3 6	eqtrd	$⊢ ((S \subseteq ℂ \land A \in S) \land z \in ℂ) \to A z^{0} = A$
8	7	mpteq2dva	$⊢ (S \subseteq ℂ \land A \in S) \to (z \in ℂ ⟼ A z^{0}) = (z \in ℂ ⟼ A)$
9		fconstmpt	$⊢ ℂ \times \{A\} = (z \in ℂ ⟼ A)$
10	8 9	eqtr4di	$⊢ (S \subseteq ℂ \land A \in S) \to (z \in ℂ ⟼ A z^{0}) = ℂ \times \{A\}$
11		0nn0	$⊢ 0 \in ℕ_{0}$
12		eqid	$⊢ (z \in ℂ ⟼ A z^{0}) = (z \in ℂ ⟼ A z^{0})$
13	12	ply1term	$⊢ (S \subseteq ℂ \land A \in S \land 0 \in ℕ_{0}) \to (z \in ℂ ⟼ A z^{0}) \in Poly (S)$
14	11 13	mp3an3	$⊢ (S \subseteq ℂ \land A \in S) \to (z \in ℂ ⟼ A z^{0}) \in Poly (S)$
15	10 14	eqeltrrd	$⊢ (S \subseteq ℂ \land A \in S) \to ℂ \times \{A\} \in Poly (S)$

Metamath Proof Explorer