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

Metamath Proof Explorer

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 ⟶ 𝐾 )