Metamath Proof Explorer

Theorem rngonegmn1l

Description: Negation in a ring is the same as left multiplication by -u 1 . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses ringneg.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ringneg.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
ringneg.3 ⊢ 𝑋 = ran 𝐺
ringneg.4 ⊢ 𝑁 = ( inv ‘ 𝐺 )
ringneg.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion rngonegmn1l ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ringneg.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ringneg.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ringneg.3 ⊢ 𝑋 = ran 𝐺
4 ringneg.4 ⊢ 𝑁 = ( inv ‘ 𝐺 )
5 ringneg.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
6 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
7 3 6 eqtri ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
8 7 2 5 rngo1cl ⊢ ( 𝑅 ∈ RingOps → 𝑈 ∈ 𝑋 )
9 1 3 4 rngonegcl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 )
10 8 9 mpdan ⊢ ( 𝑅 ∈ RingOps → ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 )
11 8 10 jca ⊢ ( 𝑅 ∈ RingOps → ( 𝑈 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 ) )
12 1 2 3 rngodir ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑈 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) 𝐻 𝐴 ) = ( ( 𝑈 𝐻 𝐴 ) 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) )
13 12 3exp2 ⊢ ( 𝑅 ∈ RingOps → ( 𝑈 ∈ 𝑋 → ( ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) 𝐻 𝐴 ) = ( ( 𝑈 𝐻 𝐴 ) 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) ) ) ) )
14 13 imp42 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑈 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) 𝐻 𝐴 ) = ( ( 𝑈 𝐻 𝐴 ) 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) )
15 14 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑈 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 ) ) → ( ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) 𝐻 𝐴 ) = ( ( 𝑈 𝐻 𝐴 ) 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) )
16 11 15 mpidan ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) 𝐻 𝐴 ) = ( ( 𝑈 𝐻 𝐴 ) 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) )
17 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
18 1 3 4 17 rngoaddneg1 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋 ) → ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) = ( GId ‘ 𝐺 ) )
19 8 18 mpdan ⊢ ( 𝑅 ∈ RingOps → ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) = ( GId ‘ 𝐺 ) )
20 19 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) = ( GId ‘ 𝐺 ) )
21 20 oveq1d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) 𝐻 𝐴 ) = ( ( GId ‘ 𝐺 ) 𝐻 𝐴 ) )
22 17 3 1 2 rngolz ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐻 𝐴 ) = ( GId ‘ 𝐺 ) )
23 21 22 eqtrd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐺 ( 𝑁 ‘ 𝑈 ) ) 𝐻 𝐴 ) = ( GId ‘ 𝐺 ) )
24 2 7 5 rngolidm ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑈 𝐻 𝐴 ) = 𝐴 )
25 24 oveq1d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐻 𝐴 ) 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) = ( 𝐴 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) )
26 16 23 25 3eqtr3rd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) = ( GId ‘ 𝐺 ) )
27 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ∈ 𝑋 )
28 27 3expa ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ∈ 𝑋 )
29 28 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ∈ 𝑋 )
30 10 29 mpidan ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ∈ 𝑋 )
31 1 rngogrpo ⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )
32 3 17 4 grpoinvid1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ↔ ( 𝐴 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) = ( GId ‘ 𝐺 ) ) )
33 31 32 syl3an1 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ↔ ( 𝐴 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) = ( GId ‘ 𝐺 ) ) )
34 30 33 mpd3an3 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ↔ ( 𝐴 𝐺 ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) ) = ( GId ‘ 𝐺 ) ) )
35 26 34 mpbird ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( ( 𝑁 ‘ 𝑈 ) 𝐻 𝐴 ) )