Metamath Proof Explorer

Theorem grporid

Description: The identity element of a group is a right identity. (Contributed by NM, 24-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		grpoidval.1	$⊢ X = ran G$
2		grpoidval.2	$⊢ U = GId (G)$
3	1 2	grpoidinv2	$⊢ (G \in GrpOp \land A \in X) \to ((U G A = A \land A G U = A) \land \exists x \in X (x G A = U \land A G x = U))$
4		simplr	$⊢ ((U G A = A \land A G U = A) \land \exists x \in X (x G A = U \land A G x = U)) \to A G U = A$
5	3 4	syl	$⊢ (G \in GrpOp \land A \in X) \to A G U = A$