Metamath Proof Explorer


Theorem grpsubeq0

Description: If the difference between two group elements is zero, they are equal. ( subeq0 analog.) (Contributed 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𝑋 = 𝑌 ) )