Theorem ringdi22

Description: Expand the product of two sums in a ring. (Contributed by Thierry Arnoux, 3-Jun-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 )
	ringdi22.t	|- ( ph -> T e. B )
Assertion	ringdi22	|- ( ph -> ( ( X .+ Y ) .x. ( Z .+ T ) ) = ( ( ( X .x. Z ) .+ ( Y .x. Z ) ) .+ ( ( X .x. T ) .+ ( Y .x. T ) ) ) )

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		ringdi22.t	|- ( ph -> T e. B )
9	4	ringgrpd	|- ( ph -> R e. Grp )
10	1 2 9 5 6	grpcld	|- ( ph -> ( X .+ Y ) e. B )
11	1 2 3 4 10 7 8	ringdid	|- ( ph -> ( ( X .+ Y ) .x. ( Z .+ T ) ) = ( ( ( X .+ Y ) .x. Z ) .+ ( ( X .+ Y ) .x. T ) ) )
12	1 2 3 4 5 6 7	ringdird	|- ( ph -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
13	1 2 3 4 5 6 8	ringdird	|- ( ph -> ( ( X .+ Y ) .x. T ) = ( ( X .x. T ) .+ ( Y .x. T ) ) )
14	12 13	oveq12d	|- ( ph -> ( ( ( X .+ Y ) .x. Z ) .+ ( ( X .+ Y ) .x. T ) ) = ( ( ( X .x. Z ) .+ ( Y .x. Z ) ) .+ ( ( X .x. T ) .+ ( Y .x. T ) ) ) )
15	11 14	eqtrd	|- ( ph -> ( ( X .+ Y ) .x. ( Z .+ T ) ) = ( ( ( X .x. Z ) .+ ( Y .x. Z ) ) .+ ( ( X .x. T ) .+ ( Y .x. T ) ) ) )