Theorem grpinvinvd

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

	Ref	Expression
Hypotheses	grpinvinvd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpinvinvd.2	⊢ 𝑁 = ( invg ‘ 𝐺 )
	grpinvinvd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	grpinvinvd.4	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	grpinvinvd	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		grpinvinvd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpinvinvd.2	⊢ 𝑁 = ( invg ‘ 𝐺 )
3		grpinvinvd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		grpinvinvd.4	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5	1 2	grpinvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
6	3 4 5	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )