# Metamath Proof Explorer

## Theorem rngodi

Description: Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ringi.1 ${⊢}{G}={1}^{st}\left({R}\right)$
ringi.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
ringi.3 ${⊢}{X}=\mathrm{ran}{G}$
Assertion rngodi ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{H}\left({B}{G}{C}\right)=\left({A}{H}{B}\right){G}\left({A}{H}{C}\right)$

### Proof

Step Hyp Ref Expression
1 ringi.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 ringi.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 ringi.3 ${⊢}{X}=\mathrm{ran}{G}$
4 1 2 3 rngoi ${⊢}{R}\in \mathrm{RingOps}\to \left(\left({G}\in \mathrm{AbelOp}\wedge {H}:{X}×{X}⟶{X}\right)\wedge \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)\wedge {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)\wedge \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)\right)\right)$
5 4 simprd ${⊢}{R}\in \mathrm{RingOps}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)\wedge {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)\wedge \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)\right)$
6 5 simpld ${⊢}{R}\in \mathrm{RingOps}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)\wedge {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)\wedge \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)\right)$
7 simp2 ${⊢}\left(\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)\wedge {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)\wedge \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)\right)\to {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)$
8 7 ralimi ${⊢}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)\wedge {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)\wedge \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)$
9 8 2ralimi ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)\wedge {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)\wedge \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)$
10 oveq1 ${⊢}{x}={A}\to {x}{H}\left({y}{G}{z}\right)={A}{H}\left({y}{G}{z}\right)$
11 oveq1 ${⊢}{x}={A}\to {x}{H}{y}={A}{H}{y}$
12 oveq1 ${⊢}{x}={A}\to {x}{H}{z}={A}{H}{z}$
13 11 12 oveq12d ${⊢}{x}={A}\to \left({x}{H}{y}\right){G}\left({x}{H}{z}\right)=\left({A}{H}{y}\right){G}\left({A}{H}{z}\right)$
14 10 13 eqeq12d ${⊢}{x}={A}\to \left({x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)↔{A}{H}\left({y}{G}{z}\right)=\left({A}{H}{y}\right){G}\left({A}{H}{z}\right)\right)$
15 oveq1 ${⊢}{y}={B}\to {y}{G}{z}={B}{G}{z}$
16 15 oveq2d ${⊢}{y}={B}\to {A}{H}\left({y}{G}{z}\right)={A}{H}\left({B}{G}{z}\right)$
17 oveq2 ${⊢}{y}={B}\to {A}{H}{y}={A}{H}{B}$
18 17 oveq1d ${⊢}{y}={B}\to \left({A}{H}{y}\right){G}\left({A}{H}{z}\right)=\left({A}{H}{B}\right){G}\left({A}{H}{z}\right)$
19 16 18 eqeq12d ${⊢}{y}={B}\to \left({A}{H}\left({y}{G}{z}\right)=\left({A}{H}{y}\right){G}\left({A}{H}{z}\right)↔{A}{H}\left({B}{G}{z}\right)=\left({A}{H}{B}\right){G}\left({A}{H}{z}\right)\right)$
20 oveq2 ${⊢}{z}={C}\to {B}{G}{z}={B}{G}{C}$
21 20 oveq2d ${⊢}{z}={C}\to {A}{H}\left({B}{G}{z}\right)={A}{H}\left({B}{G}{C}\right)$
22 oveq2 ${⊢}{z}={C}\to {A}{H}{z}={A}{H}{C}$
23 22 oveq2d ${⊢}{z}={C}\to \left({A}{H}{B}\right){G}\left({A}{H}{z}\right)=\left({A}{H}{B}\right){G}\left({A}{H}{C}\right)$
24 21 23 eqeq12d ${⊢}{z}={C}\to \left({A}{H}\left({B}{G}{z}\right)=\left({A}{H}{B}\right){G}\left({A}{H}{z}\right)↔{A}{H}\left({B}{G}{C}\right)=\left({A}{H}{B}\right){G}\left({A}{H}{C}\right)\right)$
25 14 19 24 rspc3v ${⊢}\left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)\to {A}{H}\left({B}{G}{C}\right)=\left({A}{H}{B}\right){G}\left({A}{H}{C}\right)\right)$
26 9 25 syl5 ${⊢}\left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)\wedge {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)\wedge \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)\right)\to {A}{H}\left({B}{G}{C}\right)=\left({A}{H}{B}\right){G}\left({A}{H}{C}\right)\right)$
27 6 26 mpan9 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{H}\left({B}{G}{C}\right)=\left({A}{H}{B}\right){G}\left({A}{H}{C}\right)$