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 ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrgrp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psrgrp.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
psrnegcl.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
psrnegcl.i ⊢ 𝑁 = ( invg ‘ 𝑅 )
psrnegcl.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psrnegcl.z ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion psrnegcl ( 𝜑 → ( 𝑁 ∘ 𝑋 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 psrgrp.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrgrp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 psrgrp.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
4 psrnegcl.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
5 psrnegcl.i ⊢ 𝑁 = ( invg ‘ 𝑅 )
6 psrnegcl.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
7 psrnegcl.z ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 8 5 3 grpinvf1o ⊢ ( 𝜑 → 𝑁 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑅 ) )
10 f1of ⊢ ( 𝑁 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑅 ) → 𝑁 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
11 9 10 syl ⊢ ( 𝜑 → 𝑁 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
12 1 8 4 6 7 psrelbas ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
13 fco ⊢ ( ( 𝑁 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) ∧ 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) → ( 𝑁 ∘ 𝑋 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
14 11 12 13 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∘ 𝑋 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
15 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
16 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
17 4 16 rabex2 ⊢ 𝐷 ∈ V
18 15 17 elmap ⊢ ( ( 𝑁 ∘ 𝑋 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝑁 ∘ 𝑋 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
19 14 18 sylibr ⊢ ( 𝜑 → ( 𝑁 ∘ 𝑋 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
20 1 8 4 6 2 psrbas ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
21 19 20 eleqtrrd ⊢ ( 𝜑 → ( 𝑁 ∘ 𝑋 ) ∈ 𝐵 )