Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
2 | | unitrrg.u |
. . . . . 6
β’ π = (Unitβπ
) |
3 | 1, 2 | unitcl 20093 |
. . . . 5
β’ (π₯ β π β π₯ β (Baseβπ
)) |
4 | 3 | adantl 483 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β π₯ β (Baseβπ
)) |
5 | | oveq2 7366 |
. . . . . 6
β’ ((π₯(.rβπ
)π¦) = (0gβπ
) β (((invrβπ
)βπ₯)(.rβπ
)(π₯(.rβπ
)π¦)) = (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
))) |
6 | | eqid 2733 |
. . . . . . . . . . 11
β’
(invrβπ
) = (invrβπ
) |
7 | | eqid 2733 |
. . . . . . . . . . 11
β’
(.rβπ
) = (.rβπ
) |
8 | | eqid 2733 |
. . . . . . . . . . 11
β’
(1rβπ
) = (1rβπ
) |
9 | 2, 6, 7, 8 | unitlinv 20111 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π₯ β π) β (((invrβπ
)βπ₯)(.rβπ
)π₯) = (1rβπ
)) |
10 | 9 | adantr 482 |
. . . . . . . . 9
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β (((invrβπ
)βπ₯)(.rβπ
)π₯) = (1rβπ
)) |
11 | 10 | oveq1d 7373 |
. . . . . . . 8
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β ((((invrβπ
)βπ₯)(.rβπ
)π₯)(.rβπ
)π¦) = ((1rβπ
)(.rβπ
)π¦)) |
12 | | simpll 766 |
. . . . . . . . 9
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β π
β Ring) |
13 | 2, 6, 1 | ringinvcl 20110 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π₯ β π) β ((invrβπ
)βπ₯) β (Baseβπ
)) |
14 | 13 | adantr 482 |
. . . . . . . . 9
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β ((invrβπ
)βπ₯) β (Baseβπ
)) |
15 | 4 | adantr 482 |
. . . . . . . . 9
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β π₯ β (Baseβπ
)) |
16 | | simpr 486 |
. . . . . . . . 9
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β π¦ β (Baseβπ
)) |
17 | 1, 7 | ringass 19989 |
. . . . . . . . 9
β’ ((π
β Ring β§
(((invrβπ
)βπ₯) β (Baseβπ
) β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
))) β ((((invrβπ
)βπ₯)(.rβπ
)π₯)(.rβπ
)π¦) = (((invrβπ
)βπ₯)(.rβπ
)(π₯(.rβπ
)π¦))) |
18 | 12, 14, 15, 16, 17 | syl13anc 1373 |
. . . . . . . 8
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β ((((invrβπ
)βπ₯)(.rβπ
)π₯)(.rβπ
)π¦) = (((invrβπ
)βπ₯)(.rβπ
)(π₯(.rβπ
)π¦))) |
19 | 1, 7, 8 | ringlidm 19997 |
. . . . . . . . 9
β’ ((π
β Ring β§ π¦ β (Baseβπ
)) β
((1rβπ
)(.rβπ
)π¦) = π¦) |
20 | 19 | adantlr 714 |
. . . . . . . 8
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β ((1rβπ
)(.rβπ
)π¦) = π¦) |
21 | 11, 18, 20 | 3eqtr3d 2781 |
. . . . . . 7
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β (((invrβπ
)βπ₯)(.rβπ
)(π₯(.rβπ
)π¦)) = π¦) |
22 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
23 | 1, 7, 22 | ringrz 20017 |
. . . . . . . 8
β’ ((π
β Ring β§
((invrβπ
)βπ₯) β (Baseβπ
)) β (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
24 | 12, 14, 23 | syl2anc 585 |
. . . . . . 7
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
25 | 21, 24 | eqeq12d 2749 |
. . . . . 6
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β ((((invrβπ
)βπ₯)(.rβπ
)(π₯(.rβπ
)π¦)) = (((invrβπ
)βπ₯)(.rβπ
)(0gβπ
)) β π¦ = (0gβπ
))) |
26 | 5, 25 | imbitrid 243 |
. . . . 5
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β ((π₯(.rβπ
)π¦) = (0gβπ
) β π¦ = (0gβπ
))) |
27 | 26 | ralrimiva 3140 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) = (0gβπ
) β π¦ = (0gβπ
))) |
28 | | unitrrg.e |
. . . . 5
β’ πΈ = (RLRegβπ
) |
29 | 28, 1, 7, 22 | isrrg 20774 |
. . . 4
β’ (π₯ β πΈ β (π₯ β (Baseβπ
) β§ βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) = (0gβπ
) β π¦ = (0gβπ
)))) |
30 | 4, 27, 29 | sylanbrc 584 |
. . 3
β’ ((π
β Ring β§ π₯ β π) β π₯ β πΈ) |
31 | 30 | ex 414 |
. 2
β’ (π
β Ring β (π₯ β π β π₯ β πΈ)) |
32 | 31 | ssrdv 3951 |
1
β’ (π
β Ring β π β πΈ) |