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

Metamath Proof Explorer

Theorem grpolid

Description: The identity element of a group is a left 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	grpolid	$⊢ (G \in GrpOp \land A \in X) \to U G A = 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 y \in X (y G A = U \land A G y = U))$
4	3	simplld	$⊢ (G \in GrpOp \land A \in X) \to U G A = A$