Step | Hyp | Ref
| Expression |
1 | | subrgugrp.1 |
. . . 4
β’ π = (π
βΎs π΄) |
2 | | subrgugrp.2 |
. . . 4
β’ π = (Unitβπ
) |
3 | | subrgugrp.3 |
. . . 4
β’ π = (Unitβπ) |
4 | 1, 2, 3 | subrguss 13295 |
. . 3
β’ (π΄ β (SubRingβπ
) β π β π) |
5 | | subrgrcl 13285 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
6 | 2 | a1i 9 |
. . . . 5
β’ (π
β Ring β π = (Unitβπ
)) |
7 | | subrgugrp.4 |
. . . . . 6
β’ πΊ = ((mulGrpβπ
) βΎs π) |
8 | 7 | a1i 9 |
. . . . 5
β’ (π
β Ring β πΊ = ((mulGrpβπ
) βΎs π)) |
9 | | ringsrg 13155 |
. . . . 5
β’ (π
β Ring β π
β SRing) |
10 | 6, 8, 9 | unitgrpbasd 13215 |
. . . 4
β’ (π
β Ring β π = (BaseβπΊ)) |
11 | 5, 10 | syl 14 |
. . 3
β’ (π΄ β (SubRingβπ
) β π = (BaseβπΊ)) |
12 | 4, 11 | sseqtrd 3193 |
. 2
β’ (π΄ β (SubRingβπ
) β π β (BaseβπΊ)) |
13 | 1 | subrgring 13283 |
. . 3
β’ (π΄ β (SubRingβπ
) β π β Ring) |
14 | | eqid 2177 |
. . . 4
β’
(1rβπ) = (1rβπ) |
15 | 3, 14 | 1unit 13207 |
. . 3
β’ (π β Ring β
(1rβπ)
β π) |
16 | | elex2 2753 |
. . 3
β’
((1rβπ) β π β βπ€ π€ β π) |
17 | 13, 15, 16 | 3syl 17 |
. 2
β’ (π΄ β (SubRingβπ
) β βπ€ π€ β π) |
18 | | eqid 2177 |
. . . . . . . . . . . 12
β’
(.rβπ
) = (.rβπ
) |
19 | 1, 18 | ressmulrg 12595 |
. . . . . . . . . . 11
β’ ((π΄ β (SubRingβπ
) β§ π
β Ring) β
(.rβπ
) =
(.rβπ)) |
20 | 5, 19 | mpdan 421 |
. . . . . . . . . 10
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
21 | 20 | 3ad2ant1 1018 |
. . . . . . . . 9
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (.rβπ
) = (.rβπ)) |
22 | 21 | oveqd 5889 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ
)π¦) = (π₯(.rβπ)π¦)) |
23 | | eqid 2177 |
. . . . . . . . . 10
β’
(.rβπ) = (.rβπ) |
24 | 3, 23 | unitmulcl 13213 |
. . . . . . . . 9
β’ ((π β Ring β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ)π¦) β π) |
25 | 13, 24 | syl3an1 1271 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ)π¦) β π) |
26 | 22, 25 | eqeltrd 2254 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ
)π¦) β π) |
27 | 26 | 3expa 1203 |
. . . . . 6
β’ (((π΄ β (SubRingβπ
) β§ π₯ β π) β§ π¦ β π) β (π₯(.rβπ
)π¦) β π) |
28 | 27 | ralrimiva 2550 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β βπ¦ β π (π₯(.rβπ
)π¦) β π) |
29 | | eqid 2177 |
. . . . . . 7
β’
(invrβπ
) = (invrβπ
) |
30 | | eqid 2177 |
. . . . . . 7
β’
(invrβπ) = (invrβπ) |
31 | 1, 29, 3, 30 | subrginv 13296 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β ((invrβπ
)βπ₯) = ((invrβπ)βπ₯)) |
32 | 3, 30 | unitinvcl 13223 |
. . . . . . 7
β’ ((π β Ring β§ π₯ β π) β ((invrβπ)βπ₯) β π) |
33 | 13, 32 | sylan 283 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β ((invrβπ)βπ₯) β π) |
34 | 31, 33 | eqeltrd 2254 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β ((invrβπ
)βπ₯) β π) |
35 | 28, 34 | jca 306 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (βπ¦ β π (π₯(.rβπ
)π¦) β π β§ ((invrβπ
)βπ₯) β π)) |
36 | 35 | ralrimiva 2550 |
. . 3
β’ (π΄ β (SubRingβπ
) β βπ₯ β π (βπ¦ β π (π₯(.rβπ
)π¦) β π β§ ((invrβπ
)βπ₯) β π)) |
37 | | eqid 2177 |
. . . . . . . . . . 11
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
38 | 37, 18 | mgpplusgg 13065 |
. . . . . . . . . 10
β’ (π
β Ring β
(.rβπ
) =
(+gβ(mulGrpβπ
))) |
39 | | basfn 12512 |
. . . . . . . . . . . 12
β’ Base Fn
V |
40 | | elex 2748 |
. . . . . . . . . . . 12
β’ (π
β Ring β π
β V) |
41 | | funfvex 5531 |
. . . . . . . . . . . . 13
β’ ((Fun
Base β§ π
β dom
Base) β (Baseβπ
)
β V) |
42 | 41 | funfni 5315 |
. . . . . . . . . . . 12
β’ ((Base Fn
V β§ π
β V) β
(Baseβπ
) β
V) |
43 | 39, 40, 42 | sylancr 414 |
. . . . . . . . . . 11
β’ (π
β Ring β
(Baseβπ
) β
V) |
44 | | eqidd 2178 |
. . . . . . . . . . . 12
β’ (π
β Ring β
(Baseβπ
) =
(Baseβπ
)) |
45 | 44, 6, 9 | unitssd 13209 |
. . . . . . . . . . 11
β’ (π
β Ring β π β (Baseβπ
)) |
46 | 43, 45 | ssexd 4142 |
. . . . . . . . . 10
β’ (π
β Ring β π β V) |
47 | 37 | ringmgp 13116 |
. . . . . . . . . 10
β’ (π
β Ring β
(mulGrpβπ
) β
Mnd) |
48 | 8, 38, 46, 47 | ressplusgd 12579 |
. . . . . . . . 9
β’ (π
β Ring β
(.rβπ
) =
(+gβπΊ)) |
49 | 5, 48 | syl 14 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(+gβπΊ)) |
50 | 49 | oveqd 5889 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β (π₯(.rβπ
)π¦) = (π₯(+gβπΊ)π¦)) |
51 | 50 | eleq1d 2246 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β ((π₯(.rβπ
)π¦) β π β (π₯(+gβπΊ)π¦) β π)) |
52 | 51 | ralbidv 2477 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β (βπ¦ β π (π₯(.rβπ
)π¦) β π β βπ¦ β π (π₯(+gβπΊ)π¦) β π)) |
53 | 2 | a1i 9 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β π = (Unitβπ
)) |
54 | 7 | a1i 9 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β πΊ = ((mulGrpβπ
) βΎs π)) |
55 | | eqidd 2178 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β
(invrβπ
) =
(invrβπ
)) |
56 | 53, 54, 55, 5 | invrfvald 13222 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β
(invrβπ
) =
(invgβπΊ)) |
57 | 56 | fveq1d 5516 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β
((invrβπ
)βπ₯) = ((invgβπΊ)βπ₯)) |
58 | 57 | eleq1d 2246 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β
(((invrβπ
)βπ₯) β π β ((invgβπΊ)βπ₯) β π)) |
59 | 52, 58 | anbi12d 473 |
. . . 4
β’ (π΄ β (SubRingβπ
) β ((βπ¦ β π (π₯(.rβπ
)π¦) β π β§ ((invrβπ
)βπ₯) β π) β (βπ¦ β π (π₯(+gβπΊ)π¦) β π β§ ((invgβπΊ)βπ₯) β π))) |
60 | 59 | ralbidv 2477 |
. . 3
β’ (π΄ β (SubRingβπ
) β (βπ₯ β π (βπ¦ β π (π₯(.rβπ
)π¦) β π β§ ((invrβπ
)βπ₯) β π) β βπ₯ β π (βπ¦ β π (π₯(+gβπΊ)π¦) β π β§ ((invgβπΊ)βπ₯) β π))) |
61 | 36, 60 | mpbid 147 |
. 2
β’ (π΄ β (SubRingβπ
) β βπ₯ β π (βπ¦ β π (π₯(+gβπΊ)π¦) β π β§ ((invgβπΊ)βπ₯) β π)) |
62 | 2, 7 | unitgrp 13216 |
. . 3
β’ (π
β Ring β πΊ β Grp) |
63 | | eqid 2177 |
. . . 4
β’
(BaseβπΊ) =
(BaseβπΊ) |
64 | | eqid 2177 |
. . . 4
β’
(+gβπΊ) = (+gβπΊ) |
65 | | eqid 2177 |
. . . 4
β’
(invgβπΊ) = (invgβπΊ) |
66 | 63, 64, 65 | issubg2m 12980 |
. . 3
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β (BaseβπΊ) β§ βπ€ π€ β π β§ βπ₯ β π (βπ¦ β π (π₯(+gβπΊ)π¦) β π β§ ((invgβπΊ)βπ₯) β π)))) |
67 | 5, 62, 66 | 3syl 17 |
. 2
β’ (π΄ β (SubRingβπ
) β (π β (SubGrpβπΊ) β (π β (BaseβπΊ) β§ βπ€ π€ β π β§ βπ₯ β π (βπ¦ β π (π₯(+gβπΊ)π¦) β π β§ ((invgβπΊ)βπ₯) β π)))) |
68 | 12, 17, 61, 67 | mpbir3and 1180 |
1
β’ (π΄ β (SubRingβπ
) β π β (SubGrpβπΊ)) |