Theorem rrgeq0

Description: Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	rrgval.e	|- E = ( RLReg ` R )
	rrgval.b	|- B = ( Base ` R )
	rrgval.t	|- .x. = ( .r ` R )
	rrgval.z	|- .0. = ( 0g ` R )
Assertion	rrgeq0	|- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> Y = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		rrgval.e	|- E = ( RLReg ` R )
2		rrgval.b	|- B = ( Base ` R )
3		rrgval.t	|- .x. = ( .r ` R )
4		rrgval.z	|- .0. = ( 0g ` R )
5	1 2 3 4	rrgeq0i	|- ( ( X e. E /\ Y e. B ) -> ( ( X .x. Y ) = .0. -> Y = .0. ) )
6	5	3adant1	|- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> ( ( X .x. Y ) = .0. -> Y = .0. ) )
7		simp1	|- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> R e. Ring )
8	1 2 3 4	rrgval	|- E = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) }
9	8	ssrab3	|- E C_ B
10		simp2	|- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> X e. E )
11	9 10	sseldi	|- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> X e. B )
12	2 3 4	ringrz	|- ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )
13	7 11 12	syl2anc	|- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> ( X .x. .0. ) = .0. )
14		oveq2	|- ( Y = .0. -> ( X .x. Y ) = ( X .x. .0. ) )
15	14	eqeq1d	|- ( Y = .0. -> ( ( X .x. Y ) = .0. <-> ( X .x. .0. ) = .0. ) )
16	13 15	syl5ibrcom	|- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> ( Y = .0. -> ( X .x. Y ) = .0. ) )
17	6 16	impbid	|- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> Y = .0. ) )