sgrpass

Description: A semigroup operation is associative. (Contributed by FL, 2-Nov-2009) (Revised by AV, 30-Jan-2020)

	Ref	Expression
Hypotheses	sgrpass.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	sgrpass.o	⊢ ⚬ = ( +_g ‘ 𝐺 )
Assertion	sgrpass	⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sgrpass.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		sgrpass.o	⊢ ⚬ = ( +_g ‘ 𝐺 )
3	1 2	issgrp	⊢ ( 𝐺 ∈ Smgrp ↔ ( 𝐺 ∈ Mgm ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
4		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⚬ 𝑦 ) = ( 𝑋 ⚬ 𝑦 ) )
5	4	oveq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) )
6		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
7	5 6	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
8		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 ⚬ 𝑦 ) = ( 𝑋 ⚬ 𝑌 ) )
9	8	oveq1d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) )
10		oveq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ⚬ 𝑧 ) = ( 𝑌 ⚬ 𝑧 ) )
11	10	oveq2d	⊢ ( 𝑦 = 𝑌 → ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) )
12	9 11	eqeq12d	⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) ) )
13		oveq2	⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) )
14		oveq2	⊢ ( 𝑧 = 𝑍 → ( 𝑌 ⚬ 𝑧 ) = ( 𝑌 ⚬ 𝑍 ) )
15	14	oveq2d	⊢ ( 𝑧 = 𝑍 → ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) )
16	13 15	eqeq12d	⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) ↔ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) )
17	7 12 16	rspc3v	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) → ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) )
18	17	com12	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) )
19	3 18	simplbiim	⊢ ( 𝐺 ∈ Smgrp → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) )
20	19	imp	⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) )

Metamath Proof Explorer

Theorem sgrpass

Proof