Metamath Proof Explorer

Theorem 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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) )