Metamath Proof Explorer

Theorem rngsubdir

Description: Ring multiplication distributes over subtraction. ( subdir analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014) Generalization of ringsubdir . (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 rngsubdir 
|- ( ph -> ( ( X .- Y ) .x. Z ) = ( ( X .x. Z ) .- ( Y .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 6 grpinvcld 
 |-  ( ph -> ( ( invg ` R ) ` Y ) e. B )
12 eqid 
 |-  ( +g ` R ) = ( +g ` R )
13 1 12 2 rngdir 
 |-  ( ( R e. Rng /\ ( X e. B /\ ( ( invg ` R ) ` Y ) e. B /\ Z e. B ) ) -> ( ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) .x. Z ) = ( ( X .x. Z ) ( +g ` R ) ( ( ( invg ` R ) ` Y ) .x. Z ) ) )
14 4 5 11 7 13 syl13anc 
 |-  ( ph -> ( ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) .x. Z ) = ( ( X .x. Z ) ( +g ` R ) ( ( ( invg ` R ) ` Y ) .x. Z ) ) )
15 1 2 8 4 6 7 rngmneg1 
 |-  ( ph -> ( ( ( invg ` R ) ` Y ) .x. Z ) = ( ( invg ` R ) ` ( Y .x. Z ) ) )
16 15 oveq2d 
 |-  ( ph -> ( ( X .x. Z ) ( +g ` R ) ( ( ( invg ` R ) ` Y ) .x. Z ) ) = ( ( X .x. Z ) ( +g ` R ) ( ( invg ` R ) ` ( Y .x. Z ) ) ) )
17 14 16 eqtrd 
 |-  ( ph -> ( ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) .x. Z ) = ( ( X .x. Z ) ( +g ` R ) ( ( invg ` R ) ` ( Y .x. Z ) ) ) )
18 1 12 8 3 grpsubval 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) )
19 5 6 18 syl2anc 
 |-  ( ph -> ( X .- Y ) = ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) )
20 19 oveq1d 
 |-  ( ph -> ( ( X .- Y ) .x. Z ) = ( ( X ( +g ` R ) ( ( invg ` R ) ` Y ) ) .x. Z ) )
21 1 2 rngcl 
 |-  ( ( R e. Rng /\ X e. B /\ Z e. B ) -> ( X .x. Z ) e. B )
22 4 5 7 21 syl3anc 
 |-  ( ph -> ( X .x. Z ) e. B )
23 1 2 rngcl 
 |-  ( ( R e. Rng /\ Y e. B /\ Z e. B ) -> ( Y .x. Z ) e. B )
24 4 6 7 23 syl3anc 
 |-  ( ph -> ( Y .x. Z ) e. B )
25 1 12 8 3 grpsubval 
 |-  ( ( ( X .x. Z ) e. B /\ ( Y .x. Z ) e. B ) -> ( ( X .x. Z ) .- ( Y .x. Z ) ) = ( ( X .x. Z ) ( +g ` R ) ( ( invg ` R ) ` ( Y .x. Z ) ) ) )
26 22 24 25 syl2anc 
 |-  ( ph -> ( ( X .x. Z ) .- ( Y .x. Z ) ) = ( ( X .x. Z ) ( +g ` R ) ( ( invg ` R ) ` ( Y .x. Z ) ) ) )
27 17 20 26 3eqtr4d 
 |-  ( ph -> ( ( X .- Y ) .x. Z ) = ( ( X .x. Z ) .- ( Y .x. Z ) ) )