grpinvcnv

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

	Ref	Expression
Hypotheses	grpinvinv.b	$⊢ B = {Base}_{G}$
	grpinvinv.n	$⊢ N = {inv}_{g} (G)$
Assertion	grpinvcnv	$⊢ G \in Grp \to N^{-1} = N$

Proof

Step	Hyp	Ref	Expression
1		grpinvinv.b	$⊢ B = {Base}_{G}$
2		grpinvinv.n	$⊢ N = {inv}_{g} (G)$
3		eqid	$⊢ (x \in B ⟼ N (x)) = (x \in B ⟼ N (x))$
4	1 2	grpinvcl	$⊢ (G \in Grp \land x \in B) \to N (x) \in B$
5	1 2	grpinvcl	$⊢ (G \in Grp \land y \in B) \to N (y) \in B$
6		eqid	$⊢ +_{G} = +_{G}$
7		eqid	$⊢ 0_{G} = 0_{G}$
8	1 6 7 2	grpinvid1	$⊢ (G \in Grp \land y \in B \land x \in B) \to (N (y) = x \leftrightarrow y +_{G} x = 0_{G})$
9	8	3com23	$⊢ (G \in Grp \land x \in B \land y \in B) \to (N (y) = x \leftrightarrow y +_{G} x = 0_{G})$
10	1 6 7 2	grpinvid2	$⊢ (G \in Grp \land x \in B \land y \in B) \to (N (x) = y \leftrightarrow y +_{G} x = 0_{G})$
11	9 10	bitr4d	$⊢ (G \in Grp \land x \in B \land y \in B) \to (N (y) = x \leftrightarrow N (x) = y)$
12	11	3expb	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to (N (y) = x \leftrightarrow N (x) = y)$
13		eqcom	$⊢ x = N (y) \leftrightarrow N (y) = x$
14		eqcom	$⊢ y = N (x) \leftrightarrow N (x) = y$
15	12 13 14	3bitr4g	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to (x = N (y) \leftrightarrow y = N (x))$
16	3 4 5 15	f1ocnv2d	$⊢ G \in Grp \to ((x \in B ⟼ N (x)) : B \underset{1-1 onto}{⟶} B \land {(x \in B ⟼ N (x))}^{-1} = (y \in B ⟼ N (y)))$
17	16	simprd	$⊢ G \in Grp \to {(x \in B ⟼ N (x))}^{-1} = (y \in B ⟼ N (y))$
18	1 2	grpinvf	$⊢ G \in Grp \to N : B ⟶ B$
19	18	feqmptd	$⊢ G \in Grp \to N = (x \in B ⟼ N (x))$
20	19	cnveqd	$⊢ G \in Grp \to N^{-1} = {(x \in B ⟼ N (x))}^{-1}$
21	18	feqmptd	$⊢ G \in Grp \to N = (y \in B ⟼ N (y))$
22	17 20 21	3eqtr4d	$⊢ G \in Grp \to N^{-1} = N$

Metamath Proof Explorer

Theorem grpinvcnv

Proof