Step | Hyp | Ref
| Expression |
1 | | unitpropdg.1 |
. . . . . . 7
β’ (π β π΅ = (BaseβπΎ)) |
2 | | unitpropdg.2 |
. . . . . . 7
β’ (π β π΅ = (BaseβπΏ)) |
3 | | unitpropdg.3 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) |
4 | | unitpropdg.k |
. . . . . . 7
β’ (π β πΎ β Ring) |
5 | | unitpropdg.l |
. . . . . . 7
β’ (π β πΏ β Ring) |
6 | 1, 2, 3, 4, 5 | rngidpropdg 13315 |
. . . . . 6
β’ (π β (1rβπΎ) = (1rβπΏ)) |
7 | 6 | breq2d 4016 |
. . . . 5
β’ (π β (π§(β₯rβπΎ)(1rβπΎ) β π§(β₯rβπΎ)(1rβπΏ))) |
8 | 6 | breq2d 4016 |
. . . . 5
β’ (π β (π§(β₯rβ(opprβπΎ))(1rβπΎ) β π§(β₯rβ(opprβπΎ))(1rβπΏ))) |
9 | 7, 8 | anbi12d 473 |
. . . 4
β’ (π β ((π§(β₯rβπΎ)(1rβπΎ) β§ π§(β₯rβ(opprβπΎ))(1rβπΎ)) β (π§(β₯rβπΎ)(1rβπΏ) β§ π§(β₯rβ(opprβπΎ))(1rβπΏ)))) |
10 | | ringsrg 13224 |
. . . . . . . 8
β’ (πΎ β Ring β πΎ β SRing) |
11 | 4, 10 | syl 14 |
. . . . . . 7
β’ (π β πΎ β SRing) |
12 | | ringsrg 13224 |
. . . . . . . 8
β’ (πΏ β Ring β πΏ β SRing) |
13 | 5, 12 | syl 14 |
. . . . . . 7
β’ (π β πΏ β SRing) |
14 | 1, 2, 3, 11, 13 | dvdsrpropdg 13316 |
. . . . . 6
β’ (π β
(β₯rβπΎ) = (β₯rβπΏ)) |
15 | 14 | breqd 4015 |
. . . . 5
β’ (π β (π§(β₯rβπΎ)(1rβπΏ) β π§(β₯rβπΏ)(1rβπΏ))) |
16 | | eqid 2177 |
. . . . . . . . . 10
β’
(opprβπΎ) = (opprβπΎ) |
17 | | eqid 2177 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
18 | 16, 17 | opprbasg 13247 |
. . . . . . . . 9
β’ (πΎ β Ring β
(BaseβπΎ) =
(Baseβ(opprβπΎ))) |
19 | 4, 18 | syl 14 |
. . . . . . . 8
β’ (π β (BaseβπΎ) =
(Baseβ(opprβπΎ))) |
20 | 1, 19 | eqtrd 2210 |
. . . . . . 7
β’ (π β π΅ =
(Baseβ(opprβπΎ))) |
21 | | eqid 2177 |
. . . . . . . . . 10
β’
(opprβπΏ) = (opprβπΏ) |
22 | | eqid 2177 |
. . . . . . . . . 10
β’
(BaseβπΏ) =
(BaseβπΏ) |
23 | 21, 22 | opprbasg 13247 |
. . . . . . . . 9
β’ (πΏ β Ring β
(BaseβπΏ) =
(Baseβ(opprβπΏ))) |
24 | 5, 23 | syl 14 |
. . . . . . . 8
β’ (π β (BaseβπΏ) =
(Baseβ(opprβπΏ))) |
25 | 2, 24 | eqtrd 2210 |
. . . . . . 7
β’ (π β π΅ =
(Baseβ(opprβπΏ))) |
26 | 3 | ancom2s 566 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) |
27 | 4 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β πΎ β Ring) |
28 | | simprl 529 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β π¦ β π΅) |
29 | | simprr 531 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β π₯ β π΅) |
30 | | eqid 2177 |
. . . . . . . . . 10
β’
(.rβπΎ) = (.rβπΎ) |
31 | | eqid 2177 |
. . . . . . . . . 10
β’
(.rβ(opprβπΎ)) =
(.rβ(opprβπΎ)) |
32 | 17, 30, 16, 31 | opprmulg 13243 |
. . . . . . . . 9
β’ ((πΎ β Ring β§ π¦ β π΅ β§ π₯ β π΅) β (π¦(.rβ(opprβπΎ))π₯) = (π₯(.rβπΎ)π¦)) |
33 | 27, 28, 29, 32 | syl3anc 1238 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β (π¦(.rβ(opprβπΎ))π₯) = (π₯(.rβπΎ)π¦)) |
34 | 5 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β πΏ β Ring) |
35 | | eqid 2177 |
. . . . . . . . . 10
β’
(.rβπΏ) = (.rβπΏ) |
36 | | eqid 2177 |
. . . . . . . . . 10
β’
(.rβ(opprβπΏ)) =
(.rβ(opprβπΏ)) |
37 | 22, 35, 21, 36 | opprmulg 13243 |
. . . . . . . . 9
β’ ((πΏ β Ring β§ π¦ β π΅ β§ π₯ β π΅) β (π¦(.rβ(opprβπΏ))π₯) = (π₯(.rβπΏ)π¦)) |
38 | 34, 28, 29, 37 | syl3anc 1238 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β (π¦(.rβ(opprβπΏ))π₯) = (π₯(.rβπΏ)π¦)) |
39 | 26, 33, 38 | 3eqtr4d 2220 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β (π¦(.rβ(opprβπΎ))π₯) = (π¦(.rβ(opprβπΏ))π₯)) |
40 | 16 | opprring 13249 |
. . . . . . . 8
β’ (πΎ β Ring β
(opprβπΎ) β Ring) |
41 | | ringsrg 13224 |
. . . . . . . 8
β’
((opprβπΎ) β Ring β
(opprβπΎ) β SRing) |
42 | 4, 40, 41 | 3syl 17 |
. . . . . . 7
β’ (π β
(opprβπΎ) β SRing) |
43 | 21 | opprring 13249 |
. . . . . . . 8
β’ (πΏ β Ring β
(opprβπΏ) β Ring) |
44 | | ringsrg 13224 |
. . . . . . . 8
β’
((opprβπΏ) β Ring β
(opprβπΏ) β SRing) |
45 | 5, 43, 44 | 3syl 17 |
. . . . . . 7
β’ (π β
(opprβπΏ) β SRing) |
46 | 20, 25, 39, 42, 45 | dvdsrpropdg 13316 |
. . . . . 6
β’ (π β
(β₯rβ(opprβπΎ)) =
(β₯rβ(opprβπΏ))) |
47 | 46 | breqd 4015 |
. . . . 5
β’ (π β (π§(β₯rβ(opprβπΎ))(1rβπΏ) β π§(β₯rβ(opprβπΏ))(1rβπΏ))) |
48 | 15, 47 | anbi12d 473 |
. . . 4
β’ (π β ((π§(β₯rβπΎ)(1rβπΏ) β§ π§(β₯rβ(opprβπΎ))(1rβπΏ)) β (π§(β₯rβπΏ)(1rβπΏ) β§ π§(β₯rβ(opprβπΏ))(1rβπΏ)))) |
49 | 9, 48 | bitrd 188 |
. . 3
β’ (π β ((π§(β₯rβπΎ)(1rβπΎ) β§ π§(β₯rβ(opprβπΎ))(1rβπΎ)) β (π§(β₯rβπΏ)(1rβπΏ) β§ π§(β₯rβ(opprβπΏ))(1rβπΏ)))) |
50 | | eqidd 2178 |
. . . 4
β’ (π β (UnitβπΎ) = (UnitβπΎ)) |
51 | | eqidd 2178 |
. . . 4
β’ (π β (1rβπΎ) = (1rβπΎ)) |
52 | | eqidd 2178 |
. . . 4
β’ (π β
(β₯rβπΎ) = (β₯rβπΎ)) |
53 | | eqidd 2178 |
. . . 4
β’ (π β
(opprβπΎ) = (opprβπΎ)) |
54 | | eqidd 2178 |
. . . 4
β’ (π β
(β₯rβ(opprβπΎ)) =
(β₯rβ(opprβπΎ))) |
55 | 50, 51, 52, 53, 54, 11 | isunitd 13275 |
. . 3
β’ (π β (π§ β (UnitβπΎ) β (π§(β₯rβπΎ)(1rβπΎ) β§ π§(β₯rβ(opprβπΎ))(1rβπΎ)))) |
56 | | eqidd 2178 |
. . . 4
β’ (π β (UnitβπΏ) = (UnitβπΏ)) |
57 | | eqidd 2178 |
. . . 4
β’ (π β (1rβπΏ) = (1rβπΏ)) |
58 | | eqidd 2178 |
. . . 4
β’ (π β
(β₯rβπΏ) = (β₯rβπΏ)) |
59 | | eqidd 2178 |
. . . 4
β’ (π β
(opprβπΏ) = (opprβπΏ)) |
60 | | eqidd 2178 |
. . . 4
β’ (π β
(β₯rβ(opprβπΏ)) =
(β₯rβ(opprβπΏ))) |
61 | 56, 57, 58, 59, 60, 13 | isunitd 13275 |
. . 3
β’ (π β (π§ β (UnitβπΏ) β (π§(β₯rβπΏ)(1rβπΏ) β§ π§(β₯rβ(opprβπΏ))(1rβπΏ)))) |
62 | 49, 55, 61 | 3bitr4d 220 |
. 2
β’ (π β (π§ β (UnitβπΎ) β π§ β (UnitβπΏ))) |
63 | 62 | eqrdv 2175 |
1
β’ (π β (UnitβπΎ) = (UnitβπΏ)) |