Step |
Hyp |
Ref |
Expression |
1 |
|
opprirred.1 |
|- S = ( oppR ` R ) |
2 |
|
opprirred.2 |
|- I = ( Irred ` R ) |
3 |
|
ralcom |
|- ( A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( z ( .r ` R ) y ) =/= x <-> A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) ( z ( .r ` R ) y ) =/= x ) |
4 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
5 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
6 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
7 |
4 5 1 6
|
opprmul |
|- ( y ( .r ` S ) z ) = ( z ( .r ` R ) y ) |
8 |
7
|
neeq1i |
|- ( ( y ( .r ` S ) z ) =/= x <-> ( z ( .r ` R ) y ) =/= x ) |
9 |
8
|
2ralbii |
|- ( A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) ( y ( .r ` S ) z ) =/= x <-> A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) ( z ( .r ` R ) y ) =/= x ) |
10 |
3 9
|
bitr4i |
|- ( A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( z ( .r ` R ) y ) =/= x <-> A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) ( y ( .r ` S ) z ) =/= x ) |
11 |
10
|
anbi2i |
|- ( ( x e. ( ( Base ` R ) \ ( Unit ` R ) ) /\ A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( z ( .r ` R ) y ) =/= x ) <-> ( x e. ( ( Base ` R ) \ ( Unit ` R ) ) /\ A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) ( y ( .r ` S ) z ) =/= x ) ) |
12 |
|
eqid |
|- ( Unit ` R ) = ( Unit ` R ) |
13 |
|
eqid |
|- ( ( Base ` R ) \ ( Unit ` R ) ) = ( ( Base ` R ) \ ( Unit ` R ) ) |
14 |
4 12 2 13 5
|
isirred |
|- ( x e. I <-> ( x e. ( ( Base ` R ) \ ( Unit ` R ) ) /\ A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( z ( .r ` R ) y ) =/= x ) ) |
15 |
1 4
|
opprbas |
|- ( Base ` R ) = ( Base ` S ) |
16 |
12 1
|
opprunit |
|- ( Unit ` R ) = ( Unit ` S ) |
17 |
|
eqid |
|- ( Irred ` S ) = ( Irred ` S ) |
18 |
15 16 17 13 6
|
isirred |
|- ( x e. ( Irred ` S ) <-> ( x e. ( ( Base ` R ) \ ( Unit ` R ) ) /\ A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) A. z e. ( ( Base ` R ) \ ( Unit ` R ) ) ( y ( .r ` S ) z ) =/= x ) ) |
19 |
11 14 18
|
3bitr4i |
|- ( x e. I <-> x e. ( Irred ` S ) ) |
20 |
19
|
eqriv |
|- I = ( Irred ` S ) |