Theorem grpinvcnv

Description: The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	grpinvinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpinvinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion	grpinvcnv	⊢ ( 𝐺 ∈ Grp → ◡ 𝑁 = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		grpinvinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpinvinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
3		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑥 ) )
4	1 2	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑥 ) ∈ 𝐵 )
5	1 2	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑦 ) ∈ 𝐵 )
6		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
8	1 6 7 2	grpinvid1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑦 ) = 𝑥 ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
9	8	3com23	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑦 ) = 𝑥 ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
10	1 6 7 2	grpinvid2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑥 ) = 𝑦 ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
11	9 10	bitr4d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑦 ) = 𝑥 ↔ ( 𝑁 ‘ 𝑥 ) = 𝑦 ) )
12	11	3expb	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑁 ‘ 𝑦 ) = 𝑥 ↔ ( 𝑁 ‘ 𝑥 ) = 𝑦 ) )
13		eqcom	⊢ ( 𝑥 = ( 𝑁 ‘ 𝑦 ) ↔ ( 𝑁 ‘ 𝑦 ) = 𝑥 )
14		eqcom	⊢ ( 𝑦 = ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑁 ‘ 𝑥 ) = 𝑦 )
15	12 13 14	3bitr4g	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = ( 𝑁 ‘ 𝑦 ) ↔ 𝑦 = ( 𝑁 ‘ 𝑥 ) ) )
16	3 4 5 15	f1ocnv2d	⊢ ( 𝐺 ∈ Grp → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑥 ) ) : 𝐵 –1-1-onto→ 𝐵 ∧ ◡ ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑦 ) ) ) )
17	16	simprd	⊢ ( 𝐺 ∈ Grp → ◡ ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑦 ) ) )
18	1 2	grpinvf	⊢ ( 𝐺 ∈ Grp → 𝑁 : 𝐵 ⟶ 𝐵 )
19	18	feqmptd	⊢ ( 𝐺 ∈ Grp → 𝑁 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑥 ) ) )
20	19	cnveqd	⊢ ( 𝐺 ∈ Grp → ◡ 𝑁 = ◡ ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑥 ) ) )
21	18	feqmptd	⊢ ( 𝐺 ∈ Grp → 𝑁 = ( 𝑦 ∈ 𝐵 ↦ ( 𝑁 ‘ 𝑦 ) ) )
22	17 20 21	3eqtr4d	⊢ ( 𝐺 ∈ Grp → ◡ 𝑁 = 𝑁 )