Step | Hyp | Ref
| Expression |
1 | | ringneg.3 |
. . . . . . 7
β’ π = ran πΊ |
2 | | ringneg.1 |
. . . . . . . 8
β’ πΊ = (1st βπ
) |
3 | 2 | rneqi 5937 |
. . . . . . 7
β’ ran πΊ = ran (1st
βπ
) |
4 | 1, 3 | eqtri 2761 |
. . . . . 6
β’ π = ran (1st
βπ
) |
5 | | ringneg.2 |
. . . . . 6
β’ π» = (2nd βπ
) |
6 | | ringneg.5 |
. . . . . 6
β’ π = (GIdβπ») |
7 | 4, 5, 6 | rngo1cl 36807 |
. . . . 5
β’ (π
β RingOps β π β π) |
8 | | ringneg.4 |
. . . . . . 7
β’ π = (invβπΊ) |
9 | 2, 1, 8 | rngonegcl 36795 |
. . . . . 6
β’ ((π
β RingOps β§ π β π) β (πβπ) β π) |
10 | 7, 9 | mpdan 686 |
. . . . 5
β’ (π
β RingOps β (πβπ) β π) |
11 | 7, 10 | jca 513 |
. . . 4
β’ (π
β RingOps β (π β π β§ (πβπ) β π)) |
12 | 2, 5, 1 | rngodir 36773 |
. . . . . . 7
β’ ((π
β RingOps β§ (π β π β§ (πβπ) β π β§ π΄ β π)) β ((ππΊ(πβπ))π»π΄) = ((ππ»π΄)πΊ((πβπ)π»π΄))) |
13 | 12 | 3exp2 1355 |
. . . . . 6
β’ (π
β RingOps β (π β π β ((πβπ) β π β (π΄ β π β ((ππΊ(πβπ))π»π΄) = ((ππ»π΄)πΊ((πβπ)π»π΄)))))) |
14 | 13 | imp42 428 |
. . . . 5
β’ (((π
β RingOps β§ (π β π β§ (πβπ) β π)) β§ π΄ β π) β ((ππΊ(πβπ))π»π΄) = ((ππ»π΄)πΊ((πβπ)π»π΄))) |
15 | 14 | an32s 651 |
. . . 4
β’ (((π
β RingOps β§ π΄ β π) β§ (π β π β§ (πβπ) β π)) β ((ππΊ(πβπ))π»π΄) = ((ππ»π΄)πΊ((πβπ)π»π΄))) |
16 | 11, 15 | mpidan 688 |
. . 3
β’ ((π
β RingOps β§ π΄ β π) β ((ππΊ(πβπ))π»π΄) = ((ππ»π΄)πΊ((πβπ)π»π΄))) |
17 | | eqid 2733 |
. . . . . . . 8
β’
(GIdβπΊ) =
(GIdβπΊ) |
18 | 2, 1, 8, 17 | rngoaddneg1 36796 |
. . . . . . 7
β’ ((π
β RingOps β§ π β π) β (ππΊ(πβπ)) = (GIdβπΊ)) |
19 | 7, 18 | mpdan 686 |
. . . . . 6
β’ (π
β RingOps β (ππΊ(πβπ)) = (GIdβπΊ)) |
20 | 19 | adantr 482 |
. . . . 5
β’ ((π
β RingOps β§ π΄ β π) β (ππΊ(πβπ)) = (GIdβπΊ)) |
21 | 20 | oveq1d 7424 |
. . . 4
β’ ((π
β RingOps β§ π΄ β π) β ((ππΊ(πβπ))π»π΄) = ((GIdβπΊ)π»π΄)) |
22 | 17, 1, 2, 5 | rngolz 36790 |
. . . 4
β’ ((π
β RingOps β§ π΄ β π) β ((GIdβπΊ)π»π΄) = (GIdβπΊ)) |
23 | 21, 22 | eqtrd 2773 |
. . 3
β’ ((π
β RingOps β§ π΄ β π) β ((ππΊ(πβπ))π»π΄) = (GIdβπΊ)) |
24 | 5, 4, 6 | rngolidm 36805 |
. . . 4
β’ ((π
β RingOps β§ π΄ β π) β (ππ»π΄) = π΄) |
25 | 24 | oveq1d 7424 |
. . 3
β’ ((π
β RingOps β§ π΄ β π) β ((ππ»π΄)πΊ((πβπ)π»π΄)) = (π΄πΊ((πβπ)π»π΄))) |
26 | 16, 23, 25 | 3eqtr3rd 2782 |
. 2
β’ ((π
β RingOps β§ π΄ β π) β (π΄πΊ((πβπ)π»π΄)) = (GIdβπΊ)) |
27 | 2, 5, 1 | rngocl 36769 |
. . . . . 6
β’ ((π
β RingOps β§ (πβπ) β π β§ π΄ β π) β ((πβπ)π»π΄) β π) |
28 | 27 | 3expa 1119 |
. . . . 5
β’ (((π
β RingOps β§ (πβπ) β π) β§ π΄ β π) β ((πβπ)π»π΄) β π) |
29 | 28 | an32s 651 |
. . . 4
β’ (((π
β RingOps β§ π΄ β π) β§ (πβπ) β π) β ((πβπ)π»π΄) β π) |
30 | 10, 29 | mpidan 688 |
. . 3
β’ ((π
β RingOps β§ π΄ β π) β ((πβπ)π»π΄) β π) |
31 | 2 | rngogrpo 36778 |
. . . 4
β’ (π
β RingOps β πΊ β GrpOp) |
32 | 1, 17, 8 | grpoinvid1 29781 |
. . . 4
β’ ((πΊ β GrpOp β§ π΄ β π β§ ((πβπ)π»π΄) β π) β ((πβπ΄) = ((πβπ)π»π΄) β (π΄πΊ((πβπ)π»π΄)) = (GIdβπΊ))) |
33 | 31, 32 | syl3an1 1164 |
. . 3
β’ ((π
β RingOps β§ π΄ β π β§ ((πβπ)π»π΄) β π) β ((πβπ΄) = ((πβπ)π»π΄) β (π΄πΊ((πβπ)π»π΄)) = (GIdβπΊ))) |
34 | 30, 33 | mpd3an3 1463 |
. 2
β’ ((π
β RingOps β§ π΄ β π) β ((πβπ΄) = ((πβπ)π»π΄) β (π΄πΊ((πβπ)π»π΄)) = (GIdβπΊ))) |
35 | 26, 34 | mpbird 257 |
1
β’ ((π
β RingOps β§ π΄ β π) β (πβπ΄) = ((πβπ)π»π΄)) |