# Metamath Proof Explorer

## Theorem rngoass

Description: Associative law for the multiplication operation of a ring. (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 rngoass ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{H}{B}\right){H}{C}={A}{H}\left({B}{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 simp1 ${⊢}\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 \left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{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}}\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{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}}\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)$
10 6 9 syl ${⊢}{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({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)$
11 oveq1 ${⊢}{x}={A}\to {x}{H}{y}={A}{H}{y}$
12 11 oveq1d ${⊢}{x}={A}\to \left({x}{H}{y}\right){H}{z}=\left({A}{H}{y}\right){H}{z}$
13 oveq1 ${⊢}{x}={A}\to {x}{H}\left({y}{H}{z}\right)={A}{H}\left({y}{H}{z}\right)$
14 12 13 eqeq12d ${⊢}{x}={A}\to \left(\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)↔\left({A}{H}{y}\right){H}{z}={A}{H}\left({y}{H}{z}\right)\right)$
15 oveq2 ${⊢}{y}={B}\to {A}{H}{y}={A}{H}{B}$
16 15 oveq1d ${⊢}{y}={B}\to \left({A}{H}{y}\right){H}{z}=\left({A}{H}{B}\right){H}{z}$
17 oveq1 ${⊢}{y}={B}\to {y}{H}{z}={B}{H}{z}$
18 17 oveq2d ${⊢}{y}={B}\to {A}{H}\left({y}{H}{z}\right)={A}{H}\left({B}{H}{z}\right)$
19 16 18 eqeq12d ${⊢}{y}={B}\to \left(\left({A}{H}{y}\right){H}{z}={A}{H}\left({y}{H}{z}\right)↔\left({A}{H}{B}\right){H}{z}={A}{H}\left({B}{H}{z}\right)\right)$
20 oveq2 ${⊢}{z}={C}\to \left({A}{H}{B}\right){H}{z}=\left({A}{H}{B}\right){H}{C}$
21 oveq2 ${⊢}{z}={C}\to {B}{H}{z}={B}{H}{C}$
22 21 oveq2d ${⊢}{z}={C}\to {A}{H}\left({B}{H}{z}\right)={A}{H}\left({B}{H}{C}\right)$
23 20 22 eqeq12d ${⊢}{z}={C}\to \left(\left({A}{H}{B}\right){H}{z}={A}{H}\left({B}{H}{z}\right)↔\left({A}{H}{B}\right){H}{C}={A}{H}\left({B}{H}{C}\right)\right)$
24 14 19 23 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}}\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)\to \left({A}{H}{B}\right){H}{C}={A}{H}\left({B}{H}{C}\right)\right)$
25 10 24 mpan9 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{H}{B}\right){H}{C}={A}{H}\left({B}{H}{C}\right)$