Theorem grpsubrcan

Description: Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014)

	Ref	Expression
Hypotheses	grpsubcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpsubcl.m	⊢ − = ( -g ‘ 𝐺 )
Assertion	grpsubrcan	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 − 𝑍 ) = ( 𝑌 − 𝑍 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		grpsubcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpsubcl.m	⊢ − = ( -g ‘ 𝐺 )
3		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
5	1 3 4 2	grpsubval	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 − 𝑍 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
6	5	3adant2	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 − 𝑍 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
7	1 3 4 2	grpsubval	⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 − 𝑍 ) = ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
8	7	3adant1	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 − 𝑍 ) = ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) )
9	6 8	eqeq12d	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 − 𝑍 ) = ( 𝑌 − 𝑍 ) ↔ ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ) )
10	9	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 − 𝑍 ) = ( 𝑌 − 𝑍 ) ↔ ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ) )
11		simpl	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
12		simpr1	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
13		simpr2	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
14	1 4	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
15	14	3ad2antr3	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
16	1 3	grprcan	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ) ) → ( ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ↔ 𝑋 = 𝑌 ) )
17	11 12 13 15 16	syl13anc	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) = ( 𝑌 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ) ↔ 𝑋 = 𝑌 ) )
18	10 17	bitrd	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 − 𝑍 ) = ( 𝑌 − 𝑍 ) ↔ 𝑋 = 𝑌 ) )