This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opprunit

Description: Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses opprunit.1 
|- U = ( Unit ` R )
opprunit.2 
|- S = ( oppR ` R )
Assertion opprunit 
|- U = ( Unit ` S )

Proof

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 )