Proof of Theorem rngonegmn1r
Step | Hyp | Ref
| Expression |
1 | | ringneg.3 |
. . . . . . . . 9
⊢ 𝑋 = ran 𝐺 |
2 | | ringneg.1 |
. . . . . . . . . 10
⊢ 𝐺 = (1st ‘𝑅) |
3 | 2 | rneqi 5806 |
. . . . . . . . 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 35834 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋) |
8 | | ringneg.4 |
. . . . . . . 8
⊢ 𝑁 = (inv‘𝐺) |
9 | 2, 1, 8 | rngonegcl 35822 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋) → (𝑁‘𝑈) ∈ 𝑋) |
10 | 7, 9 | mpdan 687 |
. . . . . 6
⊢ (𝑅 ∈ RingOps → (𝑁‘𝑈) ∈ 𝑋) |
11 | 10 | adantr 484 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝑈) ∈ 𝑋) |
12 | 7 | adantr 484 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → 𝑈 ∈ 𝑋) |
13 | 11, 12 | jca 515 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝑈) ∈ 𝑋 ∧ 𝑈 ∈ 𝑋)) |
14 | 2, 5, 1 | rngodi 35799 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ (𝑁‘𝑈) ∈ 𝑋 ∧ 𝑈 ∈ 𝑋)) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈))) |
15 | 14 | 3exp2 1356 |
. . . . 5
⊢ (𝑅 ∈ RingOps → (𝐴 ∈ 𝑋 → ((𝑁‘𝑈) ∈ 𝑋 → (𝑈 ∈ 𝑋 → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈)))))) |
16 | 15 | imp43 431 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ ((𝑁‘𝑈) ∈ 𝑋 ∧ 𝑈 ∈ 𝑋)) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈))) |
17 | 13, 16 | mpdan 687 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈))) |
18 | | eqid 2737 |
. . . . . . . 8
⊢
(GId‘𝐺) =
(GId‘𝐺) |
19 | 2, 1, 8, 18 | rngoaddneg2 35824 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋) → ((𝑁‘𝑈)𝐺𝑈) = (GId‘𝐺)) |
20 | 7, 19 | mpdan 687 |
. . . . . 6
⊢ (𝑅 ∈ RingOps → ((𝑁‘𝑈)𝐺𝑈) = (GId‘𝐺)) |
21 | 20 | adantr 484 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝑈)𝐺𝑈) = (GId‘𝐺)) |
22 | 21 | oveq2d 7229 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = (𝐴𝐻(GId‘𝐺))) |
23 | 18, 1, 2, 5 | rngorz 35818 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻(GId‘𝐺)) = (GId‘𝐺)) |
24 | 22, 23 | eqtrd 2777 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻((𝑁‘𝑈)𝐺𝑈)) = (GId‘𝐺)) |
25 | 5, 4, 6 | rngoridm 35833 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻𝑈) = 𝐴) |
26 | 25 | oveq2d 7229 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝐴𝐻(𝑁‘𝑈))𝐺(𝐴𝐻𝑈)) = ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴)) |
27 | 17, 24, 26 | 3eqtr3rd 2786 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴) = (GId‘𝐺)) |
28 | 2, 5, 1 | rngocl 35796 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ (𝑁‘𝑈) ∈ 𝑋) → (𝐴𝐻(𝑁‘𝑈)) ∈ 𝑋) |
29 | 11, 28 | mpd3an3 1464 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻(𝑁‘𝑈)) ∈ 𝑋) |
30 | 2 | rngogrpo 35805 |
. . . 4
⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp) |
31 | 1, 18, 8 | grpoinvid2 28610 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐻(𝑁‘𝑈)) ∈ 𝑋) → ((𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈)) ↔ ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴) = (GId‘𝐺))) |
32 | 30, 31 | syl3an1 1165 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐻(𝑁‘𝑈)) ∈ 𝑋) → ((𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈)) ↔ ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴) = (GId‘𝐺))) |
33 | 29, 32 | mpd3an3 1464 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈)) ↔ ((𝐴𝐻(𝑁‘𝑈))𝐺𝐴) = (GId‘𝐺))) |
34 | 27, 33 | mpbird 260 |
1
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈))) |