grpinvval

Description: The inverse of a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 7-Aug-2013)

	Ref	Expression
Hypotheses	grpinvval.b	$⊢ B = {Base}_{G}$
	grpinvval.p	$⊢ \underset{˙}{+} = +_{G}$
	grpinvval.o	$⊢ \underset{˙}{0} = 0_{G}$
	grpinvval.n	$⊢ N = {inv}_{g} (G)$
Assertion	grpinvval	$⊢ X \in B \to N (X) = (ι y \in B \| y \underset{˙}{+} X = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		grpinvval.b	$⊢ B = {Base}_{G}$
2		grpinvval.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpinvval.o	$⊢ \underset{˙}{0} = 0_{G}$
4		grpinvval.n	$⊢ N = {inv}_{g} (G)$
5		oveq2	$⊢ x = X \to y \underset{˙}{+} x = y \underset{˙}{+} X$
6	5	eqeq1d	$⊢ x = X \to (y \underset{˙}{+} x = \underset{˙}{0} \leftrightarrow y \underset{˙}{+} X = \underset{˙}{0})$
7	6	riotabidv	$⊢ x = X \to (ι y \in B \| y \underset{˙}{+} x = \underset{˙}{0}) = (ι y \in B \| y \underset{˙}{+} X = \underset{˙}{0})$
8	1 2 3 4	grpinvfval	$⊢ N = (x \in B ⟼ (ι y \in B \| y \underset{˙}{+} x = \underset{˙}{0}))$
9		riotaex	$⊢ (ι y \in B \| y \underset{˙}{+} X = \underset{˙}{0}) \in V$
10	7 8 9	fvmpt	$⊢ X \in B \to N (X) = (ι y \in B \| y \underset{˙}{+} X = \underset{˙}{0})$

Metamath Proof Explorer