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

Metamath Proof Explorer

Theorem ringnegr

Description: Negation in a ring is the same as right multiplication by -1. ( rngonegmn1r analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)

Ref Expression
Hypotheses ringnegl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringnegl.t ⊢ · = ( .r ‘ 𝑅 )
ringnegl.u ⊢ 1 = ( 1r ‘ 𝑅 )
ringnegl.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
ringnegl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ringnegl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion ringnegr ( 𝜑 → ( 𝑋 · ( 𝑁 ‘ 1 ) ) = ( 𝑁 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ringnegl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringnegl.t ⊢ · = ( .r ‘ 𝑅 )
3 ringnegl.u ⊢ 1 = ( 1r ‘ 𝑅 )
4 ringnegl.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
5 ringnegl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 ringnegl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
8 5 7 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
9 1 3 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
10 5 9 syl ⊢ ( 𝜑 → 1 ∈ 𝐵 )
11 1 4 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → ( 𝑁 ‘ 1 ) ∈ 𝐵 )
12 8 10 11 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 1 ) ∈ 𝐵 )
13 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
14 1 13 2 ringdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 1 ) ∈ 𝐵 ∧ 1 ∈ 𝐵 ) ) → ( 𝑋 · ( ( 𝑁 ‘ 1 ) ( +g ‘ 𝑅 ) 1 ) ) = ( ( 𝑋 · ( 𝑁 ‘ 1 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 1 ) ) )
15 5 6 12 10 14 syl13anc ⊢ ( 𝜑 → ( 𝑋 · ( ( 𝑁 ‘ 1 ) ( +g ‘ 𝑅 ) 1 ) ) = ( ( 𝑋 · ( 𝑁 ‘ 1 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 1 ) ) )
16 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17 1 13 16 4 grplinv ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → ( ( 𝑁 ‘ 1 ) ( +g ‘ 𝑅 ) 1 ) = ( 0g ‘ 𝑅 ) )
18 8 10 17 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 1 ) ( +g ‘ 𝑅 ) 1 ) = ( 0g ‘ 𝑅 ) )
19 18 oveq2d ⊢ ( 𝜑 → ( 𝑋 · ( ( 𝑁 ‘ 1 ) ( +g ‘ 𝑅 ) 1 ) ) = ( 𝑋 · ( 0g ‘ 𝑅 ) ) )
20 1 2 16 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
21 5 6 20 syl2anc ⊢ ( 𝜑 → ( 𝑋 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
22 19 21 eqtrd ⊢ ( 𝜑 → ( 𝑋 · ( ( 𝑁 ‘ 1 ) ( +g ‘ 𝑅 ) 1 ) ) = ( 0g ‘ 𝑅 ) )
23 1 2 3 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 1 ) = 𝑋 )
24 5 6 23 syl2anc ⊢ ( 𝜑 → ( 𝑋 · 1 ) = 𝑋 )
25 24 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝑁 ‘ 1 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 1 ) ) = ( ( 𝑋 · ( 𝑁 ‘ 1 ) ) ( +g ‘ 𝑅 ) 𝑋 ) )
26 15 22 25 3eqtr3rd ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝑁 ‘ 1 ) ) ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) )
27 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 1 ) ∈ 𝐵 ) → ( 𝑋 · ( 𝑁 ‘ 1 ) ) ∈ 𝐵 )
28 5 6 12 27 syl3anc ⊢ ( 𝜑 → ( 𝑋 · ( 𝑁 ‘ 1 ) ) ∈ 𝐵 )
29 1 13 16 4 grpinvid2 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 · ( 𝑁 ‘ 1 ) ) ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) = ( 𝑋 · ( 𝑁 ‘ 1 ) ) ↔ ( ( 𝑋 · ( 𝑁 ‘ 1 ) ) ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) ) )
30 8 6 28 29 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) = ( 𝑋 · ( 𝑁 ‘ 1 ) ) ↔ ( ( 𝑋 · ( 𝑁 ‘ 1 ) ) ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) ) )
31 26 30 mpbird ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = ( 𝑋 · ( 𝑁 ‘ 1 ) ) )
32 31 eqcomd ⊢ ( 𝜑 → ( 𝑋 · ( 𝑁 ‘ 1 ) ) = ( 𝑁 ‘ 𝑋 ) )