Proof of Theorem rngonegmn1r
| Step | Hyp | Ref
| Expression |
| 1 | | ringneg.3 |
. . . . . . . . 9
⊢ 𝑋 = ran 𝐺 |
| 2 | | ringneg.1 |
. . . . . . . . . 10
⊢ 𝐺 = (1st ‘𝑅) |
| 3 | 2 | rneqi 5948 |
. . . . . . . . 9
⊢ ran 𝐺 = ran (1st
‘𝑅) |
| 4 | 1, 3 | eqtri 2765 |
. . . . . . . 8
⊢ 𝑋 = ran (1st
‘𝑅) |
| 5 | | ringneg.2 |
. . . . . . . 8
⊢ 𝐻 = (2nd ‘𝑅) |
| 6 | | ringneg.5 |
. . . . . . . 8
⊢ 𝑈 = (GId‘𝐻) |
| 7 | 4, 5, 6 | rngo1cl 37946 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋) |
| 8 | | ringneg.4 |
. . . . . . . 8
⊢ 𝑁 = (inv‘𝐺) |
| 9 | 2, 1, 8 | rngonegcl 37934 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋) → (𝑁‘𝑈) ∈ 𝑋) |
| 10 | 7, 9 | mpdan 687 |
. . . . . 6
⊢ (𝑅 ∈ RingOps → (𝑁‘𝑈) ∈ 𝑋) |
| 11 | 10 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝑈) ∈ 𝑋) |
| 12 | 7 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → 𝑈 ∈ 𝑋) |
| 13 | 11, 12 | jca 511 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝑈) ∈ 𝑋 ∧ 𝑈 ∈ 𝑋)) |
| 14 | 2, 5, 1 | rngodi 37911 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ (𝑁‘𝑈) ∈ 𝑋 ∧ 𝑈 ∈ 𝑋)) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈))) |
| 15 | 14 | 3exp2 1355 |
. . . . 5
⊢ (𝑅 ∈ RingOps → (𝐴 ∈ 𝑋 → ((𝑁‘𝑈) ∈ 𝑋 → (𝑈 ∈ 𝑋 → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈)))))) |
| 16 | 15 | imp43 427 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ ((𝑁‘𝑈) ∈ 𝑋 ∧ 𝑈 ∈ 𝑋)) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈))) |
| 17 | 13, 16 | mpdan 687 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈))) |
| 18 | | eqid 2737 |
. . . . . . . 8
⊢
(GId‘𝐺) =
(GId‘𝐺) |
| 19 | 2, 1, 8, 18 | rngoaddneg2 37936 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋) → ((𝑁‘𝑈)𝐺𝑈) = (GId‘𝐺)) |
| 20 | 7, 19 | mpdan 687 |
. . . . . 6
⊢ (𝑅 ∈ RingOps → ((𝑁‘𝑈)𝐺𝑈) = (GId‘𝐺)) |
| 21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝑈)𝐺𝑈) = (GId‘𝐺)) |
| 22 | 21 | oveq2d 7447 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = (𝐴𝐻(GId‘𝐺))) |
| 23 | 18, 1, 2, 5 | rngorz 37930 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻(GId‘𝐺)) = (GId‘𝐺)) |
| 24 | 22, 23 | eqtrd 2777 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = (GId‘𝐺)) |
| 25 | 5, 4, 6 | rngoridm 37945 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻𝑈) = 𝐴) |
| 26 | 25 | oveq2d 7447 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴)) |
| 27 | 17, 24, 26 | 3eqtr3rd 2786 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴) = (GId‘𝐺)) |
| 28 | 2, 5, 1 | rngocl 37908 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ (𝑁‘𝑈) ∈ 𝑋) → (𝐴𝐻(𝑁‘𝑈)) ∈ 𝑋) |
| 29 | 11, 28 | mpd3an3 1464 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻(𝑁‘𝑈)) ∈ 𝑋) |
| 30 | 2 | rngogrpo 37917 |
. . . 4
⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp) |
| 31 | 1, 18, 8 | grpoinvid2 30548 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐻(𝑁‘𝑈)) ∈ 𝑋) → ((𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈)) ↔ ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴) = (GId‘𝐺))) |
| 32 | 30, 31 | syl3an1 1164 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐻(𝑁‘𝑈)) ∈ 𝑋) → ((𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈)) ↔ ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴) = (GId‘𝐺))) |
| 33 | 29, 32 | mpd3an3 1464 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈)) ↔ ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴) = (GId‘𝐺))) |
| 34 | 27, 33 | mpbird 257 |
1
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈))) |