Metamath Proof Explorer

Theorem opprdomn

Description: The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 opprdomn.1 
 |-  O = ( oppR ` R )
2 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
3 1 opprnzr 
 |-  ( R e. NzRing -> O e. NzRing )
4 2 3 syl 
 |-  ( R e. Domn -> O e. NzRing )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 5 6 7 domneq0 
 |-  ( ( R e. Domn /\ y e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> ( ( y ( .r ` R ) x ) = ( 0g ` R ) <-> ( y = ( 0g ` R ) \/ x = ( 0g ` R ) ) ) )
9 8 3com23 
 |-  ( ( R e. Domn /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( y ( .r ` R ) x ) = ( 0g ` R ) <-> ( y = ( 0g ` R ) \/ x = ( 0g ` R ) ) ) )
10 eqid 
 |-  ( .r ` O ) = ( .r ` O )
11 5 6 1 10 opprmul 
 |-  ( x ( .r ` O ) y ) = ( y ( .r ` R ) x )
12 11 eqeq1i 
 |-  ( ( x ( .r ` O ) y ) = ( 0g ` R ) <-> ( y ( .r ` R ) x ) = ( 0g ` R ) )
13 orcom 
 |-  ( ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) <-> ( y = ( 0g ` R ) \/ x = ( 0g ` R ) ) )
14 9 12 13 3bitr4g 
 |-  ( ( R e. Domn /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` O ) y ) = ( 0g ` R ) <-> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) )
15 14 biimpd 
 |-  ( ( R e. Domn /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` O ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) )
16 15 3expb 
 |-  ( ( R e. Domn /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( .r ` O ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) )
17 16 ralrimivva 
 |-  ( R e. Domn -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` O ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) )
18 1 5 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
19 1 7 oppr0 
 |-  ( 0g ` R ) = ( 0g ` O )
20 18 10 19 isdomn 
 |-  ( O e. Domn <-> ( O e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` O ) y ) = ( 0g ` R ) -> ( x = ( 0g ` R ) \/ y = ( 0g ` R ) ) ) ) )
21 4 17 20 sylanbrc 
 |-  ( R e. Domn -> O e. Domn )