Metamath Proof Explorer

Theorem unitrrg

Description: Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypotheses unitrrg.e 
|- E = ( RLReg ` R )
unitrrg.u 
|- U = ( Unit ` R )
Assertion unitrrg 
|- ( R e. Ring -> U C_ E )

Proof

Step Hyp Ref Expression
1 unitrrg.e 
 |-  E = ( RLReg ` R )
2 unitrrg.u 
 |-  U = ( Unit ` R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 3 2 unitcl 
 |-  ( x e. U -> x e. ( Base ` R ) )
5 4 adantl 
 |-  ( ( R e. Ring /\ x e. U ) -> x e. ( Base ` R ) )
6 oveq2 
 |-  ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) ( x ( .r ` R ) y ) ) = ( ( ( invr ` R ) ` x ) ( .r ` R ) ( 0g ` R ) ) )
7 eqid 
 |-  ( invr ` R ) = ( invr ` R )
8 eqid 
 |-  ( .r ` R ) = ( .r ` R )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 2 7 8 9 unitlinv 
 |-  ( ( R e. Ring /\ x e. U ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) = ( 1r ` R ) )
11 10 adantr 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) = ( 1r ` R ) )
12 11 oveq1d 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) ( .r ` R ) y ) = ( ( 1r ` R ) ( .r ` R ) y ) )
13 simpll 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> R e. Ring )
14 2 7 3 ringinvcl 
 |-  ( ( R e. Ring /\ x e. U ) -> ( ( invr ` R ) ` x ) e. ( Base ` R ) )
15 14 adantr 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( ( invr ` R ) ` x ) e. ( Base ` R ) )
16 5 adantr 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> x e. ( Base ` R ) )
17 simpr 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> y e. ( Base ` R ) )
18 3 8 ringass 
 |-  ( ( R e. Ring /\ ( ( ( invr ` R ) ` x ) e. ( Base ` R ) /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) ( .r ` R ) y ) = ( ( ( invr ` R ) ` x ) ( .r ` R ) ( x ( .r ` R ) y ) ) )
19 13 15 16 17 18 syl13anc 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) ( .r ` R ) y ) = ( ( ( invr ` R ) ` x ) ( .r ` R ) ( x ( .r ` R ) y ) ) )
20 3 8 9 ringlidm 
 |-  ( ( R e. Ring /\ y e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) y ) = y )
21 20 adantlr 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) y ) = y )
22 12 19 21 3eqtr3d 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) ( x ( .r ` R ) y ) ) = y )
23 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
24 3 8 23 ringrz 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` x ) e. ( Base ` R ) ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
25 13 15 24 syl2anc 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
26 22 25 eqeq12d 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( ( ( ( invr ` R ) ` x ) ( .r ` R ) ( x ( .r ` R ) y ) ) = ( ( ( invr ` R ) ` x ) ( .r ` R ) ( 0g ` R ) ) <-> y = ( 0g ` R ) ) )
27 6 26 imbitrid 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> y = ( 0g ` R ) ) )
28 27 ralrimiva 
 |-  ( ( R e. Ring /\ x e. U ) -> A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> y = ( 0g ` R ) ) )
29 1 3 8 23 isrrg 
 |-  ( x e. E <-> ( x e. ( Base ` R ) /\ A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> y = ( 0g ` R ) ) ) )
30 5 28 29 sylanbrc 
 |-  ( ( R e. Ring /\ x e. U ) -> x e. E )
31 30 ex 
 |-  ( R e. Ring -> ( x e. U -> x e. E ) )
32 31 ssrdv 
 |-  ( R e. Ring -> U C_ E )