Metamath Proof Explorer

Theorem rngsubdi

Description: Ring multiplication distributes over subtraction. ( subdi analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014) ringsubdi generalized for non-unital rings. (Revised by AV, 23-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 rngsubdi.b 
 |-  B = ( Base ` R )
2 rngsubdi.t 
 |-  .x. = ( .r ` R )
3 rngsubdi.m 
 |-  .- = ( -g ` R )
4 rngsubdi.r 
 |-  ( ph -> R e. Rng )
5 rngsubdi.x 
 |-  ( ph -> X e. B )
6 rngsubdi.y 
 |-  ( ph -> Y e. B )
7 rngsubdi.z 
 |-  ( ph -> Z e. B )
8 eqid 
 |-  ( invg ` R ) = ( invg ` R )
9 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
10 4 9 syl 
 |-  ( ph -> R e. Grp )
11 1 8 10 7 grpinvcld 
 |-  ( ph -> ( ( invg ` R ) ` Z ) e. B )
12 eqid 
 |-  ( +g ` R ) = ( +g ` R )
13 1 12 2 rngdi 
 |-  ( ( R e. Rng /\ ( X e. B /\ Y e. B /\ ( ( invg ` R ) ` Z ) e. B ) ) -> ( X .x. ( Y ( +g ` R ) ( ( invg ` R ) ` Z ) ) ) = ( ( X .x. Y ) ( +g ` R ) ( X .x. ( ( invg ` R ) ` Z ) ) ) )
14 4 5 6 11 13 syl13anc 
 |-  ( ph -> ( X .x. ( Y ( +g ` R ) ( ( invg ` R ) ` Z ) ) ) = ( ( X .x. Y ) ( +g ` R ) ( X .x. ( ( invg ` R ) ` Z ) ) ) )
15 1 2 8 4 5 7 rngmneg2 
 |-  ( ph -> ( X .x. ( ( invg ` R ) ` Z ) ) = ( ( invg ` R ) ` ( X .x. Z ) ) )
16 15 oveq2d 
 |-  ( ph -> ( ( X .x. Y ) ( +g ` R ) ( X .x. ( ( invg ` R ) ` Z ) ) ) = ( ( X .x. Y ) ( +g ` R ) ( ( invg ` R ) ` ( X .x. Z ) ) ) )
17 14 16 eqtrd 
 |-  ( ph -> ( X .x. ( Y ( +g ` R ) ( ( invg ` R ) ` Z ) ) ) = ( ( X .x. Y ) ( +g ` R ) ( ( invg ` R ) ` ( X .x. Z ) ) ) )
18 1 12 8 3 grpsubval 
 |-  ( ( Y e. B /\ Z e. B ) -> ( Y .- Z ) = ( Y ( +g ` R ) ( ( invg ` R ) ` Z ) ) )
19 6 7 18 syl2anc 
 |-  ( ph -> ( Y .- Z ) = ( Y ( +g ` R ) ( ( invg ` R ) ` Z ) ) )
20 19 oveq2d 
 |-  ( ph -> ( X .x. ( Y .- Z ) ) = ( X .x. ( Y ( +g ` R ) ( ( invg ` R ) ` Z ) ) ) )
21 1 2 rngcl 
 |-  ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
22 4 5 6 21 syl3anc 
 |-  ( ph -> ( X .x. Y ) e. B )
23 1 2 rngcl 
 |-  ( ( R e. Rng /\ X e. B /\ Z e. B ) -> ( X .x. Z ) e. B )
24 4 5 7 23 syl3anc 
 |-  ( ph -> ( X .x. Z ) e. B )
25 1 12 8 3 grpsubval 
 |-  ( ( ( X .x. Y ) e. B /\ ( X .x. Z ) e. B ) -> ( ( X .x. Y ) .- ( X .x. Z ) ) = ( ( X .x. Y ) ( +g ` R ) ( ( invg ` R ) ` ( X .x. Z ) ) ) )
26 22 24 25 syl2anc 
 |-  ( ph -> ( ( X .x. Y ) .- ( X .x. Z ) ) = ( ( X .x. Y ) ( +g ` R ) ( ( invg ` R ) ` ( X .x. Z ) ) ) )
27 17 20 26 3eqtr4d 
 |-  ( ph -> ( X .x. ( Y .- Z ) ) = ( ( X .x. Y ) .- ( X .x. Z ) ) )