Theorem domnrrg

Description: In a domain, any nonzero element is a nonzero-divisor. (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 )