Theorem ringdi22

Description: Expand the product of two sums in a ring. (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	ringdi22.1	|- B = ( Base ` R )
	ringdi22.2	|- .+ = ( +g ` R )
	ringdi22.3	|- .x. = ( .r ` R )
	ringdi22.4	|- ( ph -> R e. Ring )
	ringdi22.5	|- ( ph -> X e. B )
	ringdi22.6	|- ( ph -> Y e. B )
	ringdi22.7	|- ( ph -> Z e. B )
	ringdi22.8	|- ( 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		ringdi22.1	|- B = ( Base ` R )
2		ringdi22.2	|- .+ = ( +g ` R )
3		ringdi22.3	|- .x. = ( .r ` R )
4		ringdi22.4	|- ( ph -> R e. Ring )
5		ringdi22.5	|- ( ph -> X e. B )
6		ringdi22.6	|- ( ph -> Y e. B )
7		ringdi22.7	|- ( ph -> Z e. B )
8		ringdi22.8	|- ( 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 ) ) ) )