Step | Hyp | Ref
| Expression |
1 | | subrgugrp.1 |
. . 3
β’ π = (π
βΎs π΄) |
2 | | subrgugrp.2 |
. . 3
β’ π = (Unitβπ
) |
3 | | subrgugrp.3 |
. . 3
β’ π = (Unitβπ) |
4 | 1, 2, 3 | subrguss 20279 |
. 2
β’ (π΄ β (SubRingβπ
) β π β π) |
5 | 1 | subrgring 20267 |
. . 3
β’ (π΄ β (SubRingβπ
) β π β Ring) |
6 | | eqid 2733 |
. . . 4
β’
(1rβπ) = (1rβπ) |
7 | 3, 6 | 1unit 20095 |
. . 3
β’ (π β Ring β
(1rβπ)
β π) |
8 | | ne0i 4298 |
. . 3
β’
((1rβπ) β π β π β β
) |
9 | 5, 7, 8 | 3syl 18 |
. 2
β’ (π΄ β (SubRingβπ
) β π β β
) |
10 | | eqid 2733 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
11 | 1, 10 | ressmulr 17196 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (.rβπ
) = (.rβπ)) |
13 | 12 | oveqd 7378 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ
)π¦) = (π₯(.rβπ)π¦)) |
14 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
15 | 3, 14 | unitmulcl 20101 |
. . . . . . . 8
β’ ((π β Ring β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ)π¦) β π) |
16 | 5, 15 | syl3an1 1164 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ)π¦) β π) |
17 | 13, 16 | eqeltrd 2834 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ
)π¦) β π) |
18 | 17 | 3expa 1119 |
. . . . 5
β’ (((π΄ β (SubRingβπ
) β§ π₯ β π) β§ π¦ β π) β (π₯(.rβπ
)π¦) β π) |
19 | 18 | ralrimiva 3140 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β βπ¦ β π (π₯(.rβπ
)π¦) β π) |
20 | | eqid 2733 |
. . . . . 6
β’
(invrβπ
) = (invrβπ
) |
21 | | eqid 2733 |
. . . . . 6
β’
(invrβπ) = (invrβπ) |
22 | 1, 20, 3, 21 | subrginv 20280 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β ((invrβπ
)βπ₯) = ((invrβπ)βπ₯)) |
23 | 3, 21 | unitinvcl 20111 |
. . . . . 6
β’ ((π β Ring β§ π₯ β π) β ((invrβπ)βπ₯) β π) |
24 | 5, 23 | sylan 581 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β ((invrβπ)βπ₯) β π) |
25 | 22, 24 | eqeltrd 2834 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β ((invrβπ
)βπ₯) β π) |
26 | 19, 25 | jca 513 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (βπ¦ β π (π₯(.rβπ
)π¦) β π β§ ((invrβπ
)βπ₯) β π)) |
27 | 26 | ralrimiva 3140 |
. 2
β’ (π΄ β (SubRingβπ
) β βπ₯ β π (βπ¦ β π (π₯(.rβπ
)π¦) β π β§ ((invrβπ
)βπ₯) β π)) |
28 | | subrgrcl 20269 |
. . 3
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
29 | | subrgugrp.4 |
. . . 4
β’ πΊ = ((mulGrpβπ
) βΎs π) |
30 | 2, 29 | unitgrp 20104 |
. . 3
β’ (π
β Ring β πΊ β Grp) |
31 | 2, 29 | unitgrpbas 20103 |
. . . 4
β’ π = (BaseβπΊ) |
32 | 2 | fvexi 6860 |
. . . . 5
β’ π β V |
33 | | eqid 2733 |
. . . . . . 7
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
34 | 33, 10 | mgpplusg 19908 |
. . . . . 6
β’
(.rβπ
) = (+gβ(mulGrpβπ
)) |
35 | 29, 34 | ressplusg 17179 |
. . . . 5
β’ (π β V β
(.rβπ
) =
(+gβπΊ)) |
36 | 32, 35 | ax-mp 5 |
. . . 4
β’
(.rβπ
) = (+gβπΊ) |
37 | 2, 29, 20 | invrfval 20110 |
. . . 4
β’
(invrβπ
) = (invgβπΊ) |
38 | 31, 36, 37 | issubg2 18951 |
. . 3
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β π β§ π β β
β§ βπ₯ β π (βπ¦ β π (π₯(.rβπ
)π¦) β π β§ ((invrβπ
)βπ₯) β π)))) |
39 | 28, 30, 38 | 3syl 18 |
. 2
β’ (π΄ β (SubRingβπ
) β (π β (SubGrpβπΊ) β (π β π β§ π β β
β§ βπ₯ β π (βπ¦ β π (π₯(.rβπ
)π¦) β π β§ ((invrβπ
)βπ₯) β π)))) |
40 | 4, 9, 27, 39 | mpbir3and 1343 |
1
β’ (π΄ β (SubRingβπ
) β π β (SubGrpβπΊ)) |