This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- B = ( Base ` G )
grpidrcan.p 
|- .+ = ( +g ` G )
grpidrcan.o 
|- .0. = ( 0g ` G )
Assertion grpidlcan 
|- ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( ( Z .+ X ) = X <-> Z = .0. ) )

Proof

Step Hyp Ref Expression
1 grpidrcan.b 
 |-  B = ( Base ` G )
2 grpidrcan.p 
 |-  .+ = ( +g ` G )
3 grpidrcan.o 
 |-  .0. = ( 0g ` G )
4 1 2 3 grplid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( .0. .+ X ) = X )
5 4 3adant3 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( .0. .+ X ) = X )
6 5 eqeq2d 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( ( Z .+ X ) = ( .0. .+ X ) <-> ( Z .+ X ) = X ) )
7 simp1 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> G e. Grp )
8 simp3 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> Z e. B )
9 1 3 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
10 9 3ad2ant1 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> .0. e. B )
11 simp2 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> X e. B )
12 1 2 grprcan 
 |-  ( ( G e. Grp /\ ( Z e. B /\ .0. e. B /\ X e. B ) ) -> ( ( Z .+ X ) = ( .0. .+ X ) <-> Z = .0. ) )
13 7 8 10 11 12 syl13anc 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( ( Z .+ X ) = ( .0. .+ X ) <-> Z = .0. ) )
14 6 13 bitr3d 
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( ( Z .+ X ) = X <-> Z = .0. ) )