Theorem grpsubeq0

Description: If the difference between two group elements is zero, they are equal. ( subeq0 analog.) (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by NM, 31-Mar-2014)

	Ref	Expression
Hypotheses	grpsubid.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpsubid.o	⊢ 0 = ( 0g ‘ 𝐺 )
	grpsubid.m	⊢ − = ( -g ‘ 𝐺 )
Assertion	grpsubeq0	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 − 𝑌 ) = 0 ↔ 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		grpsubid.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpsubid.o	⊢ 0 = ( 0g ‘ 𝐺 )
3		grpsubid.m	⊢ − = ( -g ‘ 𝐺 )
4		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
6	1 4 5 3	grpsubval	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
7	6	3adant1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
8	7	eqeq1d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 − 𝑌 ) = 0 ↔ ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = 0 ) )
9		simp1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐺 ∈ Grp )
10	1 5	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝐵 )
11	10	3adant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝐵 )
12		simp2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
13	1 4 2 5	grpinvid2	⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = 𝑋 ↔ ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = 0 ) )
14	9 11 12 13	syl3anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = 𝑋 ↔ ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = 0 ) )
15	1 5	grpinvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = 𝑌 )
16	15	3adant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = 𝑌 )
17	16	eqeq1d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = 𝑋 ↔ 𝑌 = 𝑋 ) )
18		eqcom	⊢ ( 𝑌 = 𝑋 ↔ 𝑋 = 𝑌 )
19	17 18	bitrdi	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = 𝑋 ↔ 𝑋 = 𝑌 ) )
20	8 14 19	3bitr2d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 − 𝑌 ) = 0 ↔ 𝑋 = 𝑌 ) )