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

Metamath Proof Explorer

Theorem dvr1

Description: A ring element divided by the ring unity is itself. ( div1 analog.) (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses dvr1.b 
|- B = ( Base ` R )
dvr1.d 
|- ./ = ( /r ` R )
dvr1.o 
|- .1. = ( 1r ` R )
Assertion dvr1 
|- ( ( R e. Ring /\ X e. B ) -> ( X ./ .1. ) = X )

Proof

Step Hyp Ref Expression
1 dvr1.b 
 |-  B = ( Base ` R )
2 dvr1.d 
 |-  ./ = ( /r ` R )
3 dvr1.o 
 |-  .1. = ( 1r ` R )
4 id 
 |-  ( X e. B -> X e. B )
5 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
6 5 3 1unit 
 |-  ( R e. Ring -> .1. e. ( Unit ` R ) )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 eqid 
 |-  ( invr ` R ) = ( invr ` R )
9 1 7 5 8 2 dvrval 
 |-  ( ( X e. B /\ .1. e. ( Unit ` R ) ) -> ( X ./ .1. ) = ( X ( .r ` R ) ( ( invr ` R ) ` .1. ) ) )
10 4 6 9 syl2anr 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X ./ .1. ) = ( X ( .r ` R ) ( ( invr ` R ) ` .1. ) ) )
11 8 3 1rinv 
 |-  ( R e. Ring -> ( ( invr ` R ) ` .1. ) = .1. )
12 11 adantr 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( invr ` R ) ` .1. ) = .1. )
13 12 oveq2d 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X ( .r ` R ) ( ( invr ` R ) ` .1. ) ) = ( X ( .r ` R ) .1. ) )
14 1 7 3 ringridm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X ( .r ` R ) .1. ) = X )
15 10 13 14 3eqtrd 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X ./ .1. ) = X )