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	$⊢ \underset{˙}{+} = +_{G}$
		grpidrcan.o	$⊢ \underset{˙}{0} = 0_{G}$
	Assertion	grpidlcan	$⊢ (G \in Grp \land X \in B \land Z \in B) \to (Z \underset{˙}{+} X = X \leftrightarrow Z = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		grpidrcan.b	$⊢ B = {Base}_{G}$
2		grpidrcan.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpidrcan.o	$⊢ \underset{˙}{0} = 0_{G}$
4	1 2 3	grplid	$⊢ (G \in Grp \land X \in B) \to \underset{˙}{0} \underset{˙}{+} X = X$
5	4	3adant3	$⊢ (G \in Grp \land X \in B \land Z \in B) \to \underset{˙}{0} \underset{˙}{+} X = X$
6	5	eqeq2d	$⊢ (G \in Grp \land X \in B \land Z \in B) \to (Z \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X \leftrightarrow Z \underset{˙}{+} X = X)$
7		simp1	$⊢ (G \in Grp \land X \in B \land Z \in B) \to G \in Grp$
8		simp3	$⊢ (G \in Grp \land X \in B \land Z \in B) \to Z \in B$
9	1 3	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in B$
10	9	3ad2ant1	$⊢ (G \in Grp \land X \in B \land Z \in B) \to \underset{˙}{0} \in B$
11		simp2	$⊢ (G \in Grp \land X \in B \land Z \in B) \to X \in B$
12	1 2	grprcan	$⊢ (G \in Grp \land (Z \in B \land \underset{˙}{0} \in B \land X \in B)) \to (Z \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X \leftrightarrow Z = \underset{˙}{0})$
13	7 8 10 11 12	syl13anc	$⊢ (G \in Grp \land X \in B \land Z \in B) \to (Z \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X \leftrightarrow Z = \underset{˙}{0})$
14	6 13	bitr3d	$⊢ (G \in Grp \land X \in B \land Z \in B) \to (Z \underset{˙}{+} X = X \leftrightarrow Z = \underset{˙}{0})$