Metamath Proof Explorer

Theorem grpoid

Description: Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	grpoinveu.1	$⊢ X = ran G$
		grpoinveu.2	$⊢ U = GId (G)$
	Assertion	grpoid	$⊢ (G \in GrpOp \land A \in X) \to (A = U \leftrightarrow A G A = A)$

Proof

Step	Hyp	Ref	Expression
1		grpoinveu.1	$⊢ X = ran G$
2		grpoinveu.2	$⊢ U = GId (G)$
3	1 2	grpoidcl	$⊢ G \in GrpOp \to U \in X$
4	1	grporcan	$⊢ (G \in GrpOp \land (A \in X \land U \in X \land A \in X)) \to (A G A = U G A \leftrightarrow A = U)$
5	4	3exp2	$⊢ G \in GrpOp \to (A \in X \to (U \in X \to (A \in X \to (A G A = U G A \leftrightarrow A = U))))$
6	3 5	mpid	$⊢ G \in GrpOp \to (A \in X \to (A \in X \to (A G A = U G A \leftrightarrow A = U)))$
7	6	pm2.43d	$⊢ G \in GrpOp \to (A \in X \to (A G A = U G A \leftrightarrow A = U))$
8	7	imp	$⊢ (G \in GrpOp \land A \in X) \to (A G A = U G A \leftrightarrow A = U)$
9	1 2	grpolid	$⊢ (G \in GrpOp \land A \in X) \to U G A = A$
10	9	eqeq2d	$⊢ (G \in GrpOp \land A \in X) \to (A G A = U G A \leftrightarrow A G A = A)$
11	8 10	bitr3d	$⊢ (G \in GrpOp \land A \in X) \to (A = U \leftrightarrow A G A = A)$