coe1f2

Description: Functionality of univariate power series coefficient vectors. (Contributed by Stefan O'Rear, 25-Mar-2015)

Step	Hyp	Ref	Expression
1		coe1fval.a	$⊢ A = {coe}_{1} (F)$
2		coe1f2.b	$⊢ B = {Base}_{P}$
3		coe1f2.p	$⊢ P = {PwSer}_{1} (R)$
4		coe1f2.k	$⊢ K = {Base}_{R}$
5	3 2 4	psr1basf	$⊢ F \in B \to F : {ℕ_{0}}^{1_{𝑜}} ⟶ K$
6		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
7		nn0ex	$⊢ ℕ_{0} \in V$
8		0ex	$⊢ \emptyset \in V$
9		eqid	$⊢ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\}) = (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\})$
10	6 7 8 9	mapsnf1o3	$⊢ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\}) : ℕ_{0} \underset{1-1 onto}{⟶} {ℕ_{0}}^{1_{𝑜}}$
11		f1of	$⊢ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\}) : ℕ_{0} \underset{1-1 onto}{⟶} {ℕ_{0}}^{1_{𝑜}} \to (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\}) : ℕ_{0} ⟶ {ℕ_{0}}^{1_{𝑜}}$
12	10 11	ax-mp	$⊢ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\}) : ℕ_{0} ⟶ {ℕ_{0}}^{1_{𝑜}}$
13		fco	$⊢ (F : {ℕ_{0}}^{1_{𝑜}} ⟶ K \land (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\}) : ℕ_{0} ⟶ {ℕ_{0}}^{1_{𝑜}}) \to (F \circ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\})) : ℕ_{0} ⟶ K$
14	5 12 13	sylancl	$⊢ F \in B \to (F \circ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\})) : ℕ_{0} ⟶ K$
15	1 2 3 9	coe1fval3	$⊢ F \in B \to A = F \circ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\})$
16	15	feq1d	$⊢ F \in B \to (A : ℕ_{0} ⟶ K \leftrightarrow (F \circ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\})) : ℕ_{0} ⟶ K)$
17	14 16	mpbird	$⊢ F \in B \to A : ℕ_{0} ⟶ K$

Metamath Proof Explorer