grpoinvf

Description: Mapping of the inverse function of a group. (Contributed by NM, 29-Mar-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpasscan1.1	$⊢ X = ran G$
	grpasscan1.2	$⊢ N = inv (G)$
Assertion	grpoinvf	$⊢ G \in GrpOp \to N : X \underset{1-1 onto}{⟶} X$

Proof

Step	Hyp	Ref	Expression
1		grpasscan1.1	$⊢ X = ran G$
2		grpasscan1.2	$⊢ N = inv (G)$
3		riotaex	$⊢ (ι y \in X \| y G x = GId (G)) \in V$
4		eqid	$⊢ (x \in X ⟼ (ι y \in X \| y G x = GId (G))) = (x \in X ⟼ (ι y \in X \| y G x = GId (G)))$
5	3 4	fnmpti	$⊢ (x \in X ⟼ (ι y \in X \| y G x = GId (G))) Fn X$
6		eqid	$⊢ GId (G) = GId (G)$
7	1 6 2	grpoinvfval	$⊢ G \in GrpOp \to N = (x \in X ⟼ (ι y \in X \| y G x = GId (G)))$
8	7	fneq1d	$⊢ G \in GrpOp \to (N Fn X \leftrightarrow (x \in X ⟼ (ι y \in X \| y G x = GId (G))) Fn X)$
9	5 8	mpbiri	$⊢ G \in GrpOp \to N Fn X$
10		fnrnfv	$⊢ N Fn X \to ran N = \{y \| \exists x \in X y = N (x)\}$
11	9 10	syl	$⊢ G \in GrpOp \to ran N = \{y \| \exists x \in X y = N (x)\}$
12	1 2	grpoinvcl	$⊢ (G \in GrpOp \land y \in X) \to N (y) \in X$
13	1 2	grpo2inv	$⊢ (G \in GrpOp \land y \in X) \to N (N (y)) = y$
14	13	eqcomd	$⊢ (G \in GrpOp \land y \in X) \to y = N (N (y))$
15		fveq2	$⊢ x = N (y) \to N (x) = N (N (y))$
16	15	rspceeqv	$⊢ (N (y) \in X \land y = N (N (y))) \to \exists x \in X y = N (x)$
17	12 14 16	syl2anc	$⊢ (G \in GrpOp \land y \in X) \to \exists x \in X y = N (x)$
18	17	ex	$⊢ G \in GrpOp \to (y \in X \to \exists x \in X y = N (x))$
19		simpr	$⊢ ((G \in GrpOp \land x \in X) \land y = N (x)) \to y = N (x)$
20	1 2	grpoinvcl	$⊢ (G \in GrpOp \land x \in X) \to N (x) \in X$
21	20	adantr	$⊢ ((G \in GrpOp \land x \in X) \land y = N (x)) \to N (x) \in X$
22	19 21	eqeltrd	$⊢ ((G \in GrpOp \land x \in X) \land y = N (x)) \to y \in X$
23	22	rexlimdva2	$⊢ G \in GrpOp \to (\exists x \in X y = N (x) \to y \in X)$
24	18 23	impbid	$⊢ G \in GrpOp \to (y \in X \leftrightarrow \exists x \in X y = N (x))$
25	24	eqabdv	$⊢ G \in GrpOp \to X = \{y \| \exists x \in X y = N (x)\}$
26	11 25	eqtr4d	$⊢ G \in GrpOp \to ran N = X$
27		fveq2	$⊢ N (x) = N (y) \to N (N (x)) = N (N (y))$
28	1 2	grpo2inv	$⊢ (G \in GrpOp \land x \in X) \to N (N (x)) = x$
29	28 13	eqeqan12d	$⊢ ((G \in GrpOp \land x \in X) \land (G \in GrpOp \land y \in X)) \to (N (N (x)) = N (N (y)) \leftrightarrow x = y)$
30	29	anandis	$⊢ (G \in GrpOp \land (x \in X \land y \in X)) \to (N (N (x)) = N (N (y)) \leftrightarrow x = y)$
31	27 30	imbitrid	$⊢ (G \in GrpOp \land (x \in X \land y \in X)) \to (N (x) = N (y) \to x = y)$
32	31	ralrimivva	$⊢ G \in GrpOp \to \forall x \in X \forall y \in X (N (x) = N (y) \to x = y)$
33		dff1o6	$⊢ N : X \underset{1-1 onto}{⟶} X \leftrightarrow (N Fn X \land ran N = X \land \forall x \in X \forall y \in X (N (x) = N (y) \to x = y))$
34	9 26 32 33	syl3anbrc	$⊢ G \in GrpOp \to N : X \underset{1-1 onto}{⟶} X$

Metamath Proof Explorer

Theorem grpoinvf

Proof