Theorem coe1f2

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

	Ref	Expression
Hypotheses	coe1fval.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
	coe1f2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1f2.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
	coe1f2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion	coe1f2	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
2		coe1f2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		coe1f2.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
4		coe1f2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5	3 2 4	psr1basf	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )
6		df1o2	⊢ 1o = { ∅ }
7		nn0ex	⊢ ℕ0 ∈ V
8		0ex	⊢ ∅ ∈ V
9		eqid	⊢ ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) )
10	6 7 8 9	mapsnf1o3	⊢ ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o )
11		f1of	⊢ ( ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o ) → ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) : ℕ0 ⟶ ( ℕ0 ↑m 1o ) )
12	10 11	ax-mp	⊢ ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) : ℕ0 ⟶ ( ℕ0 ↑m 1o )
13		fco	⊢ ( ( 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 ∧ ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) : ℕ0 ⟶ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ∘ ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) ) : ℕ0 ⟶ 𝐾 )
14	5 12 13	sylancl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 ∘ ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) ) : ℕ0 ⟶ 𝐾 )
15	1 2 3 9	coe1fval3	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 = ( 𝐹 ∘ ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) ) )
16	15	feq1d	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐴 : ℕ0 ⟶ 𝐾 ↔ ( 𝐹 ∘ ( 𝑥 ∈ ℕ0 ↦ ( 1o × { 𝑥 } ) ) ) : ℕ0 ⟶ 𝐾 ) )
17	14 16	mpbird	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ 𝐾 )