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	⊢ ( 𝜑 → ( 𝑁 ∘ 𝑋 ) ∈ 𝐵 )