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