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

Metamath Proof Explorer

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 } ) )