Metamath Proof Explorer

Theorem isunit

Description: Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 8-Dec-2015)

Ref Expression
Hypotheses unit.1 
|- U = ( Unit ` R )
unit.2 
|- .1. = ( 1r ` R )
unit.3 
|- .|| = ( ||r ` R )
unit.4 
|- S = ( oppR ` R )
unit.5 
|- E = ( ||r ` S )
Assertion isunit 
|- ( X e. U <-> ( X .|| .1. /\ X E .1. ) )

Proof

Step Hyp Ref Expression
1 unit.1 
 |-  U = ( Unit ` R )
2 unit.2 
 |-  .1. = ( 1r ` R )
3 unit.3 
 |-  .|| = ( ||r ` R )
4 unit.4 
 |-  S = ( oppR ` R )
5 unit.5 
 |-  E = ( ||r ` S )
6 elfvdm 
 |-  ( X e. ( Unit ` R ) -> R e. dom Unit )
7 6 1 eleq2s 
 |-  ( X e. U -> R e. dom Unit )
8 7 elexd 
 |-  ( X e. U -> R e. _V )
9 df-br 
 |-  ( X .|| .1. <-> <. X , .1. >. e. .|| )
10 elfvdm 
 |-  ( <. X , .1. >. e. ( ||r ` R ) -> R e. dom ||r )
11 10 3 eleq2s 
 |-  ( <. X , .1. >. e. .|| -> R e. dom ||r )
12 11 elexd 
 |-  ( <. X , .1. >. e. .|| -> R e. _V )
13 9 12 sylbi 
 |-  ( X .|| .1. -> R e. _V )
14 13 adantr 
 |-  ( ( X .|| .1. /\ X E .1. ) -> R e. _V )
15 fveq2 
 |-  ( r = R -> ( ||r ` r ) = ( ||r ` R ) )
16 15 3 eqtr4di 
 |-  ( r = R -> ( ||r ` r ) = .|| )
17 fveq2 
 |-  ( r = R -> ( oppR ` r ) = ( oppR ` R ) )
18 17 4 eqtr4di 
 |-  ( r = R -> ( oppR ` r ) = S )
19 18 fveq2d 
 |-  ( r = R -> ( ||r ` ( oppR ` r ) ) = ( ||r ` S ) )
20 19 5 eqtr4di 
 |-  ( r = R -> ( ||r ` ( oppR ` r ) ) = E )
21 16 20 ineq12d 
 |-  ( r = R -> ( ( ||r ` r ) i^i ( ||r ` ( oppR ` r ) ) ) = ( .|| i^i E ) )
22 21 cnveqd 
 |-  ( r = R -> `' ( ( ||r ` r ) i^i ( ||r ` ( oppR ` r ) ) ) = `' ( .|| i^i E ) )
23 fveq2 
 |-  ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
24 23 2 eqtr4di 
 |-  ( r = R -> ( 1r ` r ) = .1. )
25 24 sneqd 
 |-  ( r = R -> { ( 1r ` r ) } = { .1. } )
26 22 25 imaeq12d 
 |-  ( r = R -> ( `' ( ( ||r ` r ) i^i ( ||r ` ( oppR ` r ) ) ) " { ( 1r ` r ) } ) = ( `' ( .|| i^i E ) " { .1. } ) )
27 df-unit 
 |-  Unit = ( r e. _V |-> ( `' ( ( ||r ` r ) i^i ( ||r ` ( oppR ` r ) ) ) " { ( 1r ` r ) } ) )
28 3 fvexi 
 |-  .|| e. _V
29 28 inex1 
 |-  ( .|| i^i E ) e. _V
30 29 cnvex 
 |-  `' ( .|| i^i E ) e. _V
31 30 imaex 
 |-  ( `' ( .|| i^i E ) " { .1. } ) e. _V
32 26 27 31 fvmpt 
 |-  ( R e. _V -> ( Unit ` R ) = ( `' ( .|| i^i E ) " { .1. } ) )
33 1 32 eqtrid 
 |-  ( R e. _V -> U = ( `' ( .|| i^i E ) " { .1. } ) )
34 33 eleq2d 
 |-  ( R e. _V -> ( X e. U <-> X e. ( `' ( .|| i^i E ) " { .1. } ) ) )
35 inss1 
 |-  ( .|| i^i E ) C_ .||
36 3 reldvdsr 
 |-  Rel .||
37 relss 
 |-  ( ( .|| i^i E ) C_ .|| -> ( Rel .|| -> Rel ( .|| i^i E ) ) )
38 35 36 37 mp2 
 |-  Rel ( .|| i^i E )
39 eliniseg2 
 |-  ( Rel ( .|| i^i E ) -> ( X e. ( `' ( .|| i^i E ) " { .1. } ) <-> X ( .|| i^i E ) .1. ) )
40 38 39 ax-mp 
 |-  ( X e. ( `' ( .|| i^i E ) " { .1. } ) <-> X ( .|| i^i E ) .1. )
41 brin 
 |-  ( X ( .|| i^i E ) .1. <-> ( X .|| .1. /\ X E .1. ) )
42 40 41 bitri 
 |-  ( X e. ( `' ( .|| i^i E ) " { .1. } ) <-> ( X .|| .1. /\ X E .1. ) )
43 34 42 bitrdi 
 |-  ( R e. _V -> ( X e. U <-> ( X .|| .1. /\ X E .1. ) ) )
44 8 14 43 pm5.21nii 
 |-  ( X e. U <-> ( X .|| .1. /\ X E .1. ) )