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

Metamath Proof Explorer

Theorem grpid

Description: Two ways of saying that an element of a group is the identity element. Provides a convenient way to compute the value of the identity element. (Contributed by NM, 24-Aug-2011)

		Ref	Expression
	Hypotheses	grpinveu.b	$⊢ B = {Base}_{G}$
		grpinveu.p	$⊢ \underset{˙}{+} = +_{G}$
		grpinveu.o	$⊢ \underset{˙}{0} = 0_{G}$
	Assertion	grpid	$⊢ (G \in Grp \land X \in B) \to (X \underset{˙}{+} X = X \leftrightarrow \underset{˙}{0} = X)$

Proof

Step	Hyp	Ref	Expression
1		grpinveu.b	$⊢ B = {Base}_{G}$
2		grpinveu.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpinveu.o	$⊢ \underset{˙}{0} = 0_{G}$
4		eqcom	$⊢ \underset{˙}{0} = X \leftrightarrow X = \underset{˙}{0}$
5	1 3	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in B$
6	1 2	grprcan	$⊢ (G \in Grp \land (X \in B \land \underset{˙}{0} \in B \land X \in B)) \to (X \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X \leftrightarrow X = \underset{˙}{0})$
7	6	3exp2	$⊢ G \in Grp \to (X \in B \to (\underset{˙}{0} \in B \to (X \in B \to (X \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X \leftrightarrow X = \underset{˙}{0}))))$
8	5 7	mpid	$⊢ G \in Grp \to (X \in B \to (X \in B \to (X \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X \leftrightarrow X = \underset{˙}{0})))$
9	8	pm2.43d	$⊢ G \in Grp \to (X \in B \to (X \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X \leftrightarrow X = \underset{˙}{0}))$
10	9	imp	$⊢ (G \in Grp \land X \in B) \to (X \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X \leftrightarrow X = \underset{˙}{0})$
11	1 2 3	grplid	$⊢ (G \in Grp \land X \in B) \to \underset{˙}{0} \underset{˙}{+} X = X$
12	11	eqeq2d	$⊢ (G \in Grp \land X \in B) \to (X \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X \leftrightarrow X \underset{˙}{+} X = X)$
13	10 12	bitr3d	$⊢ (G \in Grp \land X \in B) \to (X = \underset{˙}{0} \leftrightarrow X \underset{˙}{+} X = X)$
14	4 13	bitr2id	$⊢ (G \in Grp \land X \in B) \to (X \underset{˙}{+} X = X \leftrightarrow \underset{˙}{0} = X)$