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

Metamath Proof Explorer

Theorem domnrrg

Description: In a domain, a nonzero element is a regular element. (Contributed by Mario Carneiro, 28-Mar-2015)

Ref Expression
Hypotheses isdomn2.b 
|- B = ( Base ` R )
isdomn2.t 
|- E = ( RLReg ` R )
isdomn2.z 
|- .0. = ( 0g ` R )
Assertion domnrrg 
|- ( ( R e. Domn /\ X e. B /\ X =/= .0. ) -> X e. E )

Proof

Step Hyp Ref Expression
1 isdomn2.b 
 |-  B = ( Base ` R )
2 isdomn2.t 
 |-  E = ( RLReg ` R )
3 isdomn2.z 
 |-  .0. = ( 0g ` R )
4 1 2 3 isdomn2 
 |-  ( R e. Domn <-> ( R e. NzRing /\ ( B \ { .0. } ) C_ E ) )
5 4 simprbi 
 |-  ( R e. Domn -> ( B \ { .0. } ) C_ E )
6 5 3ad2ant1 
 |-  ( ( R e. Domn /\ X e. B /\ X =/= .0. ) -> ( B \ { .0. } ) C_ E )
7 simp2 
 |-  ( ( R e. Domn /\ X e. B /\ X =/= .0. ) -> X e. B )
8 simp3 
 |-  ( ( R e. Domn /\ X e. B /\ X =/= .0. ) -> X =/= .0. )
9 eldifsn 
 |-  ( X e. ( B \ { .0. } ) <-> ( X e. B /\ X =/= .0. ) )
10 7 8 9 sylanbrc 
 |-  ( ( R e. Domn /\ X e. B /\ X =/= .0. ) -> X e. ( B \ { .0. } ) )
11 6 10 sseldd 
 |-  ( ( R e. Domn /\ X e. B /\ X =/= .0. ) -> X e. E )