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 ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → 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 ∈ GrpOp → G ∈ GrpOp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
3 2 ibi ⊢ G ∈ GrpOp → G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
4 3 simp2d ⊢ G ∈ GrpOp → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
5 oveq1 ⊢ x = A → x G y = A G y
6 5 oveq1d ⊢ x = A → x G y G z = A G y G z
7 oveq1 ⊢ x = A → x G y G z = A G y G z
8 6 7 eqeq12d ⊢ x = A → x G y G z = x G y G z ↔ A G y G z = A G y G z
9 oveq2 ⊢ y = B → A G y = A G B
10 9 oveq1d ⊢ y = B → A G y G z = A G B G z
11 oveq1 ⊢ y = B → y G z = B G z
12 11 oveq2d ⊢ y = B → A G y G z = A G B G z
13 10 12 eqeq12d ⊢ y = B → A G y G z = A G y G z ↔ A G B G z = A G B G z
14 oveq2 ⊢ z = C → A G B G z = A G B G C
15 oveq2 ⊢ z = C → B G z = B G C
16 15 oveq2d ⊢ z = C → A G B G z = A G B G C
17 14 16 eqeq12d ⊢ z = C → A G B G z = A G B G z ↔ A G B G C = A G B G C
18 8 13 17 rspc3v ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z → A G B G C = A G B G C
19 4 18 mpan9 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G B G C