Theorem grpinv11

Description: The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015)

	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	6	adantl	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) )
8	1 2	grpinvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
9	3 4 8	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
10	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
11	1 2	grpinvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) = 𝑌 )
12	3 5 11	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) = 𝑌 )
13	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑌 ) ) = 𝑌 )
14	7 10 13	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) ) → 𝑋 = 𝑌 )
15	14	ex	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
16		fveq2	⊢ ( 𝑋 = 𝑌 → ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) )
17	15 16	impbid1	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )