Theorem dvdsrmul

Description: A left-multiple of X is divisible by X . (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	dvdsr.1	|- B = ( Base ` R )
	dvdsr.2	|- .|| = ( ||r ` R )
	dvdsr.3	|- .x. = ( .r ` R )
Assertion	dvdsrmul	|- ( ( X e. B /\ Y e. B ) -> X .|| ( Y .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	|- B = ( Base ` R )
2		dvdsr.2	|- .|| = ( ||r ` R )
3		dvdsr.3	|- .x. = ( .r ` R )
4		simpl	|- ( ( X e. B /\ Y e. B ) -> X e. B )
5		simpr	|- ( ( X e. B /\ Y e. B ) -> Y e. B )
6		eqid	|- ( Y .x. X ) = ( Y .x. X )
7		oveq1	|- ( z = Y -> ( z .x. X ) = ( Y .x. X ) )
8	7	eqeq1d	|- ( z = Y -> ( ( z .x. X ) = ( Y .x. X ) <-> ( Y .x. X ) = ( Y .x. X ) ) )
9	8	rspcev	|- ( ( Y e. B /\ ( Y .x. X ) = ( Y .x. X ) ) -> E. z e. B ( z .x. X ) = ( Y .x. X ) )
10	5 6 9	sylancl	|- ( ( X e. B /\ Y e. B ) -> E. z e. B ( z .x. X ) = ( Y .x. X ) )
11	1 2 3	dvdsr	|- ( X .|| ( Y .x. X ) <-> ( X e. B /\ E. z e. B ( z .x. X ) = ( Y .x. X ) ) )
12	4 10 11	sylanbrc	|- ( ( X e. B /\ Y e. B ) -> X .|| ( Y .x. X ) )