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

Metamath Proof Explorer

Theorem dvdsr01

Description: In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg .) (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses dvdsr0.b 
|- B = ( Base ` R )
dvdsr0.d 
|- .|| = ( ||r ` R )
dvdsr0.z 
|- .0. = ( 0g ` R )
Assertion dvdsr01 
|- ( ( R e. Ring /\ X e. B ) -> X .|| .0. )

Proof

Step Hyp Ref Expression
1 dvdsr0.b 
 |-  B = ( Base ` R )
2 dvdsr0.d 
 |-  .|| = ( ||r ` R )
3 dvdsr0.z 
 |-  .0. = ( 0g ` R )
4 1 3 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
5 eqid 
 |-  ( .r ` R ) = ( .r ` R )
6 1 5 3 ringlz 
 |-  ( ( R e. Ring /\ X e. B ) -> ( .0. ( .r ` R ) X ) = .0. )
7 oveq1 
 |-  ( x = .0. -> ( x ( .r ` R ) X ) = ( .0. ( .r ` R ) X ) )
8 7 eqeq1d 
 |-  ( x = .0. -> ( ( x ( .r ` R ) X ) = .0. <-> ( .0. ( .r ` R ) X ) = .0. ) )
9 8 rspcev 
 |-  ( ( .0. e. B /\ ( .0. ( .r ` R ) X ) = .0. ) -> E. x e. B ( x ( .r ` R ) X ) = .0. )
10 4 6 9 syl2an2r 
 |-  ( ( R e. Ring /\ X e. B ) -> E. x e. B ( x ( .r ` R ) X ) = .0. )
11 1 2 5 dvdsr2 
 |-  ( X e. B -> ( X .|| .0. <-> E. x e. B ( x ( .r ` R ) X ) = .0. ) )
12 11 adantl 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .|| .0. <-> E. x e. B ( x ( .r ` R ) X ) = .0. ) )
13 10 12 mpbird 
 |-  ( ( R e. Ring /\ X e. B ) -> X .|| .0. )