Theorem coe1fval3

Description: Univariate power series coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	coe1fval.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
	coe1f2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1f2.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
	coe1fval3.g	⊢ 𝐺 = ( 𝑦 ∈ ℕ0 ↦ ( 1o × { 𝑦 } ) )
Assertion	coe1fval3	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 = ( 𝐹 ∘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
2		coe1f2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		coe1f2.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
4		coe1fval3.g	⊢ 𝐺 = ( 𝑦 ∈ ℕ0 ↦ ( 1o × { 𝑦 } ) )
5	1	coe1fval	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 = ( 𝑦 ∈ ℕ0 ↦ ( 𝐹 ‘ ( 1o × { 𝑦 } ) ) ) )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7	3 2 6	psr1basf	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑅 ) )
8		ssv	⊢ ( Base ‘ 𝑅 ) ⊆ V
9		fss	⊢ ( ( 𝐹 : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑅 ) ∧ ( Base ‘ 𝑅 ) ⊆ V ) → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ V )
10	7 8 9	sylancl	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ V )
11		fconst6g	⊢ ( 𝑦 ∈ ℕ0 → ( 1o × { 𝑦 } ) : 1o ⟶ ℕ0 )
12	11	adantl	⊢ ( ( 𝐹 : ( ℕ0 ↑m 1o ) ⟶ V ∧ 𝑦 ∈ ℕ0 ) → ( 1o × { 𝑦 } ) : 1o ⟶ ℕ0 )
13		nn0ex	⊢ ℕ0 ∈ V
14		1oex	⊢ 1o ∈ V
15	13 14	elmap	⊢ ( ( 1o × { 𝑦 } ) ∈ ( ℕ0 ↑m 1o ) ↔ ( 1o × { 𝑦 } ) : 1o ⟶ ℕ0 )
16	12 15	sylibr	⊢ ( ( 𝐹 : ( ℕ0 ↑m 1o ) ⟶ V ∧ 𝑦 ∈ ℕ0 ) → ( 1o × { 𝑦 } ) ∈ ( ℕ0 ↑m 1o ) )
17	4	a1i	⊢ ( 𝐹 : ( ℕ0 ↑m 1o ) ⟶ V → 𝐺 = ( 𝑦 ∈ ℕ0 ↦ ( 1o × { 𝑦 } ) ) )
18		id	⊢ ( 𝐹 : ( ℕ0 ↑m 1o ) ⟶ V → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ V )
19	18	feqmptd	⊢ ( 𝐹 : ( ℕ0 ↑m 1o ) ⟶ V → 𝐹 = ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
20		fveq2	⊢ ( 𝑥 = ( 1o × { 𝑦 } ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 1o × { 𝑦 } ) ) )
21	16 17 19 20	fmptco	⊢ ( 𝐹 : ( ℕ0 ↑m 1o ) ⟶ V → ( 𝐹 ∘ 𝐺 ) = ( 𝑦 ∈ ℕ0 ↦ ( 𝐹 ‘ ( 1o × { 𝑦 } ) ) ) )
22	10 21	syl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 ∘ 𝐺 ) = ( 𝑦 ∈ ℕ0 ↦ ( 𝐹 ‘ ( 1o × { 𝑦 } ) ) ) )
23	5 22	eqtr4d	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 = ( 𝐹 ∘ 𝐺 ) )