Metamath Proof Explorer

Theorem rngdir

Description: Distributive law for the multiplication operation of a nonunital ring (right-distributivity). (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses rngdi.b 
|- B = ( Base ` R )
rngdi.p 
|- .+ = ( +g ` R )
rngdi.t 
|- .x. = ( .r ` R )
Assertion rngdir 
|- ( ( R e. Rng /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )

Proof

Step Hyp Ref Expression
1 rngdi.b 
 |-  B = ( Base ` R )
2 rngdi.p 
 |-  .+ = ( +g ` R )
3 rngdi.t 
 |-  .x. = ( .r ` R )
4 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
5 1 4 2 3 isrng 
 |-  ( R e. Rng <-> ( R e. Abel /\ ( mulGrp ` R ) e. Smgrp /\ A. a e. B A. b e. B A. c e. B ( ( a .x. ( b .+ c ) ) = ( ( a .x. b ) .+ ( a .x. c ) ) /\ ( ( a .+ b ) .x. c ) = ( ( a .x. c ) .+ ( b .x. c ) ) ) ) )
6 oveq1 
 |-  ( a = X -> ( a .x. ( b .+ c ) ) = ( X .x. ( b .+ c ) ) )
7 oveq1 
 |-  ( a = X -> ( a .x. b ) = ( X .x. b ) )
8 oveq1 
 |-  ( a = X -> ( a .x. c ) = ( X .x. c ) )
9 7 8 oveq12d 
 |-  ( a = X -> ( ( a .x. b ) .+ ( a .x. c ) ) = ( ( X .x. b ) .+ ( X .x. c ) ) )
10 6 9 eqeq12d 
 |-  ( a = X -> ( ( a .x. ( b .+ c ) ) = ( ( a .x. b ) .+ ( a .x. c ) ) <-> ( X .x. ( b .+ c ) ) = ( ( X .x. b ) .+ ( X .x. c ) ) ) )
11 oveq1 
 |-  ( a = X -> ( a .+ b ) = ( X .+ b ) )
12 11 oveq1d 
 |-  ( a = X -> ( ( a .+ b ) .x. c ) = ( ( X .+ b ) .x. c ) )
13 8 oveq1d 
 |-  ( a = X -> ( ( a .x. c ) .+ ( b .x. c ) ) = ( ( X .x. c ) .+ ( b .x. c ) ) )
14 12 13 eqeq12d 
 |-  ( a = X -> ( ( ( a .+ b ) .x. c ) = ( ( a .x. c ) .+ ( b .x. c ) ) <-> ( ( X .+ b ) .x. c ) = ( ( X .x. c ) .+ ( b .x. c ) ) ) )
15 10 14 anbi12d 
 |-  ( a = X -> ( ( ( a .x. ( b .+ c ) ) = ( ( a .x. b ) .+ ( a .x. c ) ) /\ ( ( a .+ b ) .x. c ) = ( ( a .x. c ) .+ ( b .x. c ) ) ) <-> ( ( X .x. ( b .+ c ) ) = ( ( X .x. b ) .+ ( X .x. c ) ) /\ ( ( X .+ b ) .x. c ) = ( ( X .x. c ) .+ ( b .x. c ) ) ) ) )
16 oveq1 
 |-  ( b = Y -> ( b .+ c ) = ( Y .+ c ) )
17 16 oveq2d 
 |-  ( b = Y -> ( X .x. ( b .+ c ) ) = ( X .x. ( Y .+ c ) ) )
18 oveq2 
 |-  ( b = Y -> ( X .x. b ) = ( X .x. Y ) )
19 18 oveq1d 
 |-  ( b = Y -> ( ( X .x. b ) .+ ( X .x. c ) ) = ( ( X .x. Y ) .+ ( X .x. c ) ) )
20 17 19 eqeq12d 
 |-  ( b = Y -> ( ( X .x. ( b .+ c ) ) = ( ( X .x. b ) .+ ( X .x. c ) ) <-> ( X .x. ( Y .+ c ) ) = ( ( X .x. Y ) .+ ( X .x. c ) ) ) )
21 oveq2 
 |-  ( b = Y -> ( X .+ b ) = ( X .+ Y ) )
22 21 oveq1d 
 |-  ( b = Y -> ( ( X .+ b ) .x. c ) = ( ( X .+ Y ) .x. c ) )
23 oveq1 
 |-  ( b = Y -> ( b .x. c ) = ( Y .x. c ) )
24 23 oveq2d 
 |-  ( b = Y -> ( ( X .x. c ) .+ ( b .x. c ) ) = ( ( X .x. c ) .+ ( Y .x. c ) ) )
25 22 24 eqeq12d 
 |-  ( b = Y -> ( ( ( X .+ b ) .x. c ) = ( ( X .x. c ) .+ ( b .x. c ) ) <-> ( ( X .+ Y ) .x. c ) = ( ( X .x. c ) .+ ( Y .x. c ) ) ) )
26 20 25 anbi12d 
 |-  ( b = Y -> ( ( ( X .x. ( b .+ c ) ) = ( ( X .x. b ) .+ ( X .x. c ) ) /\ ( ( X .+ b ) .x. c ) = ( ( X .x. c ) .+ ( b .x. c ) ) ) <-> ( ( X .x. ( Y .+ c ) ) = ( ( X .x. Y ) .+ ( X .x. c ) ) /\ ( ( X .+ Y ) .x. c ) = ( ( X .x. c ) .+ ( Y .x. c ) ) ) ) )
27 oveq2 
 |-  ( c = Z -> ( Y .+ c ) = ( Y .+ Z ) )
28 27 oveq2d 
 |-  ( c = Z -> ( X .x. ( Y .+ c ) ) = ( X .x. ( Y .+ Z ) ) )
29 oveq2 
 |-  ( c = Z -> ( X .x. c ) = ( X .x. Z ) )
30 29 oveq2d 
 |-  ( c = Z -> ( ( X .x. Y ) .+ ( X .x. c ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) )
31 28 30 eqeq12d 
 |-  ( c = Z -> ( ( X .x. ( Y .+ c ) ) = ( ( X .x. Y ) .+ ( X .x. c ) ) <-> ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) ) )
32 oveq2 
 |-  ( c = Z -> ( ( X .+ Y ) .x. c ) = ( ( X .+ Y ) .x. Z ) )
33 oveq2 
 |-  ( c = Z -> ( Y .x. c ) = ( Y .x. Z ) )
34 29 33 oveq12d 
 |-  ( c = Z -> ( ( X .x. c ) .+ ( Y .x. c ) ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
35 32 34 eqeq12d 
 |-  ( c = Z -> ( ( ( X .+ Y ) .x. c ) = ( ( X .x. c ) .+ ( Y .x. c ) ) <-> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )
36 31 35 anbi12d 
 |-  ( c = Z -> ( ( ( X .x. ( Y .+ c ) ) = ( ( X .x. Y ) .+ ( X .x. c ) ) /\ ( ( X .+ Y ) .x. c ) = ( ( X .x. c ) .+ ( Y .x. c ) ) ) <-> ( ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) /\ ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) ) )
37 15 26 36 rspc3v 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( A. a e. B A. b e. B A. c e. B ( ( a .x. ( b .+ c ) ) = ( ( a .x. b ) .+ ( a .x. c ) ) /\ ( ( a .+ b ) .x. c ) = ( ( a .x. c ) .+ ( b .x. c ) ) ) -> ( ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) /\ ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) ) )
38 simpr 
 |-  ( ( ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) /\ ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
39 37 38 syl6com 
 |-  ( A. a e. B A. b e. B A. c e. B ( ( a .x. ( b .+ c ) ) = ( ( a .x. b ) .+ ( a .x. c ) ) /\ ( ( a .+ b ) .x. c ) = ( ( a .x. c ) .+ ( b .x. c ) ) ) -> ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )
40 39 3ad2ant3 
 |-  ( ( R e. Abel /\ ( mulGrp ` R ) e. Smgrp /\ A. a e. B A. b e. B A. c e. B ( ( a .x. ( b .+ c ) ) = ( ( a .x. b ) .+ ( a .x. c ) ) /\ ( ( a .+ b ) .x. c ) = ( ( a .x. c ) .+ ( b .x. c ) ) ) ) -> ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )
41 5 40 sylbi 
 |-  ( R e. Rng -> ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )
42 41 imp 
 |-  ( ( R e. Rng /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )