Theorem ringdird

Description: Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Thierry Arnoux, 4-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ringdid.b	|- B = ( Base ` R )
2		ringdid.p	|- .+ = ( +g ` R )
3		ringdid.m	|- .x. = ( .r ` R )
4		ringdid.r	|- ( ph -> R e. Ring )
5		ringdid.x	|- ( ph -> X e. B )
6		ringdid.y	|- ( ph -> Y e. B )
7		ringdid.z	|- ( ph -> Z e. B )
8	1 2 3	ringdir	|- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
9	4 5 6 7 8	syl13anc	|- ( ph -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )