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 = ran G$
	Assertion	grpoass	$⊢ (G \in GrpOp \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = A G (B G C)$

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	$⊢ X = ran G$
2	1	isgrpo	$⊢ G \in GrpOp \to (G \in GrpOp \leftrightarrow (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists u \in X \forall x \in X (u G x = x \land \exists y \in X y G x = u)))$
3	2	ibi	$⊢ G \in GrpOp \to (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists u \in X \forall x \in X (u G x = x \land \exists y \in X y G x = u))$
4	3	simp2d	$⊢ G \in GrpOp \to \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z)$
5		oveq1	$⊢ x = A \to x G y = A G y$
6	5	oveq1d	$⊢ x = A \to (x G y) G z = (A G y) G z$
7		oveq1	$⊢ x = A \to x G (y G z) = A G (y G z)$
8	6 7	eqeq12d	$⊢ x = A \to ((x G y) G z = x G (y G z) \leftrightarrow (A G y) G z = A G (y G z))$
9		oveq2	$⊢ y = B \to A G y = A G B$
10	9	oveq1d	$⊢ y = B \to (A G y) G z = (A G B) G z$
11		oveq1	$⊢ y = B \to y G z = B G z$
12	11	oveq2d	$⊢ y = B \to A G (y G z) = A G (B G z)$
13	10 12	eqeq12d	$⊢ y = B \to ((A G y) G z = A G (y G z) \leftrightarrow (A G B) G z = A G (B G z))$
14		oveq2	$⊢ z = C \to (A G B) G z = (A G B) G C$
15		oveq2	$⊢ z = C \to B G z = B G C$
16	15	oveq2d	$⊢ z = C \to A G (B G z) = A G (B G C)$
17	14 16	eqeq12d	$⊢ z = C \to ((A G B) G z = A G (B G z) \leftrightarrow (A G B) G C = A G (B G C))$
18	8 13 17	rspc3v	$⊢ (A \in X \land B \in X \land C \in X) \to (\forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \to (A G B) G C = A G (B G C))$
19	4 18	mpan9	$⊢ (G \in GrpOp \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = A G (B G C)$