Step | Hyp | Ref
| Expression |
1 | | ringnegmul.3 |
. . . . . . 7
β’ π = ran πΊ |
2 | | ringnegmul.1 |
. . . . . . . 8
β’ πΊ = (1st βπ
) |
3 | 2 | rneqi 5896 |
. . . . . . 7
β’ ran πΊ = ran (1st
βπ
) |
4 | 1, 3 | eqtri 2761 |
. . . . . 6
β’ π = ran (1st
βπ
) |
5 | | ringnegmul.2 |
. . . . . 6
β’ π» = (2nd βπ
) |
6 | | eqid 2733 |
. . . . . 6
β’
(GIdβπ») =
(GIdβπ») |
7 | 4, 5, 6 | rngo1cl 36448 |
. . . . 5
β’ (π
β RingOps β
(GIdβπ») β π) |
8 | | ringnegmul.4 |
. . . . . 6
β’ π = (invβπΊ) |
9 | 2, 1, 8 | rngonegcl 36436 |
. . . . 5
β’ ((π
β RingOps β§
(GIdβπ») β π) β (πβ(GIdβπ»)) β π) |
10 | 7, 9 | mpdan 686 |
. . . 4
β’ (π
β RingOps β (πβ(GIdβπ»)) β π) |
11 | 2, 5, 1 | rngoass 36415 |
. . . . . . 7
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ (πβ(GIdβπ»)) β π)) β ((π΄π»π΅)π»(πβ(GIdβπ»))) = (π΄π»(π΅π»(πβ(GIdβπ»))))) |
12 | 11 | 3exp2 1355 |
. . . . . 6
β’ (π
β RingOps β (π΄ β π β (π΅ β π β ((πβ(GIdβπ»)) β π β ((π΄π»π΅)π»(πβ(GIdβπ»))) = (π΄π»(π΅π»(πβ(GIdβπ»)))))))) |
13 | 12 | com24 95 |
. . . . 5
β’ (π
β RingOps β ((πβ(GIdβπ»)) β π β (π΅ β π β (π΄ β π β ((π΄π»π΅)π»(πβ(GIdβπ»))) = (π΄π»(π΅π»(πβ(GIdβπ»)))))))) |
14 | 13 | com34 91 |
. . . 4
β’ (π
β RingOps β ((πβ(GIdβπ»)) β π β (π΄ β π β (π΅ β π β ((π΄π»π΅)π»(πβ(GIdβπ»))) = (π΄π»(π΅π»(πβ(GIdβπ»)))))))) |
15 | 10, 14 | mpd 15 |
. . 3
β’ (π
β RingOps β (π΄ β π β (π΅ β π β ((π΄π»π΅)π»(πβ(GIdβπ»))) = (π΄π»(π΅π»(πβ(GIdβπ»))))))) |
16 | 15 | 3imp 1112 |
. 2
β’ ((π
β RingOps β§ π΄ β π β§ π΅ β π) β ((π΄π»π΅)π»(πβ(GIdβπ»))) = (π΄π»(π΅π»(πβ(GIdβπ»))))) |
17 | 2, 5, 1 | rngocl 36410 |
. . . . 5
β’ ((π
β RingOps β§ π΄ β π β§ π΅ β π) β (π΄π»π΅) β π) |
18 | 17 | 3expb 1121 |
. . . 4
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π)) β (π΄π»π΅) β π) |
19 | 2, 5, 1, 8, 6 | rngonegmn1r 36451 |
. . . 4
β’ ((π
β RingOps β§ (π΄π»π΅) β π) β (πβ(π΄π»π΅)) = ((π΄π»π΅)π»(πβ(GIdβπ»)))) |
20 | 18, 19 | syldan 592 |
. . 3
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π)) β (πβ(π΄π»π΅)) = ((π΄π»π΅)π»(πβ(GIdβπ»)))) |
21 | 20 | 3impb 1116 |
. 2
β’ ((π
β RingOps β§ π΄ β π β§ π΅ β π) β (πβ(π΄π»π΅)) = ((π΄π»π΅)π»(πβ(GIdβπ»)))) |
22 | 2, 5, 1, 8, 6 | rngonegmn1r 36451 |
. . . 4
β’ ((π
β RingOps β§ π΅ β π) β (πβπ΅) = (π΅π»(πβ(GIdβπ»)))) |
23 | 22 | 3adant2 1132 |
. . 3
β’ ((π
β RingOps β§ π΄ β π β§ π΅ β π) β (πβπ΅) = (π΅π»(πβ(GIdβπ»)))) |
24 | 23 | oveq2d 7377 |
. 2
β’ ((π
β RingOps β§ π΄ β π β§ π΅ β π) β (π΄π»(πβπ΅)) = (π΄π»(π΅π»(πβ(GIdβπ»))))) |
25 | 16, 21, 24 | 3eqtr4d 2783 |
1
β’ ((π
β RingOps β§ π΄ β π β§ π΅ β π) β (πβ(π΄π»π΅)) = (π΄π»(πβπ΅))) |