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

Metamath Proof Explorer

Theorem opprdomnb

Description: A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn . (Contributed by SN, 15-Jun-2015)

Ref Expression
Hypothesis opprdomn.1 
|- O = ( oppR ` R )
Assertion opprdomnb 
|- ( R e. Domn <-> O e. Domn )

Proof

Step Hyp Ref Expression
1 opprdomn.1 
 |-  O = ( oppR ` R )
2 1 opprnzrb 
 |-  ( R e. NzRing <-> O e. NzRing )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 1 3 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
5 eqid 
 |-  ( .r ` R ) = ( .r ` R )
6 eqid 
 |-  ( .r ` O ) = ( .r ` O )
7 3 5 1 6 opprmul 
 |-  ( y ( .r ` O ) x ) = ( x ( .r ` R ) y )
8 7 eqcomi 
 |-  ( x ( .r ` R ) y ) = ( y ( .r ` O ) x )
9 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
10 1 9 oppr0 
 |-  ( 0g ` R ) = ( 0g ` O )
11 8 10 eqeq12i 
 |-  ( ( x ( .r ` R ) y ) = ( 0g ` R ) <-> ( y ( .r ` O ) x ) = ( 0g ` O ) )
12 10 eqeq2i 
 |-  ( x = ( 0g ` R ) <-> x = ( 0g ` O ) )
13 10 eqeq2i 
 |-  ( y = ( 0g ` R ) <-> y = ( 0g ` O ) )
14 12 13 orbi12i 
 |-  ( ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) <-> ( x = ( 0g ` O ) \/ y = ( 0g ` O ) ) )
15 orcom 
 |-  ( ( x = ( 0g ` O ) \/ y = ( 0g ` O ) ) <-> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) )
16 14 15 bitri 
 |-  ( ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) <-> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) )
17 11 16 imbi12i 
 |-  ( ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) <-> ( ( y ( .r ` O ) x ) = ( 0g ` O ) -> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) ) )
18 4 17 raleqbii 
 |-  ( A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) <-> A. y e. ( Base ` O ) ( ( y ( .r ` O ) x ) = ( 0g ` O ) -> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) ) )
19 4 18 raleqbii 
 |-  ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) <-> A. x e. ( Base ` O ) A. y e. ( Base ` O ) ( ( y ( .r ` O ) x ) = ( 0g ` O ) -> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) ) )
20 ralcom 
 |-  ( A. x e. ( Base ` O ) A. y e. ( Base ` O ) ( ( y ( .r ` O ) x ) = ( 0g ` O ) -> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) ) <-> A. y e. ( Base ` O ) A. x e. ( Base ` O ) ( ( y ( .r ` O ) x ) = ( 0g ` O ) -> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) ) )
21 19 20 bitri 
 |-  ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) <-> A. y e. ( Base ` O ) A. x e. ( Base ` O ) ( ( y ( .r ` O ) x ) = ( 0g ` O ) -> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) ) )
22 2 21 anbi12i 
 |-  ( ( R e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) ) <-> ( O e. NzRing /\ A. y e. ( Base ` O ) A. x e. ( Base ` O ) ( ( y ( .r ` O ) x ) = ( 0g ` O ) -> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) ) ) )
23 3 5 9 isdomn 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) ) )
24 eqid 
 |-  ( Base ` O ) = ( Base ` O )
25 eqid 
 |-  ( 0g ` O ) = ( 0g ` O )
26 24 6 25 isdomn 
 |-  ( O e. Domn <-> ( O e. NzRing /\ A. y e. ( Base ` O ) A. x e. ( Base ` O ) ( ( y ( .r ` O ) x ) = ( 0g ` O ) -> ( y = ( 0g ` O ) \/ x = ( 0g ` O ) ) ) ) )
27 22 23 26 3bitr4i 
 |-  ( R e. Domn <-> O e. Domn )