Theorem grpinvinvd

Description: Double inverse law for groups. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	grpinvinvd.1	$$⊢B={\mathrm{Base}}_G$$
	grpinvinvd.2	$$⊢N={inv}_g\left(G\right)$$
	grpinvinvd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
	grpinvinvd.4	$$⊢\phi \to X\in B$$
Assertion	grpinvinvd	$$⊢\phi \to N\left(N\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		grpinvinvd.1	$$⊢B={\mathrm{Base}}_G$$
2		grpinvinvd.2	$$⊢N={inv}_g\left(G\right)$$
3		grpinvinvd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
4		grpinvinvd.4	$$⊢\phi \to X\in B$$
5	1 2	grpinvinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(N\left(X\right)\right)=X$$
6	3 4 5	syl2anc	$$⊢\phi \to N\left(N\left(X\right)\right)=X$$