Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . . . 5
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
2 | 1 | ringmgp 19970 |
. . . 4
β’ (π
β Ring β
(mulGrpβπ
) β
Mnd) |
3 | 2 | 3ad2ant1 1133 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (mulGrpβπ
) β Mnd) |
4 | | ringgrp 19969 |
. . . . 5
β’ (π
β Ring β π
β Grp) |
5 | | invginvrid.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
6 | | invginvrid.u |
. . . . . 6
β’ π = (Unitβπ
) |
7 | 5, 6 | unitcl 20088 |
. . . . 5
β’ (π β π β π β π΅) |
8 | | invginvrid.n |
. . . . . 6
β’ π = (invgβπ
) |
9 | 5, 8 | grpinvcl 18798 |
. . . . 5
β’ ((π
β Grp β§ π β π΅) β (πβπ) β π΅) |
10 | 4, 7, 9 | syl2an 596 |
. . . 4
β’ ((π
β Ring β§ π β π) β (πβπ) β π΅) |
11 | 10 | 3adant2 1131 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (πβπ) β π΅) |
12 | 6, 8 | unitnegcl 20110 |
. . . . 5
β’ ((π
β Ring β§ π β π) β (πβπ) β π) |
13 | | invginvrid.i |
. . . . . 6
β’ πΌ = (invrβπ
) |
14 | 6, 13, 5 | ringinvcl 20105 |
. . . . 5
β’ ((π
β Ring β§ (πβπ) β π) β (πΌβ(πβπ)) β π΅) |
15 | 12, 14 | syldan 591 |
. . . 4
β’ ((π
β Ring β§ π β π) β (πΌβ(πβπ)) β π΅) |
16 | 15 | 3adant2 1131 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (πΌβ(πβπ)) β π΅) |
17 | | simp2 1137 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β π β π΅) |
18 | 1, 5 | mgpbas 19902 |
. . . . 5
β’ π΅ =
(Baseβ(mulGrpβπ
)) |
19 | | invginvrid.t |
. . . . . 6
β’ Β· =
(.rβπ
) |
20 | 1, 19 | mgpplusg 19900 |
. . . . 5
β’ Β· =
(+gβ(mulGrpβπ
)) |
21 | 18, 20 | mndass 18565 |
. . . 4
β’
(((mulGrpβπ
)
β Mnd β§ ((πβπ) β π΅ β§ (πΌβ(πβπ)) β π΅ β§ π β π΅)) β (((πβπ) Β· (πΌβ(πβπ))) Β· π) = ((πβπ) Β· ((πΌβ(πβπ)) Β· π))) |
22 | 21 | eqcomd 2742 |
. . 3
β’
(((mulGrpβπ
)
β Mnd β§ ((πβπ) β π΅ β§ (πΌβ(πβπ)) β π΅ β§ π β π΅)) β ((πβπ) Β· ((πΌβ(πβπ)) Β· π)) = (((πβπ) Β· (πΌβ(πβπ))) Β· π)) |
23 | 3, 11, 16, 17, 22 | syl13anc 1372 |
. 2
β’ ((π
β Ring β§ π β π΅ β§ π β π) β ((πβπ) Β· ((πΌβ(πβπ)) Β· π)) = (((πβπ) Β· (πΌβ(πβπ))) Β· π)) |
24 | | simp1 1136 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β π
β Ring) |
25 | 12 | 3adant2 1131 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (πβπ) β π) |
26 | | eqid 2736 |
. . . . 5
β’
(1rβπ
) = (1rβπ
) |
27 | 6, 13, 19, 26 | unitrinv 20107 |
. . . 4
β’ ((π
β Ring β§ (πβπ) β π) β ((πβπ) Β· (πΌβ(πβπ))) = (1rβπ
)) |
28 | 24, 25, 27 | syl2anc 584 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β ((πβπ) Β· (πΌβ(πβπ))) = (1rβπ
)) |
29 | 28 | oveq1d 7372 |
. 2
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (((πβπ) Β· (πΌβ(πβπ))) Β· π) = ((1rβπ
) Β· π)) |
30 | 5, 19, 26 | ringlidm 19992 |
. . 3
β’ ((π
β Ring β§ π β π΅) β ((1rβπ
) Β· π) = π) |
31 | 30 | 3adant3 1132 |
. 2
β’ ((π
β Ring β§ π β π΅ β§ π β π) β ((1rβπ
) Β· π) = π) |
32 | 23, 29, 31 | 3eqtrd 2780 |
1
β’ ((π
β Ring β§ π β π΅ β§ π β π) β ((πβπ) Β· ((πΌβ(πβπ)) Β· π)) = π) |