Metamath Proof Explorer

Theorem ringnegl

Description: Negation in a ring is the same as left multiplication by -1. ( rngonegmn1l 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 ringnegl ( 𝜑 → ( ( 𝑁 ‘ 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 1 3 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
8 5 7 syl ⊢ ( 𝜑 → 1 ∈ 𝐵 )
9 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
10 5 9 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
11 1 4 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → ( 𝑁 ‘ 1 ) ∈ 𝐵 )
12 10 8 11 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 1 ) ∈ 𝐵 )
13 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
14 1 13 2 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1 ∈ 𝐵 ∧ ( 𝑁 ‘ 1 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 1 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 1 ) ) · 𝑋 ) = ( ( 1 · 𝑋 ) ( +g ‘ 𝑅 ) ( ( 𝑁 ‘ 1 ) · 𝑋 ) ) )
15 5 8 12 6 14 syl13anc ⊢ ( 𝜑 → ( ( 1 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 1 ) ) · 𝑋 ) = ( ( 1 · 𝑋 ) ( +g ‘ 𝑅 ) ( ( 𝑁 ‘ 1 ) · 𝑋 ) ) )
16 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17 1 13 16 4 grprinv ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → ( 1 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 1 ) ) = ( 0g ‘ 𝑅 ) )
18 10 8 17 syl2anc ⊢ ( 𝜑 → ( 1 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 1 ) ) = ( 0g ‘ 𝑅 ) )
19 18 oveq1d ⊢ ( 𝜑 → ( ( 1 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 1 ) ) · 𝑋 ) = ( ( 0g ‘ 𝑅 ) · 𝑋 ) )
20 1 2 16 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) · 𝑋 ) = ( 0g ‘ 𝑅 ) )
21 5 6 20 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) · 𝑋 ) = ( 0g ‘ 𝑅 ) )
22 19 21 eqtrd ⊢ ( 𝜑 → ( ( 1 ( +g ‘ 𝑅 ) ( 𝑁 ‘ 1 ) ) · 𝑋 ) = ( 0g ‘ 𝑅 ) )
23 1 2 3 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 1 · 𝑋 ) = 𝑋 )
24 5 6 23 syl2anc ⊢ ( 𝜑 → ( 1 · 𝑋 ) = 𝑋 )
25 24 oveq1d ⊢ ( 𝜑 → ( ( 1 · 𝑋 ) ( +g ‘ 𝑅 ) ( ( 𝑁 ‘ 1 ) · 𝑋 ) ) = ( 𝑋 ( +g ‘ 𝑅 ) ( ( 𝑁 ‘ 1 ) · 𝑋 ) ) )
26 15 22 25 3eqtr3rd ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝑅 ) ( ( 𝑁 ‘ 1 ) · 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
27 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 1 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ 1 ) · 𝑋 ) ∈ 𝐵 )
28 5 12 6 27 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 1 ) · 𝑋 ) ∈ 𝐵 )
29 1 13 16 4 grpinvid1 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( ( 𝑁 ‘ 1 ) · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) = ( ( 𝑁 ‘ 1 ) · 𝑋 ) ↔ ( 𝑋 ( +g ‘ 𝑅 ) ( ( 𝑁 ‘ 1 ) · 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) )
30 10 6 28 29 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) = ( ( 𝑁 ‘ 1 ) · 𝑋 ) ↔ ( 𝑋 ( +g ‘ 𝑅 ) ( ( 𝑁 ‘ 1 ) · 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) )
31 26 30 mpbird ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = ( ( 𝑁 ‘ 1 ) · 𝑋 ) )
32 31 eqcomd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 1 ) · 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )