Description: Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rngdi.b | |
|
rngdi.p | |
||
rngdi.t | |
||
Assertion | rngdir | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rngdi.b | |
|
2 | rngdi.p | |
|
3 | rngdi.t | |
|
4 | eqid | |
|
5 | 1 4 2 3 | isrng | |
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 | |
41 | 5 40 | sylbi | |
42 | 41 | imp | |