Metamath Proof Explorer

Theorem grpoinvcl

Description: A group element's inverse is a group element. (Contributed by NM, 27-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	grpinvcl.1	$⊢ X = ran G$
		grpinvcl.2	$⊢ N = inv (G)$
	Assertion	grpoinvcl	$⊢ (G \in GrpOp \land A \in X) \to N (A) \in X$

Proof

Step	Hyp	Ref	Expression
1		grpinvcl.1	$⊢ X = ran G$
2		grpinvcl.2	$⊢ N = inv (G)$
3		eqid	$⊢ GId (G) = GId (G)$
4	1 3 2	grpoinvval	$⊢ (G \in GrpOp \land A \in X) \to N (A) = (ι y \in X \| y G A = GId (G))$
5	1 3	grpoinveu	$⊢ (G \in GrpOp \land A \in X) \to \exists! y \in X y G A = GId (G)$
6		riotacl	$⊢ \exists! y \in X y G A = GId (G) \to (ι y \in X \| y G A = GId (G)) \in X$
7	5 6	syl	$⊢ (G \in GrpOp \land A \in X) \to (ι y \in X \| y G A = GId (G)) \in X$
8	4 7	eqeltrd	$⊢ (G \in GrpOp \land A \in X) \to N (A) \in X$