Theorem ringsubdir

Description: Ring multiplication distributes over subtraction. ( subdir analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)

	Ref	Expression
Hypotheses	ringsubdi.b	|- B = ( Base ` R )
	ringsubdi.t	|- .x. = ( .r ` R )
	ringsubdi.m	|- .- = ( -g ` R )
	ringsubdi.r	|- ( ph -> R e. Ring )
	ringsubdi.x	|- ( ph -> X e. B )
	ringsubdi.y	|- ( ph -> Y e. B )
	ringsubdi.z	|- ( ph -> Z e. B )
Assertion	ringsubdir	|- ( ph -> ( ( X .- Y ) .x. Z ) = ( ( X .x. Z ) .- ( Y .x. Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		ringsubdi.b	|- B = ( Base ` R )
2		ringsubdi.t	|- .x. = ( .r ` R )
3		ringsubdi.m	|- .- = ( -g ` R )
4		ringsubdi.r	|- ( ph -> R e. Ring )
5		ringsubdi.x	|- ( ph -> X e. B )
6		ringsubdi.y	|- ( ph -> Y e. B )
7		ringsubdi.z	|- ( ph -> Z e. B )
8		ringrng	|- ( R e. Ring -> R e. Rng )
9	4 8	syl	|- ( ph -> R e. Rng )
10	1 2 3 9 5 6 7	rngsubdir	|- ( ph -> ( ( X .- Y ) .x. Z ) = ( ( X .x. Z ) .- ( Y .x. Z ) ) )