Metamath Proof Explorer

Theorem ablpncan3

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

Ref Expression
Hypotheses ablsubadd.b ⊢ B = Base G
ablsubadd.p ⊢ + ˙ = + G
ablsubadd.m ⊢ - ˙ = - G
Assertion ablpncan3 ⊢ G ∈ Abel ∧ X ∈ B ∧ Y ∈ B → X + ˙ Y - ˙ X = Y

Proof

Step Hyp Ref Expression
1 ablsubadd.b ⊢ B = Base G
2 ablsubadd.p ⊢ + ˙ = + G
3 ablsubadd.m ⊢ - ˙ = - G
4 simpl ⊢ G ∈ Abel ∧ X ∈ B ∧ Y ∈ B → G ∈ Abel
5 simprl ⊢ G ∈ Abel ∧ X ∈ B ∧ Y ∈ B → X ∈ B
6 ablgrp ⊢ G ∈ Abel → G ∈ Grp
7 6 adantr ⊢ G ∈ Abel ∧ X ∈ B ∧ Y ∈ B → G ∈ Grp
8 simprr ⊢ G ∈ Abel ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
9 1 3 grpsubcl ⊢ G ∈ Grp ∧ Y ∈ B ∧ X ∈ B → Y - ˙ X ∈ B
10 7 8 5 9 syl3anc ⊢ G ∈ Abel ∧ X ∈ B ∧ Y ∈ B → Y - ˙ X ∈ B
11 1 2 ablcom ⊢ G ∈ Abel ∧ X ∈ B ∧ Y - ˙ X ∈ B → X + ˙ Y - ˙ X = Y - ˙ X + ˙ X
12 4 5 10 11 syl3anc ⊢ G ∈ Abel ∧ X ∈ B ∧ Y ∈ B → X + ˙ Y - ˙ X = Y - ˙ X + ˙ X
13 1 2 3 grpnpcan ⊢ G ∈ Grp ∧ Y ∈ B ∧ X ∈ B → Y - ˙ X + ˙ X = Y
14 7 8 5 13 syl3anc ⊢ G ∈ Abel ∧ X ∈ B ∧ Y ∈ B → Y - ˙ X + ˙ X = Y
15 12 14 eqtrd ⊢ G ∈ Abel ∧ X ∈ B ∧ Y ∈ B → X + ˙ Y - ˙ X = Y