Metamath Proof Explorer

Theorem grpoinvval

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

		Ref	Expression
	Hypotheses	grpinvfval.1	$⊢ X = ran G$
		grpinvfval.2	$⊢ U = GId (G)$
		grpinvfval.3	$⊢ N = inv (G)$
	Assertion	grpoinvval	$⊢ (G \in GrpOp \land A \in X) \to N (A) = (ι y \in X \| y G A = U)$

Proof

Step	Hyp	Ref	Expression
1		grpinvfval.1	$⊢ X = ran G$
2		grpinvfval.2	$⊢ U = GId (G)$
3		grpinvfval.3	$⊢ N = inv (G)$
4	1 2 3	grpoinvfval	$⊢ G \in GrpOp \to N = (x \in X ⟼ (ι y \in X \| y G x = U))$
5	4	fveq1d	$⊢ G \in GrpOp \to N (A) = (x \in X ⟼ (ι y \in X \| y G x = U)) (A)$
6		oveq2	$⊢ x = A \to y G x = y G A$
7	6	eqeq1d	$⊢ x = A \to (y G x = U \leftrightarrow y G A = U)$
8	7	riotabidv	$⊢ x = A \to (ι y \in X \| y G x = U) = (ι y \in X \| y G A = U)$
9		eqid	$⊢ (x \in X ⟼ (ι y \in X \| y G x = U)) = (x \in X ⟼ (ι y \in X \| y G x = U))$
10		riotaex	$⊢ (ι y \in X \| y G A = U) \in V$
11	8 9 10	fvmpt	$⊢ A \in X \to (x \in X ⟼ (ι y \in X \| y G x = U)) (A) = (ι y \in X \| y G A = U)$
12	5 11	sylan9eq	$⊢ (G \in GrpOp \land A \in X) \to N (A) = (ι y \in X \| y G A = U)$