# Metamath Proof Explorer

## Theorem grpoass

Description: A group operation is associative. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 ${⊢}{X}=\mathrm{ran}{G}$
Assertion grpoass ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}{C}={A}{G}\left({B}{G}{C}\right)$

### Proof

Step Hyp Ref Expression
1 grpfo.1 ${⊢}{X}=\mathrm{ran}{G}$
2 1 isgrpo ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}\in \mathrm{GrpOp}↔\left({G}:{X}×{X}⟶{X}\wedge \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}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
3 2 ibi ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}:{X}×{X}⟶{X}\wedge \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}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)$
4 3 simp2d ${⊢}{G}\in \mathrm{GrpOp}\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}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)$
5 oveq1 ${⊢}{x}={A}\to {x}{G}{y}={A}{G}{y}$
6 5 oveq1d ${⊢}{x}={A}\to \left({x}{G}{y}\right){G}{z}=\left({A}{G}{y}\right){G}{z}$
7 oveq1 ${⊢}{x}={A}\to {x}{G}\left({y}{G}{z}\right)={A}{G}\left({y}{G}{z}\right)$
8 6 7 eqeq12d ${⊢}{x}={A}\to \left(\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)↔\left({A}{G}{y}\right){G}{z}={A}{G}\left({y}{G}{z}\right)\right)$
9 oveq2 ${⊢}{y}={B}\to {A}{G}{y}={A}{G}{B}$
10 9 oveq1d ${⊢}{y}={B}\to \left({A}{G}{y}\right){G}{z}=\left({A}{G}{B}\right){G}{z}$
11 oveq1 ${⊢}{y}={B}\to {y}{G}{z}={B}{G}{z}$
12 11 oveq2d ${⊢}{y}={B}\to {A}{G}\left({y}{G}{z}\right)={A}{G}\left({B}{G}{z}\right)$
13 10 12 eqeq12d ${⊢}{y}={B}\to \left(\left({A}{G}{y}\right){G}{z}={A}{G}\left({y}{G}{z}\right)↔\left({A}{G}{B}\right){G}{z}={A}{G}\left({B}{G}{z}\right)\right)$
14 oveq2 ${⊢}{z}={C}\to \left({A}{G}{B}\right){G}{z}=\left({A}{G}{B}\right){G}{C}$
15 oveq2 ${⊢}{z}={C}\to {B}{G}{z}={B}{G}{C}$
16 15 oveq2d ${⊢}{z}={C}\to {A}{G}\left({B}{G}{z}\right)={A}{G}\left({B}{G}{C}\right)$
17 14 16 eqeq12d ${⊢}{z}={C}\to \left(\left({A}{G}{B}\right){G}{z}={A}{G}\left({B}{G}{z}\right)↔\left({A}{G}{B}\right){G}{C}={A}{G}\left({B}{G}{C}\right)\right)$
18 8 13 17 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}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\to \left({A}{G}{B}\right){G}{C}={A}{G}\left({B}{G}{C}\right)\right)$
19 4 18 mpan9 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}{C}={A}{G}\left({B}{G}{C}\right)$