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

Metamath Proof Explorer

Theorem psrnegcl

Description: The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrgrp.s ⊢ S = I mPwSer R
psrgrp.i ⊢ φ → I ∈ V
psrgrp.r ⊢ φ → R ∈ Grp
psrnegcl.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
psrnegcl.i ⊢ N = inv g ⁡ R
psrnegcl.b ⊢ B = Base S
psrnegcl.z ⊢ φ → X ∈ B
Assertion psrnegcl ⊢ φ → N ∘ X ∈ B

Proof

Step Hyp Ref Expression
1 psrgrp.s ⊢ S = I mPwSer R
2 psrgrp.i ⊢ φ → I ∈ V
3 psrgrp.r ⊢ φ → R ∈ Grp
4 psrnegcl.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
5 psrnegcl.i ⊢ N = inv g ⁡ R
6 psrnegcl.b ⊢ B = Base S
7 psrnegcl.z ⊢ φ → X ∈ B
8 eqid ⊢ Base R = Base R
9 8 5 3 grpinvf1o ⊢ φ → N : Base R ⟶ 1-1 onto Base R
10 f1of ⊢ N : Base R ⟶ 1-1 onto Base R → N : Base R ⟶ Base R
11 9 10 syl ⊢ φ → N : Base R ⟶ Base R
12 1 8 4 6 7 psrelbas ⊢ φ → X : D ⟶ Base R
13 fco ⊢ N : Base R ⟶ Base R ∧ X : D ⟶ Base R → N ∘ X : D ⟶ Base R
14 11 12 13 syl2anc ⊢ φ → N ∘ X : D ⟶ Base R
15 fvex ⊢ Base R ∈ V
16 ovex ⊢ ℕ 0 I ∈ V
17 4 16 rabex2 ⊢ D ∈ V
18 15 17 elmap ⊢ N ∘ X ∈ Base R D ↔ N ∘ X : D ⟶ Base R
19 14 18 sylibr ⊢ φ → N ∘ X ∈ Base R D
20 1 8 4 6 2 psrbas ⊢ φ → B = Base R D
21 19 20 eleqtrrd ⊢ φ → N ∘ X ∈ B