Step | Hyp | Ref
| Expression |
1 | | subrguss.3 |
. . . . . . . . 9
β’ π = (Unitβπ) |
2 | 1 | a1i 9 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β π = (Unitβπ)) |
3 | | eqidd 2178 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β
(1rβπ) =
(1rβπ)) |
4 | | eqidd 2178 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β
(β₯rβπ) = (β₯rβπ)) |
5 | | eqidd 2178 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β
(opprβπ) = (opprβπ)) |
6 | | eqidd 2178 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β
(β₯rβ(opprβπ)) =
(β₯rβ(opprβπ))) |
7 | | subrguss.1 |
. . . . . . . . . 10
β’ π = (π
βΎs π΄) |
8 | 7 | subrgring 13283 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β π β Ring) |
9 | | ringsrg 13155 |
. . . . . . . . 9
β’ (π β Ring β π β SRing) |
10 | 8, 9 | syl 14 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β π β SRing) |
11 | 2, 3, 4, 5, 6, 10 | isunitd 13206 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β (π₯ β π β (π₯(β₯rβπ)(1rβπ) β§ π₯(β₯rβ(opprβπ))(1rβπ)))) |
12 | 11 | simprbda 383 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π₯(β₯rβπ)(1rβπ)) |
13 | | eqid 2177 |
. . . . . . . 8
β’
(1rβπ
) = (1rβπ
) |
14 | 7, 13 | subrg1 13290 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β
(1rβπ
) =
(1rβπ)) |
15 | 14 | adantr 276 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (1rβπ
) = (1rβπ)) |
16 | 12, 15 | breqtrrd 4030 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π₯(β₯rβπ)(1rβπ
)) |
17 | | eqid 2177 |
. . . . . . . 8
β’
(β₯rβπ
) = (β₯rβπ
) |
18 | | eqid 2177 |
. . . . . . . 8
β’
(β₯rβπ) = (β₯rβπ) |
19 | 7, 17, 18 | subrgdvds 13294 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β
(β₯rβπ) β (β₯rβπ
)) |
20 | 19 | adantr 276 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (β₯rβπ) β
(β₯rβπ
)) |
21 | 20 | ssbrd 4045 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (π₯(β₯rβπ)(1rβπ
) β π₯(β₯rβπ
)(1rβπ
))) |
22 | 16, 21 | mpd 13 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π₯(β₯rβπ
)(1rβπ
)) |
23 | | subrgrcl 13285 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
24 | 23 | adantr 276 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π
β Ring) |
25 | | eqid 2177 |
. . . . . . . 8
β’
(opprβπ
) = (opprβπ
) |
26 | | eqid 2177 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
27 | 25, 26 | opprbasg 13178 |
. . . . . . 7
β’ (π
β Ring β
(Baseβπ
) =
(Baseβ(opprβπ
))) |
28 | 24, 27 | syl 14 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (Baseβπ
) =
(Baseβ(opprβπ
))) |
29 | | eqidd 2178 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
))) |
30 | 25 | opprring 13180 |
. . . . . . 7
β’ (π
β Ring β
(opprβπ
) β Ring) |
31 | | ringsrg 13155 |
. . . . . . 7
β’
((opprβπ
) β Ring β
(opprβπ
) β SRing) |
32 | 24, 30, 31 | 3syl 17 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (opprβπ
) β SRing) |
33 | | eqidd 2178 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β
(.rβ(opprβπ
)) =
(.rβ(opprβπ
))) |
34 | 7 | subrgbas 13289 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β π΄ = (Baseβπ)) |
35 | 34 | adantr 276 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π΄ = (Baseβπ)) |
36 | 26 | subrgss 13281 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β π΄ β (Baseβπ
)) |
37 | 36 | adantr 276 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π΄ β (Baseβπ
)) |
38 | 35, 37 | eqsstrrd 3192 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (Baseβπ) β (Baseβπ
)) |
39 | | eqidd 2178 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (Baseβπ) = (Baseβπ)) |
40 | 1 | a1i 9 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π = (Unitβπ)) |
41 | 10 | adantr 276 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π β SRing) |
42 | | simpr 110 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π₯ β π) |
43 | 39, 40, 41, 42 | unitcld 13208 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π₯ β (Baseβπ)) |
44 | 38, 43 | sseldd 3156 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π₯ β (Baseβπ
)) |
45 | | eqid 2177 |
. . . . . . . . 9
β’
(invrβπ) = (invrβπ) |
46 | | eqid 2177 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
47 | 1, 45, 46 | ringinvcl 13225 |
. . . . . . . 8
β’ ((π β Ring β§ π₯ β π) β ((invrβπ)βπ₯) β (Baseβπ)) |
48 | 8, 47 | sylan 283 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β ((invrβπ)βπ₯) β (Baseβπ)) |
49 | 38, 48 | sseldd 3156 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β ((invrβπ)βπ₯) β (Baseβπ
)) |
50 | 28, 29, 32, 33, 44, 49 | dvdsrmuld 13196 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π₯(β₯rβ(opprβπ
))(((invrβπ)βπ₯)(.rβ(opprβπ
))π₯)) |
51 | 1, 45 | unitinvcl 13223 |
. . . . . . . 8
β’ ((π β Ring β§ π₯ β π) β ((invrβπ)βπ₯) β π) |
52 | 8, 51 | sylan 283 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β ((invrβπ)βπ₯) β π) |
53 | | eqid 2177 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
54 | | eqid 2177 |
. . . . . . . 8
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
55 | 26, 53, 25, 54 | opprmulg 13174 |
. . . . . . 7
β’ ((π
β Ring β§
((invrβπ)βπ₯) β π β§ π₯ β π) β (((invrβπ)βπ₯)(.rβ(opprβπ
))π₯) = (π₯(.rβπ
)((invrβπ)βπ₯))) |
56 | 24, 52, 42, 55 | syl3anc 1238 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (((invrβπ)βπ₯)(.rβ(opprβπ
))π₯) = (π₯(.rβπ
)((invrβπ)βπ₯))) |
57 | | eqid 2177 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
58 | | eqid 2177 |
. . . . . . . . 9
β’
(1rβπ) = (1rβπ) |
59 | 1, 45, 57, 58 | unitrinv 13227 |
. . . . . . . 8
β’ ((π β Ring β§ π₯ β π) β (π₯(.rβπ)((invrβπ)βπ₯)) = (1rβπ)) |
60 | 8, 59 | sylan 283 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (π₯(.rβπ)((invrβπ)βπ₯)) = (1rβπ)) |
61 | 7, 53 | ressmulrg 12595 |
. . . . . . . . . 10
β’ ((π΄ β (SubRingβπ
) β§ π
β Ring) β
(.rβπ
) =
(.rβπ)) |
62 | 23, 61 | mpdan 421 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
63 | 62 | adantr 276 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (.rβπ
) = (.rβπ)) |
64 | 63 | oveqd 5889 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (π₯(.rβπ
)((invrβπ)βπ₯)) = (π₯(.rβπ)((invrβπ)βπ₯))) |
65 | 60, 64, 15 | 3eqtr4d 2220 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (π₯(.rβπ
)((invrβπ)βπ₯)) = (1rβπ
)) |
66 | 56, 65 | eqtrd 2210 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (((invrβπ)βπ₯)(.rβ(opprβπ
))π₯) = (1rβπ
)) |
67 | 50, 66 | breqtrd 4028 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π₯(β₯rβ(opprβπ
))(1rβπ
)) |
68 | | subrguss.2 |
. . . . . . 7
β’ π = (Unitβπ
) |
69 | 68 | a1i 9 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β π = (Unitβπ
)) |
70 | | eqidd 2178 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β
(1rβπ
) =
(1rβπ
)) |
71 | | eqidd 2178 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β
(β₯rβπ
) = (β₯rβπ
)) |
72 | | eqidd 2178 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β
(opprβπ
) = (opprβπ
)) |
73 | | eqidd 2178 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
))) |
74 | | ringsrg 13155 |
. . . . . . 7
β’ (π
β Ring β π
β SRing) |
75 | 23, 74 | syl 14 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β π
β SRing) |
76 | 69, 70, 71, 72, 73, 75 | isunitd 13206 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β (π₯ β π β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
)))) |
77 | 76 | adantr 276 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β (π₯ β π β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
)))) |
78 | 22, 67, 77 | mpbir2and 944 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π₯ β π) β π₯ β π) |
79 | 78 | ex 115 |
. 2
β’ (π΄ β (SubRingβπ
) β (π₯ β π β π₯ β π)) |
80 | 79 | ssrdv 3161 |
1
β’ (π΄ β (SubRingβπ
) β π β π) |