This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abl32

Description: Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015) (Revised by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses ablcom.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablcom.p ⊢ + = ( +g ‘ 𝐺 )
abl32.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
abl32.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
abl32.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
abl32.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion abl32 ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 + 𝑍 ) + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ablcom.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablcom.p ⊢ + = ( +g ‘ 𝐺 )
3 abl32.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
4 abl32.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 abl32.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 abl32.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7 ablcmn ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
8 3 7 syl ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
9 1 2 cmn32 ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 + 𝑍 ) + 𝑌 ) )
10 8 4 5 6 9 syl13anc ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 + 𝑍 ) + 𝑌 ) )