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

Metamath Proof Explorer

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