Step | Hyp | Ref
| Expression |
1 | | rngidpropd.1 |
. . . . . . 7
β’ (π β π΅ = (BaseβπΎ)) |
2 | | rngidpropd.2 |
. . . . . . 7
β’ (π β π΅ = (BaseβπΏ)) |
3 | | rngidpropd.3 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) |
4 | 1, 2, 3 | rngidpropd 20125 |
. . . . . 6
β’ (π β (1rβπΎ) = (1rβπΏ)) |
5 | 4 | breq2d 5118 |
. . . . 5
β’ (π β (π§(β₯rβπΎ)(1rβπΎ) β π§(β₯rβπΎ)(1rβπΏ))) |
6 | 4 | breq2d 5118 |
. . . . 5
β’ (π β (π§(β₯rβ(opprβπΎ))(1rβπΎ) β π§(β₯rβ(opprβπΎ))(1rβπΏ))) |
7 | 5, 6 | anbi12d 632 |
. . . 4
β’ (π β ((π§(β₯rβπΎ)(1rβπΎ) β§ π§(β₯rβ(opprβπΎ))(1rβπΎ)) β (π§(β₯rβπΎ)(1rβπΏ) β§ π§(β₯rβ(opprβπΎ))(1rβπΏ)))) |
8 | 1, 2, 3 | dvdsrpropd 20126 |
. . . . . 6
β’ (π β
(β₯rβπΎ) = (β₯rβπΏ)) |
9 | 8 | breqd 5117 |
. . . . 5
β’ (π β (π§(β₯rβπΎ)(1rβπΏ) β π§(β₯rβπΏ)(1rβπΏ))) |
10 | | eqid 2737 |
. . . . . . . . 9
β’
(opprβπΎ) = (opprβπΎ) |
11 | | eqid 2737 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
12 | 10, 11 | opprbas 20057 |
. . . . . . . 8
β’
(BaseβπΎ) =
(Baseβ(opprβπΎ)) |
13 | 1, 12 | eqtrdi 2793 |
. . . . . . 7
β’ (π β π΅ =
(Baseβ(opprβπΎ))) |
14 | | eqid 2737 |
. . . . . . . . 9
β’
(opprβπΏ) = (opprβπΏ) |
15 | | eqid 2737 |
. . . . . . . . 9
β’
(BaseβπΏ) =
(BaseβπΏ) |
16 | 14, 15 | opprbas 20057 |
. . . . . . . 8
β’
(BaseβπΏ) =
(Baseβ(opprβπΏ)) |
17 | 2, 16 | eqtrdi 2793 |
. . . . . . 7
β’ (π β π΅ =
(Baseβ(opprβπΏ))) |
18 | 3 | ancom2s 649 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) |
19 | | eqid 2737 |
. . . . . . . . 9
β’
(.rβπΎ) = (.rβπΎ) |
20 | | eqid 2737 |
. . . . . . . . 9
β’
(.rβ(opprβπΎ)) =
(.rβ(opprβπΎ)) |
21 | 11, 19, 10, 20 | opprmul 20053 |
. . . . . . . 8
β’ (π¦(.rβ(opprβπΎ))π₯) = (π₯(.rβπΎ)π¦) |
22 | | eqid 2737 |
. . . . . . . . 9
β’
(.rβπΏ) = (.rβπΏ) |
23 | | eqid 2737 |
. . . . . . . . 9
β’
(.rβ(opprβπΏ)) =
(.rβ(opprβπΏ)) |
24 | 15, 22, 14, 23 | opprmul 20053 |
. . . . . . . 8
β’ (π¦(.rβ(opprβπΏ))π₯) = (π₯(.rβπΏ)π¦) |
25 | 18, 21, 24 | 3eqtr4g 2802 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π₯ β π΅)) β (π¦(.rβ(opprβπΎ))π₯) = (π¦(.rβ(opprβπΏ))π₯)) |
26 | 13, 17, 25 | dvdsrpropd 20126 |
. . . . . 6
β’ (π β
(β₯rβ(opprβπΎ)) =
(β₯rβ(opprβπΏ))) |
27 | 26 | breqd 5117 |
. . . . 5
β’ (π β (π§(β₯rβ(opprβπΎ))(1rβπΏ) β π§(β₯rβ(opprβπΏ))(1rβπΏ))) |
28 | 9, 27 | anbi12d 632 |
. . . 4
β’ (π β ((π§(β₯rβπΎ)(1rβπΏ) β§ π§(β₯rβ(opprβπΎ))(1rβπΏ)) β (π§(β₯rβπΏ)(1rβπΏ) β§ π§(β₯rβ(opprβπΏ))(1rβπΏ)))) |
29 | 7, 28 | bitrd 279 |
. . 3
β’ (π β ((π§(β₯rβπΎ)(1rβπΎ) β§ π§(β₯rβ(opprβπΎ))(1rβπΎ)) β (π§(β₯rβπΏ)(1rβπΏ) β§ π§(β₯rβ(opprβπΏ))(1rβπΏ)))) |
30 | | eqid 2737 |
. . . 4
β’
(UnitβπΎ) =
(UnitβπΎ) |
31 | | eqid 2737 |
. . . 4
β’
(1rβπΎ) = (1rβπΎ) |
32 | | eqid 2737 |
. . . 4
β’
(β₯rβπΎ) = (β₯rβπΎ) |
33 | | eqid 2737 |
. . . 4
β’
(β₯rβ(opprβπΎ)) =
(β₯rβ(opprβπΎ)) |
34 | 30, 31, 32, 10, 33 | isunit 20087 |
. . 3
β’ (π§ β (UnitβπΎ) β (π§(β₯rβπΎ)(1rβπΎ) β§ π§(β₯rβ(opprβπΎ))(1rβπΎ))) |
35 | | eqid 2737 |
. . . 4
β’
(UnitβπΏ) =
(UnitβπΏ) |
36 | | eqid 2737 |
. . . 4
β’
(1rβπΏ) = (1rβπΏ) |
37 | | eqid 2737 |
. . . 4
β’
(β₯rβπΏ) = (β₯rβπΏ) |
38 | | eqid 2737 |
. . . 4
β’
(β₯rβ(opprβπΏ)) =
(β₯rβ(opprβπΏ)) |
39 | 35, 36, 37, 14, 38 | isunit 20087 |
. . 3
β’ (π§ β (UnitβπΏ) β (π§(β₯rβπΏ)(1rβπΏ) β§ π§(β₯rβ(opprβπΏ))(1rβπΏ))) |
40 | 29, 34, 39 | 3bitr4g 314 |
. 2
β’ (π β (π§ β (UnitβπΎ) β π§ β (UnitβπΏ))) |
41 | 40 | eqrdv 2735 |
1
β’ (π β (UnitβπΎ) = (UnitβπΏ)) |