grplactcnv

Description: The left group action of element A of group G maps the underlying set X of G one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008) (Proof shortened by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	grplact.1	$⊢ F = (g \in X ⟼ (a \in X ⟼ g \underset{˙}{+} a))$
	grplact.2	$⊢ X = {Base}_{G}$
	grplact.3	$⊢ \underset{˙}{+} = +_{G}$
	grplactcnv.4	$⊢ I = {inv}_{g} (G)$
Assertion	grplactcnv	$⊢ (G \in Grp \land A \in X) \to (F (A) : X \underset{1-1 onto}{⟶} X \land {F (A)}^{-1} = F (I (A)))$

Proof

Step	Hyp	Ref	Expression
1		grplact.1	$⊢ F = (g \in X ⟼ (a \in X ⟼ g \underset{˙}{+} a))$
2		grplact.2	$⊢ X = {Base}_{G}$
3		grplact.3	$⊢ \underset{˙}{+} = +_{G}$
4		grplactcnv.4	$⊢ I = {inv}_{g} (G)$
5		eqid	$⊢ (a \in X ⟼ A \underset{˙}{+} a) = (a \in X ⟼ A \underset{˙}{+} a)$
6	2 3	grpcl	$⊢ (G \in Grp \land A \in X \land a \in X) \to A \underset{˙}{+} a \in X$
7	6	3expa	$⊢ ((G \in Grp \land A \in X) \land a \in X) \to A \underset{˙}{+} a \in X$
8	2 4	grpinvcl	$⊢ (G \in Grp \land A \in X) \to I (A) \in X$
9	2 3	grpcl	$⊢ (G \in Grp \land I (A) \in X \land b \in X) \to I (A) \underset{˙}{+} b \in X$
10	9	3expa	$⊢ ((G \in Grp \land I (A) \in X) \land b \in X) \to I (A) \underset{˙}{+} b \in X$
11	8 10	syldanl	$⊢ ((G \in Grp \land A \in X) \land b \in X) \to I (A) \underset{˙}{+} b \in X$
12		eqcom	$⊢ a = I (A) \underset{˙}{+} b \leftrightarrow I (A) \underset{˙}{+} b = a$
13		eqid	$⊢ 0_{G} = 0_{G}$
14	2 3 13 4	grplinv	$⊢ (G \in Grp \land A \in X) \to I (A) \underset{˙}{+} A = 0_{G}$
15	14	adantr	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to I (A) \underset{˙}{+} A = 0_{G}$
16	15	oveq1d	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to (I (A) \underset{˙}{+} A) \underset{˙}{+} a = 0_{G} \underset{˙}{+} a$
17		simpll	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to G \in Grp$
18	8	adantr	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to I (A) \in X$
19		simplr	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to A \in X$
20		simprl	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to a \in X$
21	2 3	grpass	$⊢ (G \in Grp \land (I (A) \in X \land A \in X \land a \in X)) \to (I (A) \underset{˙}{+} A) \underset{˙}{+} a = I (A) \underset{˙}{+} (A \underset{˙}{+} a)$
22	17 18 19 20 21	syl13anc	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to (I (A) \underset{˙}{+} A) \underset{˙}{+} a = I (A) \underset{˙}{+} (A \underset{˙}{+} a)$
23	2 3 13	grplid	$⊢ (G \in Grp \land a \in X) \to 0_{G} \underset{˙}{+} a = a$
24	23	ad2ant2r	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to 0_{G} \underset{˙}{+} a = a$
25	16 22 24	3eqtr3rd	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to a = I (A) \underset{˙}{+} (A \underset{˙}{+} a)$
26	25	eqeq2d	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to (I (A) \underset{˙}{+} b = a \leftrightarrow I (A) \underset{˙}{+} b = I (A) \underset{˙}{+} (A \underset{˙}{+} a))$
27	12 26	syl5bb	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to (a = I (A) \underset{˙}{+} b \leftrightarrow I (A) \underset{˙}{+} b = I (A) \underset{˙}{+} (A \underset{˙}{+} a))$
28		simprr	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to b \in X$
29	7	adantrr	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to A \underset{˙}{+} a \in X$
30	2 3	grplcan	$⊢ (G \in Grp \land (b \in X \land A \underset{˙}{+} a \in X \land I (A) \in X)) \to (I (A) \underset{˙}{+} b = I (A) \underset{˙}{+} (A \underset{˙}{+} a) \leftrightarrow b = A \underset{˙}{+} a)$
31	17 28 29 18 30	syl13anc	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to (I (A) \underset{˙}{+} b = I (A) \underset{˙}{+} (A \underset{˙}{+} a) \leftrightarrow b = A \underset{˙}{+} a)$
32	27 31	bitrd	$⊢ ((G \in Grp \land A \in X) \land (a \in X \land b \in X)) \to (a = I (A) \underset{˙}{+} b \leftrightarrow b = A \underset{˙}{+} a)$
33	5 7 11 32	f1ocnv2d	$⊢ (G \in Grp \land A \in X) \to ((a \in X ⟼ A \underset{˙}{+} a) : X \underset{1-1 onto}{⟶} X \land {(a \in X ⟼ A \underset{˙}{+} a)}^{-1} = (b \in X ⟼ I (A) \underset{˙}{+} b))$
34	1 2	grplactfval	$⊢ A \in X \to F (A) = (a \in X ⟼ A \underset{˙}{+} a)$
35	34	adantl	$⊢ (G \in Grp \land A \in X) \to F (A) = (a \in X ⟼ A \underset{˙}{+} a)$
36		f1oeq1	$⊢ F (A) = (a \in X ⟼ A \underset{˙}{+} a) \to (F (A) : X \underset{1-1 onto}{⟶} X \leftrightarrow (a \in X ⟼ A \underset{˙}{+} a) : X \underset{1-1 onto}{⟶} X)$
37	35 36	syl	$⊢ (G \in Grp \land A \in X) \to (F (A) : X \underset{1-1 onto}{⟶} X \leftrightarrow (a \in X ⟼ A \underset{˙}{+} a) : X \underset{1-1 onto}{⟶} X)$
38	35	cnveqd	$⊢ (G \in Grp \land A \in X) \to {F (A)}^{-1} = {(a \in X ⟼ A \underset{˙}{+} a)}^{-1}$
39	1 2	grplactfval	$⊢ I (A) \in X \to F (I (A)) = (a \in X ⟼ I (A) \underset{˙}{+} a)$
40		oveq2	$⊢ a = b \to I (A) \underset{˙}{+} a = I (A) \underset{˙}{+} b$
41	40	cbvmptv	$⊢ (a \in X ⟼ I (A) \underset{˙}{+} a) = (b \in X ⟼ I (A) \underset{˙}{+} b)$
42	39 41	eqtrdi	$⊢ I (A) \in X \to F (I (A)) = (b \in X ⟼ I (A) \underset{˙}{+} b)$
43	8 42	syl	$⊢ (G \in Grp \land A \in X) \to F (I (A)) = (b \in X ⟼ I (A) \underset{˙}{+} b)$
44	38 43	eqeq12d	$⊢ (G \in Grp \land A \in X) \to ({F (A)}^{-1} = F (I (A)) \leftrightarrow {(a \in X ⟼ A \underset{˙}{+} a)}^{-1} = (b \in X ⟼ I (A) \underset{˙}{+} b))$
45	37 44	anbi12d	$⊢ (G \in Grp \land A \in X) \to ((F (A) : X \underset{1-1 onto}{⟶} X \land {F (A)}^{-1} = F (I (A))) \leftrightarrow ((a \in X ⟼ A \underset{˙}{+} a) : X \underset{1-1 onto}{⟶} X \land {(a \in X ⟼ A \underset{˙}{+} a)}^{-1} = (b \in X ⟼ I (A) \underset{˙}{+} b)))$
46	33 45	mpbird	$⊢ (G \in Grp \land A \in X) \to (F (A) : X \underset{1-1 onto}{⟶} X \land {F (A)}^{-1} = F (I (A)))$

Metamath Proof Explorer

Theorem grplactcnv

Proof