Metamath Proof Explorer


Theorem grpidlcan

Description: If left adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019)

Ref Expression
Hypotheses grpidrcan.b 𝐵 = ( Base ‘ 𝐺 )
grpidrcan.p + = ( +g𝐺 )
grpidrcan.o 0 = ( 0g𝐺 )
Assertion grpidlcan ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑍𝐵 ) → ( ( 𝑍 + 𝑋 ) = 𝑋𝑍 = 0 ) )

Proof

Step Hyp Ref Expression
1 grpidrcan.b 𝐵 = ( Base ‘ 𝐺 )
2 grpidrcan.p + = ( +g𝐺 )
3 grpidrcan.o 0 = ( 0g𝐺 )
4 1 2 3 grplid ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
5 4 3adant3 ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑍𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
6 5 eqeq2d ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑍𝐵 ) → ( ( 𝑍 + 𝑋 ) = ( 0 + 𝑋 ) ↔ ( 𝑍 + 𝑋 ) = 𝑋 ) )
7 simp1 ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑍𝐵 ) → 𝐺 ∈ Grp )
8 simp3 ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑍𝐵 ) → 𝑍𝐵 )
9 1 3 grpidcl ( 𝐺 ∈ Grp → 0𝐵 )
10 9 3ad2ant1 ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑍𝐵 ) → 0𝐵 )
11 simp2 ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑍𝐵 ) → 𝑋𝐵 )
12 1 2 grprcan ( ( 𝐺 ∈ Grp ∧ ( 𝑍𝐵0𝐵𝑋𝐵 ) ) → ( ( 𝑍 + 𝑋 ) = ( 0 + 𝑋 ) ↔ 𝑍 = 0 ) )
13 7 8 10 11 12 syl13anc ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑍𝐵 ) → ( ( 𝑍 + 𝑋 ) = ( 0 + 𝑋 ) ↔ 𝑍 = 0 ) )
14 6 13 bitr3d ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑍𝐵 ) → ( ( 𝑍 + 𝑋 ) = 𝑋𝑍 = 0 ) )