grpoinv

Description: The properties of a group element's inverse. (Contributed by NM, 27-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpinv.1	$⊢ X = ran G$
	grpinv.2	$⊢ U = GId (G)$
	grpinv.3	$⊢ N = inv (G)$
Assertion	grpoinv	$⊢ (G \in GrpOp \land A \in X) \to (N (A) G A = U \land A G N (A) = U)$

Proof

Step	Hyp	Ref	Expression
1		grpinv.1	$⊢ X = ran G$
2		grpinv.2	$⊢ U = GId (G)$
3		grpinv.3	$⊢ N = inv (G)$
4	1 2 3	grpoinvval	$⊢ (G \in GrpOp \land A \in X) \to N (A) = (ι y \in X \| y G A = U)$
5	1 2	grpoinveu	$⊢ (G \in GrpOp \land A \in X) \to \exists! y \in X y G A = U$
6		riotacl2	$⊢ \exists! y \in X y G A = U \to (ι y \in X \| y G A = U) \in \{y \in X \| y G A = U\}$
7	5 6	syl	$⊢ (G \in GrpOp \land A \in X) \to (ι y \in X \| y G A = U) \in \{y \in X \| y G A = U\}$
8	4 7	eqeltrd	$⊢ (G \in GrpOp \land A \in X) \to N (A) \in \{y \in X \| y G A = U\}$
9		simpl	$⊢ (y G A = U \land A G y = U) \to y G A = U$
10	9	rgenw	$⊢ \forall y \in X ((y G A = U \land A G y = U) \to y G A = U)$
11	10	a1i	$⊢ (G \in GrpOp \land A \in X) \to \forall y \in X ((y G A = U \land A G y = U) \to y G A = U)$
12	1 2	grpoidinv2	$⊢ (G \in GrpOp \land A \in X) \to ((U G A = A \land A G U = A) \land \exists y \in X (y G A = U \land A G y = U))$
13	12	simprd	$⊢ (G \in GrpOp \land A \in X) \to \exists y \in X (y G A = U \land A G y = U)$
14	11 13 5	3jca	$⊢ (G \in GrpOp \land A \in X) \to (\forall y \in X ((y G A = U \land A G y = U) \to y G A = U) \land \exists y \in X (y G A = U \land A G y = U) \land \exists! y \in X y G A = U)$
15		reupick2	$⊢ ((\forall y \in X ((y G A = U \land A G y = U) \to y G A = U) \land \exists y \in X (y G A = U \land A G y = U) \land \exists! y \in X y G A = U) \land y \in X) \to (y G A = U \leftrightarrow (y G A = U \land A G y = U))$
16	14 15	sylan	$⊢ ((G \in GrpOp \land A \in X) \land y \in X) \to (y G A = U \leftrightarrow (y G A = U \land A G y = U))$
17	16	rabbidva	$⊢ (G \in GrpOp \land A \in X) \to \{y \in X \| y G A = U\} = \{y \in X \| (y G A = U \land A G y = U)\}$
18	8 17	eleqtrd	$⊢ (G \in GrpOp \land A \in X) \to N (A) \in \{y \in X \| (y G A = U \land A G y = U)\}$
19		oveq1	$⊢ y = N (A) \to y G A = N (A) G A$
20	19	eqeq1d	$⊢ y = N (A) \to (y G A = U \leftrightarrow N (A) G A = U)$
21		oveq2	$⊢ y = N (A) \to A G y = A G N (A)$
22	21	eqeq1d	$⊢ y = N (A) \to (A G y = U \leftrightarrow A G N (A) = U)$
23	20 22	anbi12d	$⊢ y = N (A) \to ((y G A = U \land A G y = U) \leftrightarrow (N (A) G A = U \land A G N (A) = U))$
24	23	elrab	$⊢ N (A) \in \{y \in X \| (y G A = U \land A G y = U)\} \leftrightarrow (N (A) \in X \land (N (A) G A = U \land A G N (A) = U))$
25	18 24	sylib	$⊢ (G \in GrpOp \land A \in X) \to (N (A) \in X \land (N (A) G A = U \land A G N (A) = U))$
26	25	simprd	$⊢ (G \in GrpOp \land A \in X) \to (N (A) G A = U \land A G N (A) = U)$

Metamath Proof Explorer

Theorem grpoinv

Proof