Theorem grpinv11

Description: The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015) (Proof shortened by SN, 8-Jul-2025)

	Ref	Expression
Hypotheses	grpinvinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpinvinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
	grpinv11.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	grpinv11.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	grpinv11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	grpinv11	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		grpinvinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpinvinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
3		grpinv11.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		grpinv11.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		grpinv11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		fveq2	⊢ ( ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) )
7	1 2	grpinvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
8	3 4 7	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
9	1 2	grpinvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) = 𝑌 )
10	3 5 9	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) = 𝑌 )
11	8 10	eqeq12d	⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) ↔ 𝑋 = 𝑌 ) )
12	6 11	imbitrid	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
13		fveq2	⊢ ( 𝑋 = 𝑌 → ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) )
14	12 13	impbid1	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )