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 ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )