Metamath Proof Explorer

Theorem grpassd

Description: A group operation is associative. (Contributed by SN, 29-Jan-2025)

Ref Expression
Hypotheses grpassd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
grpassd.p ⊢ + = ( +g ‘ 𝐺 )
grpassd.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
grpassd.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
grpassd.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
grpassd.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion grpassd ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 grpassd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpassd.p ⊢ + = ( +g ‘ 𝐺 )
3 grpassd.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
4 grpassd.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 grpassd.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 grpassd.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )
8 3 4 5 6 7 syl13anc ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )