grpoidinv2

Description: A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpoidval.1	$⊢ X = ran G$
	grpoidval.2	$⊢ U = GId (G)$
Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		grpoidval.1	$⊢ X = ran G$
2		grpoidval.2	$⊢ U = GId (G)$
3	1 2	grpoidval	$⊢ G \in GrpOp \to U = (ι u \in X \| \forall x \in X u G x = x)$
4	1	grpoideu	$⊢ G \in GrpOp \to \exists! u \in X \forall x \in X u G x = x$
5		riotacl2	$⊢ \exists! u \in X \forall x \in X u G x = x \to (ι u \in X \| \forall x \in X u G x = x) \in \{u \in X \| \forall x \in X u G x = x\}$
6	4 5	syl	$⊢ G \in GrpOp \to (ι u \in X \| \forall x \in X u G x = x) \in \{u \in X \| \forall x \in X u G x = x\}$
7	3 6	eqeltrd	$⊢ G \in GrpOp \to U \in \{u \in X \| \forall x \in X u G x = x\}$
8		simpll	$⊢ ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \to u G x = x$
9	8	ralimi	$⊢ \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \to \forall x \in X u G x = x$
10	9	rgenw	$⊢ \forall u \in X (\forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \to \forall x \in X u G x = x)$
11	10	a1i	$⊢ G \in GrpOp \to \forall u \in X (\forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \to \forall x \in X u G x = x)$
12	1	grpoidinv	$⊢ G \in GrpOp \to \exists u \in X \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u))$
13	11 12 4	3jca	$⊢ G \in GrpOp \to (\forall u \in X (\forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \to \forall x \in X u G x = x) \land \exists u \in X \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \land \exists! u \in X \forall x \in X u G x = x)$
14		reupick2	$⊢ ((\forall u \in X (\forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \to \forall x \in X u G x = x) \land \exists u \in X \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \land \exists! u \in X \forall x \in X u G x = x) \land u \in X) \to (\forall x \in X u G x = x \leftrightarrow \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)))$
15	13 14	sylan	$⊢ (G \in GrpOp \land u \in X) \to (\forall x \in X u G x = x \leftrightarrow \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)))$
16	15	rabbidva	$⊢ G \in GrpOp \to \{u \in X \| \forall x \in X u G x = x\} = \{u \in X \| \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u))\}$
17	7 16	eleqtrd	$⊢ G \in GrpOp \to U \in \{u \in X \| \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u))\}$
18		oveq1	$⊢ u = U \to u G x = U G x$
19	18	eqeq1d	$⊢ u = U \to (u G x = x \leftrightarrow U G x = x)$
20		oveq2	$⊢ u = U \to x G u = x G U$
21	20	eqeq1d	$⊢ u = U \to (x G u = x \leftrightarrow x G U = x)$
22	19 21	anbi12d	$⊢ u = U \to ((u G x = x \land x G u = x) \leftrightarrow (U G x = x \land x G U = x))$
23		eqeq2	$⊢ u = U \to (y G x = u \leftrightarrow y G x = U)$
24		eqeq2	$⊢ u = U \to (x G y = u \leftrightarrow x G y = U)$
25	23 24	anbi12d	$⊢ u = U \to ((y G x = u \land x G y = u) \leftrightarrow (y G x = U \land x G y = U))$
26	25	rexbidv	$⊢ u = U \to (\exists y \in X (y G x = u \land x G y = u) \leftrightarrow \exists y \in X (y G x = U \land x G y = U))$
27	22 26	anbi12d	$⊢ u = U \to (((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \leftrightarrow ((U G x = x \land x G U = x) \land \exists y \in X (y G x = U \land x G y = U)))$
28	27	ralbidv	$⊢ u = U \to (\forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \leftrightarrow \forall x \in X ((U G x = x \land x G U = x) \land \exists y \in X (y G x = U \land x G y = U)))$
29	28	elrab	$⊢ U \in \{u \in X \| \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u))\} \leftrightarrow (U \in X \land \forall x \in X ((U G x = x \land x G U = x) \land \exists y \in X (y G x = U \land x G y = U)))$
30	17 29	sylib	$⊢ G \in GrpOp \to (U \in X \land \forall x \in X ((U G x = x \land x G U = x) \land \exists y \in X (y G x = U \land x G y = U)))$
31	30	simprd	$⊢ G \in GrpOp \to \forall x \in X ((U G x = x \land x G U = x) \land \exists y \in X (y G x = U \land x G y = U))$
32		oveq2	$⊢ x = A \to U G x = U G A$
33		id	$⊢ x = A \to x = A$
34	32 33	eqeq12d	$⊢ x = A \to (U G x = x \leftrightarrow U G A = A)$
35		oveq1	$⊢ x = A \to x G U = A G U$
36	35 33	eqeq12d	$⊢ x = A \to (x G U = x \leftrightarrow A G U = A)$
37	34 36	anbi12d	$⊢ x = A \to ((U G x = x \land x G U = x) \leftrightarrow (U G A = A \land A G U = A))$
38		oveq2	$⊢ x = A \to y G x = y G A$
39	38	eqeq1d	$⊢ x = A \to (y G x = U \leftrightarrow y G A = U)$
40		oveq1	$⊢ x = A \to x G y = A G y$
41	40	eqeq1d	$⊢ x = A \to (x G y = U \leftrightarrow A G y = U)$
42	39 41	anbi12d	$⊢ x = A \to ((y G x = U \land x G y = U) \leftrightarrow (y G A = U \land A G y = U))$
43	42	rexbidv	$⊢ x = A \to (\exists y \in X (y G x = U \land x G y = U) \leftrightarrow \exists y \in X (y G A = U \land A G y = U))$
44	37 43	anbi12d	$⊢ x = A \to (((U G x = x \land x G U = x) \land \exists y \in X (y G x = U \land x G y = U)) \leftrightarrow ((U G A = A \land A G U = A) \land \exists y \in X (y G A = U \land A G y = U)))$
45	44	rspccva	$⊢ (\forall x \in X ((U G x = x \land x G U = x) \land \exists y \in X (y G x = U \land x G y = U)) \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))$
46	31 45	sylan	$⊢ (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))$

Metamath Proof Explorer

Theorem grpoidinv2

Proof