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 ⊢ G = 1 st ⁡ R
ringneg.2 ⊢ H = 2 nd ⁡ R
ringneg.3 ⊢ X = ran ⁡ G
ringneg.4 ⊢ N = inv ⁡ G
ringneg.5 ⊢ U = GId ⁡ H
Assertion rngonegmn1l ⊢ R ∈ RingOps ∧ A ∈ X → N ⁡ A = N ⁡ U H A

Proof

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