Theorem psrlinv

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	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	psrlinv.o	⊢ 0 = ( 0g ‘ 𝑅 )
	psrlinv.p	⊢ + = ( +g ‘ 𝑆 )
Assertion	psrlinv	⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑋 ) + 𝑋 ) = ( 𝐷 × { 0 } ) )

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		psrlinv.o	⊢ 0 = ( 0g ‘ 𝑅 )
9		psrlinv.p	⊢ + = ( +g ‘ 𝑆 )
10		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
11	4 10	rabex2	⊢ 𝐷 ∈ V
12	11	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
13		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ∈ V )
14		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15	1 14 4 6 7	psrelbas	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
16	15	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
17	15	feqmptd	⊢ ( 𝜑 → 𝑋 = ( 𝑥 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑥 ) ) )
18	14 5 3	grpinvf1o	⊢ ( 𝜑 → 𝑁 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑅 ) )
19		f1of	⊢ ( 𝑁 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑅 ) → 𝑁 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
20	18 19	syl	⊢ ( 𝜑 → 𝑁 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
21	20	feqmptd	⊢ ( 𝜑 → 𝑁 = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 𝑁 ‘ 𝑦 ) ) )
22		fveq2	⊢ ( 𝑦 = ( 𝑋 ‘ 𝑥 ) → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) )
23	16 17 21 22	fmptco	⊢ ( 𝜑 → ( 𝑁 ∘ 𝑋 ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
24	12 13 16 23 17	offval2	⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑋 ) ∘f ( +g ‘ 𝑅 ) 𝑋 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑥 ) ) ) )
25		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
26	1 2 3 4 5 6 7	psrnegcl	⊢ ( 𝜑 → ( 𝑁 ∘ 𝑋 ) ∈ 𝐵 )
27	1 6 25 9 26 7	psradd	⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑋 ) + 𝑋 ) = ( ( 𝑁 ∘ 𝑋 ) ∘f ( +g ‘ 𝑅 ) 𝑋 ) )
28		fconstmpt	⊢ ( 𝐷 × { 0 } ) = ( 𝑥 ∈ 𝐷 ↦ 0 )
29	14 25 8 5	grplinv	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑥 ) ) = 0 )
30	3 16 29	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑥 ) ) = 0 )
31	30	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ 0 ) )
32	28 31	eqtr4id	⊢ ( 𝜑 → ( 𝐷 × { 0 } ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 𝑁 ‘ ( 𝑋 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑥 ) ) ) )
33	24 27 32	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑋 ) + 𝑋 ) = ( 𝐷 × { 0 } ) )