Theorem grpinvfvi

Description: The group inverse function is compatible with identity-function protection. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypothesis	grpinvfvi.t	$$⊢N={inv}_g\left(G\right)$$
Assertion	grpinvfvi	$$⊢N={inv}_g\left(\mathrm{I}\left(G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpinvfvi.t	$$⊢N={inv}_g\left(G\right)$$
2		fvi	$$⊢G\in \mathrm{V}\to \mathrm{I}\left(G\right)=G$$
3	2	fveq2d	$$⊢G\in \mathrm{V}\to {inv}_g\left(\mathrm{I}\left(G\right)\right)={inv}_g\left(G\right)$$
4		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
5		eqid	$$⊢{inv}_g\left(\varnothing \right)={inv}_g\left(\varnothing \right)$$
6	4 5	grpinvfn	$$⊢{inv}_g\left(\varnothing \right)Fn\varnothing$$
7		fn0	$$⊢{inv}_g\left(\varnothing \right)Fn\varnothing \leftrightarrow {inv}_g\left(\varnothing \right)=\varnothing$$
8	6 7	mpbi	$$⊢{inv}_g\left(\varnothing \right)=\varnothing$$
9		fvprc	$$⊢\neg G\in \mathrm{V}\to \mathrm{I}\left(G\right)=\varnothing$$
10	9	fveq2d	$$⊢\neg G\in \mathrm{V}\to {inv}_g\left(\mathrm{I}\left(G\right)\right)={inv}_g\left(\varnothing \right)$$
11		fvprc	$$⊢\neg G\in \mathrm{V}\to {inv}_g\left(G\right)=\varnothing$$
12	8 10 11	3eqtr4a	$$⊢\neg G\in \mathrm{V}\to {inv}_g\left(\mathrm{I}\left(G\right)\right)={inv}_g\left(G\right)$$
13	3 12	pm2.61i	$$⊢{inv}_g\left(\mathrm{I}\left(G\right)\right)={inv}_g\left(G\right)$$
14	1 13	eqtr4i	$$⊢N={inv}_g\left(\mathrm{I}\left(G\right)\right)$$