Step |
Hyp |
Ref |
Expression |
1 |
|
opprunit.1 |
|- U = ( Unit ` R ) |
2 |
|
opprunit.2 |
|- S = ( oppR ` R ) |
3 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
4 |
2 3
|
opprbas |
|- ( Base ` R ) = ( Base ` S ) |
5 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
6 |
|
eqid |
|- ( oppR ` S ) = ( oppR ` S ) |
7 |
|
eqid |
|- ( .r ` ( oppR ` S ) ) = ( .r ` ( oppR ` S ) ) |
8 |
4 5 6 7
|
opprmul |
|- ( y ( .r ` ( oppR ` S ) ) x ) = ( x ( .r ` S ) y ) |
9 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
10 |
3 9 2 5
|
opprmul |
|- ( x ( .r ` S ) y ) = ( y ( .r ` R ) x ) |
11 |
8 10
|
eqtr2i |
|- ( y ( .r ` R ) x ) = ( y ( .r ` ( oppR ` S ) ) x ) |
12 |
11
|
eqeq1i |
|- ( ( y ( .r ` R ) x ) = ( 1r ` R ) <-> ( y ( .r ` ( oppR ` S ) ) x ) = ( 1r ` R ) ) |
13 |
12
|
rexbii |
|- ( E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) <-> E. y e. ( Base ` R ) ( y ( .r ` ( oppR ` S ) ) x ) = ( 1r ` R ) ) |
14 |
13
|
anbi2i |
|- ( ( x e. ( Base ` R ) /\ E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) ) <-> ( x e. ( Base ` R ) /\ E. y e. ( Base ` R ) ( y ( .r ` ( oppR ` S ) ) x ) = ( 1r ` R ) ) ) |
15 |
|
eqid |
|- ( ||r ` R ) = ( ||r ` R ) |
16 |
3 15 9
|
dvdsr |
|- ( x ( ||r ` R ) ( 1r ` R ) <-> ( x e. ( Base ` R ) /\ E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) ) ) |
17 |
6 4
|
opprbas |
|- ( Base ` R ) = ( Base ` ( oppR ` S ) ) |
18 |
|
eqid |
|- ( ||r ` ( oppR ` S ) ) = ( ||r ` ( oppR ` S ) ) |
19 |
17 18 7
|
dvdsr |
|- ( x ( ||r ` ( oppR ` S ) ) ( 1r ` R ) <-> ( x e. ( Base ` R ) /\ E. y e. ( Base ` R ) ( y ( .r ` ( oppR ` S ) ) x ) = ( 1r ` R ) ) ) |
20 |
14 16 19
|
3bitr4i |
|- ( x ( ||r ` R ) ( 1r ` R ) <-> x ( ||r ` ( oppR ` S ) ) ( 1r ` R ) ) |
21 |
20
|
anbi2ci |
|- ( ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` S ) ( 1r ` R ) ) <-> ( x ( ||r ` S ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` S ) ) ( 1r ` R ) ) ) |
22 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
23 |
|
eqid |
|- ( ||r ` S ) = ( ||r ` S ) |
24 |
1 22 15 2 23
|
isunit |
|- ( x e. U <-> ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` S ) ( 1r ` R ) ) ) |
25 |
|
eqid |
|- ( Unit ` S ) = ( Unit ` S ) |
26 |
2 22
|
oppr1 |
|- ( 1r ` R ) = ( 1r ` S ) |
27 |
25 26 23 6 18
|
isunit |
|- ( x e. ( Unit ` S ) <-> ( x ( ||r ` S ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` S ) ) ( 1r ` R ) ) ) |
28 |
21 24 27
|
3bitr4i |
|- ( x e. U <-> x e. ( Unit ` S ) ) |
29 |
28
|
eqriv |
|- U = ( Unit ` S ) |