This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )