This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐹 ∈ 𝐵 → 𝐴 = ( 𝐹 ∘ 𝐺 ) )