# 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}={\mathrm{Base}}_{{R}}$
rngdi.p
rngdi.t
Assertion rngdir

### Proof

Step Hyp Ref Expression
1 rngdi.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 rngdi.p
3 rngdi.t
4 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
5 1 4 2 3 isrng Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
6 oveq1
7 oveq1
8 oveq1
9 7 8 oveq12d
10 6 9 eqeq12d
11 oveq1
12 11 oveq1d
13 8 oveq1d
14 12 13 eqeq12d
15 10 14 anbi12d
16 oveq1
17 16 oveq2d
18 oveq2
19 18 oveq1d
20 17 19 eqeq12d
21 oveq2
22 21 oveq1d
23 oveq1
24 23 oveq2d
25 22 24 eqeq12d
26 20 25 anbi12d
27 oveq2
28 27 oveq2d
29 oveq2
30 29 oveq2d
31 28 30 eqeq12d
32 oveq2
33 oveq2
34 29 33 oveq12d
35 32 34 eqeq12d
36 31 35 anbi12d
37 15 26 36 rspc3v
38 simpr
39 37 38 syl6com
40 39 3ad2ant3 Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
41 5 40 sylbi
42 41 imp