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. )