Metamath Proof Explorer

Theorem crngunit

Description: Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses crngunit.1 
|- U = ( Unit ` R )
crngunit.2 
|- .1. = ( 1r ` R )
crngunit.3 
|- .|| = ( ||r ` R )
Assertion crngunit 
|- ( R e. CRing -> ( X e. U <-> X .|| .1. ) )

Proof

Step Hyp Ref Expression
1 crngunit.1 
 |-  U = ( Unit ` R )
2 crngunit.2 
 |-  .1. = ( 1r ` R )
3 crngunit.3 
 |-  .|| = ( ||r ` R )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 eqid 
 |-  ( .r ` R ) = ( .r ` R )
6 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
7 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
8 4 5 6 7 crngoppr 
 |-  ( ( R e. CRing /\ y e. ( Base ` R ) /\ X e. ( Base ` R ) ) -> ( y ( .r ` R ) X ) = ( y ( .r ` ( oppR ` R ) ) X ) )
9 8 3expa 
 |-  ( ( ( R e. CRing /\ y e. ( Base ` R ) ) /\ X e. ( Base ` R ) ) -> ( y ( .r ` R ) X ) = ( y ( .r ` ( oppR ` R ) ) X ) )
10 9 eqcomd 
 |-  ( ( ( R e. CRing /\ y e. ( Base ` R ) ) /\ X e. ( Base ` R ) ) -> ( y ( .r ` ( oppR ` R ) ) X ) = ( y ( .r ` R ) X ) )
11 10 an32s 
 |-  ( ( ( R e. CRing /\ X e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> ( y ( .r ` ( oppR ` R ) ) X ) = ( y ( .r ` R ) X ) )
12 11 eqeq1d 
 |-  ( ( ( R e. CRing /\ X e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> ( ( y ( .r ` ( oppR ` R ) ) X ) = .1. <-> ( y ( .r ` R ) X ) = .1. ) )
13 12 rexbidva 
 |-  ( ( R e. CRing /\ X e. ( Base ` R ) ) -> ( E. y e. ( Base ` R ) ( y ( .r ` ( oppR ` R ) ) X ) = .1. <-> E. y e. ( Base ` R ) ( y ( .r ` R ) X ) = .1. ) )
14 13 pm5.32da 
 |-  ( R e. CRing -> ( ( X e. ( Base ` R ) /\ E. y e. ( Base ` R ) ( y ( .r ` ( oppR ` R ) ) X ) = .1. ) <-> ( X e. ( Base ` R ) /\ E. y e. ( Base ` R ) ( y ( .r ` R ) X ) = .1. ) ) )
15 6 4 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
16 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
17 15 16 7 dvdsr 
 |-  ( X ( ||r ` ( oppR ` R ) ) .1. <-> ( X e. ( Base ` R ) /\ E. y e. ( Base ` R ) ( y ( .r ` ( oppR ` R ) ) X ) = .1. ) )
18 4 3 5 dvdsr 
 |-  ( X .|| .1. <-> ( X e. ( Base ` R ) /\ E. y e. ( Base ` R ) ( y ( .r ` R ) X ) = .1. ) )
19 14 17 18 3bitr4g 
 |-  ( R e. CRing -> ( X ( ||r ` ( oppR ` R ) ) .1. <-> X .|| .1. ) )
20 19 anbi2d 
 |-  ( R e. CRing -> ( ( X .|| .1. /\ X ( ||r ` ( oppR ` R ) ) .1. ) <-> ( X .|| .1. /\ X .|| .1. ) ) )
21 1 2 3 6 16 isunit 
 |-  ( X e. U <-> ( X .|| .1. /\ X ( ||r ` ( oppR ` R ) ) .1. ) )
22 pm4.24 
 |-  ( X .|| .1. <-> ( X .|| .1. /\ X .|| .1. ) )
23 20 21 22 3bitr4g 
 |-  ( R e. CRing -> ( X e. U <-> X .|| .1. ) )