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

Metamath Proof Explorer

Theorem ablpncan3

Description: A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015)

Ref Expression
Hypotheses ablsubadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablsubadd.p ⊢ + = ( +g ‘ 𝐺 )
ablsubadd.m ⊢ − = ( -g ‘ 𝐺 )
Assertion ablpncan3 ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 + ( 𝑌 − 𝑋 ) ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 ablsubadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablsubadd.p ⊢ + = ( +g ‘ 𝐺 )
3 ablsubadd.m ⊢ − = ( -g ‘ 𝐺 )
4 simpl ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐺 ∈ Abel )
5 simprl ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
6 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
7 6 adantr ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
8 simprr ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
9 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 − 𝑋 ) ∈ 𝐵 )
10 7 8 5 9 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑌 − 𝑋 ) ∈ 𝐵 )
11 1 2 ablcom ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 − 𝑋 ) ∈ 𝐵 ) → ( 𝑋 + ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) + 𝑋 ) )
12 4 5 10 11 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 + ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) + 𝑋 ) )
13 1 2 3 grpnpcan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑌 − 𝑋 ) + 𝑋 ) = 𝑌 )
14 7 8 5 13 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑌 − 𝑋 ) + 𝑋 ) = 𝑌 )
15 12 14 eqtrd ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 + ( 𝑌 − 𝑋 ) ) = 𝑌 )