Step | Hyp | Ref
| Expression |
1 | | subrgugrp.1 |
. . . . 5
β’ π = (π
βΎs π΄) |
2 | | subrgugrp.2 |
. . . . 5
β’ π = (Unitβπ
) |
3 | | subrgugrp.3 |
. . . . 5
β’ π = (Unitβπ) |
4 | 1, 2, 3 | subrguss 13295 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π β π) |
5 | 4 | sselda 3155 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β π) |
6 | 1 | subrgbas 13289 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β π΄ = (Baseβπ)) |
7 | 6 | adantr 276 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π΄ = (Baseβπ)) |
8 | 3 | a1i 9 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π = (Unitβπ)) |
9 | 1 | subrgring 13283 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β π β Ring) |
10 | | ringsrg 13155 |
. . . . . 6
β’ (π β Ring β π β SRing) |
11 | 9, 10 | syl 14 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β π β SRing) |
12 | 11 | adantr 276 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β SRing) |
13 | | simpr 110 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β π) |
14 | 7, 8, 12, 13 | unitcld 13208 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β π΄) |
15 | | eqid 2177 |
. . . . . 6
β’
(invrβπ) = (invrβπ) |
16 | | eqid 2177 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
17 | 3, 15, 16 | ringinvcl 13225 |
. . . . 5
β’ ((π β Ring β§ π β π) β ((invrβπ)βπ) β (Baseβπ)) |
18 | 9, 17 | sylan 283 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β ((invrβπ)βπ) β (Baseβπ)) |
19 | | subrgunit.4 |
. . . . 5
β’ πΌ = (invrβπ
) |
20 | 1, 19, 3, 15 | subrginv 13296 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (πΌβπ) = ((invrβπ)βπ)) |
21 | 18, 20, 7 | 3eltr4d 2261 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (πΌβπ) β π΄) |
22 | 5, 14, 21 | 3jca 1177 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) |
23 | | eqidd 2178 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (Baseβπ) = (Baseβπ)) |
24 | | eqidd 2178 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (β₯rβπ) =
(β₯rβπ)) |
25 | 11 | adantr 276 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π β SRing) |
26 | | eqidd 2178 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (.rβπ) = (.rβπ)) |
27 | | simpr2 1004 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π β π΄) |
28 | 6 | adantr 276 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π΄ = (Baseβπ)) |
29 | 27, 28 | eleqtrd 2256 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π β (Baseβπ)) |
30 | | simpr3 1005 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (πΌβπ) β π΄) |
31 | 30, 28 | eleqtrd 2256 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (πΌβπ) β (Baseβπ)) |
32 | 23, 24, 25, 26, 29, 31 | dvdsrmuld 13196 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π(β₯rβπ)((πΌβπ)(.rβπ)π)) |
33 | | subrgrcl 13285 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
34 | | simpr1 1003 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π β π) |
35 | | eqid 2177 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
36 | | eqid 2177 |
. . . . . . 7
β’
(1rβπ
) = (1rβπ
) |
37 | 2, 19, 35, 36 | unitlinv 13226 |
. . . . . 6
β’ ((π
β Ring β§ π β π) β ((πΌβπ)(.rβπ
)π) = (1rβπ
)) |
38 | 33, 34, 37 | syl2an2r 595 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β ((πΌβπ)(.rβπ
)π) = (1rβπ
)) |
39 | 1, 35 | ressmulrg 12595 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π
β Ring) β
(.rβπ
) =
(.rβπ)) |
40 | 33, 39 | mpdan 421 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
41 | 40 | adantr 276 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (.rβπ
) = (.rβπ)) |
42 | 41 | oveqd 5889 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β ((πΌβπ)(.rβπ
)π) = ((πΌβπ)(.rβπ)π)) |
43 | 1, 36 | subrg1 13290 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β
(1rβπ
) =
(1rβπ)) |
44 | 43 | adantr 276 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (1rβπ
) = (1rβπ)) |
45 | 38, 42, 44 | 3eqtr3d 2218 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β ((πΌβπ)(.rβπ)π) = (1rβπ)) |
46 | 32, 45 | breqtrd 4028 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π(β₯rβπ)(1rβπ)) |
47 | 9 | adantr 276 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π β Ring) |
48 | | eqid 2177 |
. . . . . . 7
β’
(opprβπ) = (opprβπ) |
49 | 48, 16 | opprbasg 13178 |
. . . . . 6
β’ (π β Ring β
(Baseβπ) =
(Baseβ(opprβπ))) |
50 | 47, 49 | syl 14 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (Baseβπ) =
(Baseβ(opprβπ))) |
51 | | eqidd 2178 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β
(β₯rβ(opprβπ)) =
(β₯rβ(opprβπ))) |
52 | 48 | opprring 13180 |
. . . . . 6
β’ (π β Ring β
(opprβπ) β Ring) |
53 | | ringsrg 13155 |
. . . . . 6
β’
((opprβπ) β Ring β
(opprβπ) β SRing) |
54 | 47, 52, 53 | 3syl 17 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β
(opprβπ) β SRing) |
55 | | eqidd 2178 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β
(.rβ(opprβπ)) =
(.rβ(opprβπ))) |
56 | 50, 51, 54, 55, 29, 31 | dvdsrmuld 13196 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π(β₯rβ(opprβπ))((πΌβπ)(.rβ(opprβπ))π)) |
57 | | eqid 2177 |
. . . . . . 7
β’
(.rβπ) = (.rβπ) |
58 | | eqid 2177 |
. . . . . . 7
β’
(.rβ(opprβπ)) =
(.rβ(opprβπ)) |
59 | 16, 57, 48, 58 | opprmulg 13174 |
. . . . . 6
β’ ((π β Ring β§ (πΌβπ) β (Baseβπ) β§ π β (Baseβπ)) β ((πΌβπ)(.rβ(opprβπ))π) = (π(.rβπ)(πΌβπ))) |
60 | 47, 31, 29, 59 | syl3anc 1238 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β ((πΌβπ)(.rβ(opprβπ))π) = (π(.rβπ)(πΌβπ))) |
61 | 2, 19, 35, 36 | unitrinv 13227 |
. . . . . . 7
β’ ((π
β Ring β§ π β π) β (π(.rβπ
)(πΌβπ)) = (1rβπ
)) |
62 | 33, 34, 61 | syl2an2r 595 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (π(.rβπ
)(πΌβπ)) = (1rβπ
)) |
63 | 41 | oveqd 5889 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (π(.rβπ
)(πΌβπ)) = (π(.rβπ)(πΌβπ))) |
64 | 62, 63, 44 | 3eqtr3d 2218 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (π(.rβπ)(πΌβπ)) = (1rβπ)) |
65 | 60, 64 | eqtrd 2210 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β ((πΌβπ)(.rβ(opprβπ))π) = (1rβπ)) |
66 | 56, 65 | breqtrd 4028 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π(β₯rβ(opprβπ))(1rβπ)) |
67 | 3 | a1i 9 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β π = (Unitβπ)) |
68 | | eqidd 2178 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β
(1rβπ) =
(1rβπ)) |
69 | | eqidd 2178 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β
(β₯rβπ) = (β₯rβπ)) |
70 | | eqidd 2178 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β
(opprβπ) = (opprβπ)) |
71 | | eqidd 2178 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β
(β₯rβ(opprβπ)) =
(β₯rβ(opprβπ))) |
72 | 67, 68, 69, 70, 71, 11 | isunitd 13206 |
. . . 4
β’ (π΄ β (SubRingβπ
) β (π β π β (π(β₯rβπ)(1rβπ) β§ π(β₯rβ(opprβπ))(1rβπ)))) |
73 | 72 | adantr 276 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β (π β π β (π(β₯rβπ)(1rβπ) β§ π(β₯rβ(opprβπ))(1rβπ)))) |
74 | 46, 66, 73 | mpbir2and 944 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ (π β π β§ π β π΄ β§ (πΌβπ) β π΄)) β π β π) |
75 | 22, 74 | impbida 596 |
1
β’ (π΄ β (SubRingβπ
) β (π β π β (π β π β§ π β π΄ β§ (πΌβπ) β π΄))) |