Theorem grpinvfval

Description: The inverse function of a group. For a shorter proof using ax-rep , see grpinvfvalALT . (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 7-Aug-2013) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 13-Aug-2023)

	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	grpinvfval	$$⊢N=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\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		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
6	5 1	eqtr4di	$$⊢g=G\to {\mathrm{Base}}_g=B$$
7		fveq2	$$⊢g=G\to {+}_g={+}_G$$
8	7 2	eqtr4di	$$⊢g=G\to {+}_g=\underset{\dot{}}{+}$$
9	8	oveqd	$$⊢g=G\to y{+}_{g}x=y\underset{\dot{}}{+}x$$
10		fveq2	$$⊢g=G\to 0_g=0_G$$
11	10 3	eqtr4di	$$⊢g=G\to 0_g=\underset{\dot{}}{0}$$
12	9 11	eqeq12d	$$⊢g=G\to \left(y{+}_{g}x=0_g\leftrightarrow y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
13	6 12	riotaeqbidv	$$⊢g=G\to \left(\iota y\in {\mathrm{Base}}_g|y{+}_{g}x=0_g\right)=\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
14	6 13	mpteq12dv	$$⊢g=G\to \left(x\in {\mathrm{Base}}_g⟼\left(\iota y\in {\mathrm{Base}}_g|y{+}_{g}x=0_g\right)\right)=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
15		df-minusg	$$⊢{inv}_g=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼\left(\iota y\in {\mathrm{Base}}_g|y{+}_{g}x=0_g\right)\right)\right)$$
16	1	fvexi	$$⊢B\in \mathrm{V}$$
17		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
18	17 16	unex	$$⊢\left\{\varnothing \right\}\cup B\in \mathrm{V}$$
19		ssun2	$$⊢B\subseteq \left\{\varnothing \right\}\cup B$$
20		riotacl	$$⊢\exists !y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}\to \left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\in B$$
21	19 20	sseldi	$$⊢\exists !y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}\to \left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\in \left(\left\{\varnothing \right\}\cup B\right)$$
22		ssun1	$$⊢\left\{\varnothing \right\}\subseteq \left\{\varnothing \right\}\cup B$$
23		riotaund	$$⊢\neg \exists !y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}\to \left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)=\varnothing$$
24		riotaex	$$⊢\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\in \mathrm{V}$$
25	24	elsn	$$⊢\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\in \left\{\varnothing \right\}\leftrightarrow \left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)=\varnothing$$
26	23 25	sylibr	$$⊢\neg \exists !y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}\to \left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\in \left\{\varnothing \right\}$$
27	22 26	sseldi	$$⊢\neg \exists !y\in By\underset{\dot{}}{+}x=\underset{\dot{}}{0}\to \left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\in \left(\left\{\varnothing \right\}\cup B\right)$$
28	21 27	pm2.61i	$$⊢\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\in \left(\left\{\varnothing \right\}\cup B\right)$$
29	28	rgenw	$$⊢\forall x\in B\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\in \left(\left\{\varnothing \right\}\cup B\right)$$
30	16 18 29	mptexw	$$⊢\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
31	14 15 30	fvmpt	$$⊢G\in \mathrm{V}\to {inv}_g\left(G\right)=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
32		fvprc	$$⊢\neg G\in \mathrm{V}\to {inv}_g\left(G\right)=\varnothing$$
33		mpt0	$$⊢\left(x\in \varnothing ⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)=\varnothing$$
34	32 33	eqtr4di	$$⊢\neg G\in \mathrm{V}\to {inv}_g\left(G\right)=\left(x\in \varnothing ⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
35		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
36	1 35	syl5eq	$$⊢\neg G\in \mathrm{V}\to B=\varnothing$$
37	36	mpteq1d	$$⊢\neg G\in \mathrm{V}\to \left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)=\left(x\in \varnothing ⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
38	34 37	eqtr4d	$$⊢\neg G\in \mathrm{V}\to {inv}_g\left(G\right)=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
39	31 38	pm2.61i	$$⊢{inv}_g\left(G\right)=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
40	4 39	eqtri	$$⊢N=\left(x\in B⟼\left(\iota y\in B|y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$