Theorem 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={\mathrm{Base}}_G$$
	grpinvval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpinvval.o	$$⊢\underset{\dot{}}{0}=0_G$$
	grpinvval.n	$$⊢N={inv}_g\left(G\right)$$
Assertion	grpinvval	$$⊢X\in B\to N\left(X\right)=\left(\iota y\in B|y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$

Proof

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