Theorem dvdsr02

Description: Only zero is divisible by zero. (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	dvdsr02	|- ( ( R e. Ring /\ X e. B ) -> ( .0. .|| X <-> 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	4	adantr	|- ( ( R e. Ring /\ X e. B ) -> .0. e. B )
6		eqid	|- ( .r ` R ) = ( .r ` R )
7	1 2 6	dvdsr2	|- ( .0. e. B -> ( .0. .|| X <-> E. x e. B ( x ( .r ` R ) .0. ) = X ) )
8	5 7	syl	|- ( ( R e. Ring /\ X e. B ) -> ( .0. .|| X <-> E. x e. B ( x ( .r ` R ) .0. ) = X ) )
9	1 6 3	ringrz	|- ( ( R e. Ring /\ x e. B ) -> ( x ( .r ` R ) .0. ) = .0. )
10	9	eqeq1d	|- ( ( R e. Ring /\ x e. B ) -> ( ( x ( .r ` R ) .0. ) = X <-> .0. = X ) )
11		eqcom	|- ( .0. = X <-> X = .0. )
12	10 11	syl6bb	|- ( ( R e. Ring /\ x e. B ) -> ( ( x ( .r ` R ) .0. ) = X <-> X = .0. ) )
13	12	rexbidva	|- ( R e. Ring -> ( E. x e. B ( x ( .r ` R ) .0. ) = X <-> E. x e. B X = .0. ) )
14		ringgrp	|- ( R e. Ring -> R e. Grp )
15	1	grpbn0	|- ( R e. Grp -> B =/= (/) )
16		r19.9rzv	|- ( B =/= (/) -> ( X = .0. <-> E. x e. B X = .0. ) )
17	14 15 16	3syl	|- ( R e. Ring -> ( X = .0. <-> E. x e. B X = .0. ) )
18	13 17	bitr4d	|- ( R e. Ring -> ( E. x e. B ( x ( .r ` R ) .0. ) = X <-> X = .0. ) )
19	18	adantr	|- ( ( R e. Ring /\ X e. B ) -> ( E. x e. B ( x ( .r ` R ) .0. ) = X <-> X = .0. ) )
20	8 19	bitrd	|- ( ( R e. Ring /\ X e. B ) -> ( .0. .|| X <-> X = .0. ) )