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. ) )