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

Metamath Proof Explorer

Theorem rrgeq0i

Description: Property of a left-regular element. (Contributed by Stefan O'Rear, 22-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 rrgeq0i 
|- ( ( 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 isrrg 
 |-  ( X e. E <-> ( X e. B /\ A. y e. B ( ( X .x. y ) = .0. -> y = .0. ) ) )
6 5 simprbi 
 |-  ( X e. E -> A. y e. B ( ( X .x. y ) = .0. -> y = .0. ) )
7 oveq2 
 |-  ( y = Y -> ( X .x. y ) = ( X .x. Y ) )
8 7 eqeq1d 
 |-  ( y = Y -> ( ( X .x. y ) = .0. <-> ( X .x. Y ) = .0. ) )
9 eqeq1 
 |-  ( y = Y -> ( y = .0. <-> Y = .0. ) )
10 8 9 imbi12d 
 |-  ( y = Y -> ( ( ( X .x. y ) = .0. -> y = .0. ) <-> ( ( X .x. Y ) = .0. -> Y = .0. ) ) )
11 10 rspcv 
 |-  ( Y e. B -> ( A. y e. B ( ( X .x. y ) = .0. -> y = .0. ) -> ( ( X .x. Y ) = .0. -> Y = .0. ) ) )
12 6 11 mpan9 
 |-  ( ( X e. E /\ Y e. B ) -> ( ( X .x. Y ) = .0. -> Y = .0. ) )