conjghm

Description: Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	conjghm.x	$⊢ X = {Base}_{G}$
	conjghm.p	$⊢ \underset{˙}{+} = +_{G}$
	conjghm.m	$⊢ \underset{˙}{-} = -_{G}$
	conjghm.f	$⊢ F = (x \in X ⟼ (A \underset{˙}{+} x) \underset{˙}{-} A)$
Assertion	conjghm	$⊢ (G \in Grp \land A \in X) \to (F \in (G GrpHom G) \land F : X \underset{1-1 onto}{⟶} X)$

Proof

Step	Hyp	Ref	Expression
1		conjghm.x	$⊢ X = {Base}_{G}$
2		conjghm.p	$⊢ \underset{˙}{+} = +_{G}$
3		conjghm.m	$⊢ \underset{˙}{-} = -_{G}$
4		conjghm.f	$⊢ F = (x \in X ⟼ (A \underset{˙}{+} x) \underset{˙}{-} A)$
5		simpl	$⊢ (G \in Grp \land A \in X) \to G \in Grp$
6	5	adantr	$⊢ ((G \in Grp \land A \in X) \land x \in X) \to G \in Grp$
7	1 2	grpcl	$⊢ (G \in Grp \land A \in X \land x \in X) \to A \underset{˙}{+} x \in X$
8	7	3expa	$⊢ ((G \in Grp \land A \in X) \land x \in X) \to A \underset{˙}{+} x \in X$
9		simplr	$⊢ ((G \in Grp \land A \in X) \land x \in X) \to A \in X$
10	1 3	grpsubcl	$⊢ (G \in Grp \land A \underset{˙}{+} x \in X \land A \in X) \to (A \underset{˙}{+} x) \underset{˙}{-} A \in X$
11	6 8 9 10	syl3anc	$⊢ ((G \in Grp \land A \in X) \land x \in X) \to (A \underset{˙}{+} x) \underset{˙}{-} A \in X$
12	11 4	fmptd	$⊢ (G \in Grp \land A \in X) \to F : X ⟶ X$
13	5	adantr	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to G \in Grp$
14		simplr	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to A \in X$
15		simprl	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to y \in X$
16	1 2	grpcl	$⊢ (G \in Grp \land A \in X \land y \in X) \to A \underset{˙}{+} y \in X$
17	13 14 15 16	syl3anc	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to A \underset{˙}{+} y \in X$
18	1 3	grpsubcl	$⊢ (G \in Grp \land A \underset{˙}{+} y \in X \land A \in X) \to (A \underset{˙}{+} y) \underset{˙}{-} A \in X$
19	13 17 14 18	syl3anc	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to (A \underset{˙}{+} y) \underset{˙}{-} A \in X$
20		simprr	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to z \in X$
21	1 3	grpsubcl	$⊢ (G \in Grp \land z \in X \land A \in X) \to z \underset{˙}{-} A \in X$
22	13 20 14 21	syl3anc	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to z \underset{˙}{-} A \in X$
23	1 2	grpass	$⊢ (G \in Grp \land ((A \underset{˙}{+} y) \underset{˙}{-} A \in X \land A \in X \land z \underset{˙}{-} A \in X)) \to (((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} A) \underset{˙}{+} (z \underset{˙}{-} A) = ((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} (A \underset{˙}{+} (z \underset{˙}{-} A))$
24	13 19 14 22 23	syl13anc	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to (((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} A) \underset{˙}{+} (z \underset{˙}{-} A) = ((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} (A \underset{˙}{+} (z \underset{˙}{-} A))$
25	1 2 3	grpnpcan	$⊢ (G \in Grp \land A \underset{˙}{+} y \in X \land A \in X) \to ((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} A = A \underset{˙}{+} y$
26	13 17 14 25	syl3anc	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to ((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} A = A \underset{˙}{+} y$
27	26	oveq1d	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to (((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} A) \underset{˙}{+} (z \underset{˙}{-} A) = (A \underset{˙}{+} y) \underset{˙}{+} (z \underset{˙}{-} A)$
28	1 2 3	grpaddsubass	$⊢ (G \in Grp \land (A \underset{˙}{+} y \in X \land z \in X \land A \in X)) \to ((A \underset{˙}{+} y) \underset{˙}{+} z) \underset{˙}{-} A = (A \underset{˙}{+} y) \underset{˙}{+} (z \underset{˙}{-} A)$
29	13 17 20 14 28	syl13anc	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to ((A \underset{˙}{+} y) \underset{˙}{+} z) \underset{˙}{-} A = (A \underset{˙}{+} y) \underset{˙}{+} (z \underset{˙}{-} A)$
30	1 2	grpass	$⊢ (G \in Grp \land (A \in X \land y \in X \land z \in X)) \to (A \underset{˙}{+} y) \underset{˙}{+} z = A \underset{˙}{+} (y \underset{˙}{+} z)$
31	13 14 15 20 30	syl13anc	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to (A \underset{˙}{+} y) \underset{˙}{+} z = A \underset{˙}{+} (y \underset{˙}{+} z)$
32	31	oveq1d	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to ((A \underset{˙}{+} y) \underset{˙}{+} z) \underset{˙}{-} A = (A \underset{˙}{+} (y \underset{˙}{+} z)) \underset{˙}{-} A$
33	27 29 32	3eqtr2rd	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to (A \underset{˙}{+} (y \underset{˙}{+} z)) \underset{˙}{-} A = (((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} A) \underset{˙}{+} (z \underset{˙}{-} A)$
34	1 2 3	grpaddsubass	$⊢ (G \in Grp \land (A \in X \land z \in X \land A \in X)) \to (A \underset{˙}{+} z) \underset{˙}{-} A = A \underset{˙}{+} (z \underset{˙}{-} A)$
35	13 14 20 14 34	syl13anc	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to (A \underset{˙}{+} z) \underset{˙}{-} A = A \underset{˙}{+} (z \underset{˙}{-} A)$
36	35	oveq2d	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to ((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} ((A \underset{˙}{+} z) \underset{˙}{-} A) = ((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} (A \underset{˙}{+} (z \underset{˙}{-} A))$
37	24 33 36	3eqtr4d	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to (A \underset{˙}{+} (y \underset{˙}{+} z)) \underset{˙}{-} A = ((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} ((A \underset{˙}{+} z) \underset{˙}{-} A)$
38	1 2	grpcl	$⊢ (G \in Grp \land y \in X \land z \in X) \to y \underset{˙}{+} z \in X$
39	13 15 20 38	syl3anc	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to y \underset{˙}{+} z \in X$
40		oveq2	$⊢ x = y \underset{˙}{+} z \to A \underset{˙}{+} x = A \underset{˙}{+} (y \underset{˙}{+} z)$
41	40	oveq1d	$⊢ x = y \underset{˙}{+} z \to (A \underset{˙}{+} x) \underset{˙}{-} A = (A \underset{˙}{+} (y \underset{˙}{+} z)) \underset{˙}{-} A$
42		ovex	$⊢ (A \underset{˙}{+} (y \underset{˙}{+} z)) \underset{˙}{-} A \in V$
43	41 4 42	fvmpt	$⊢ y \underset{˙}{+} z \in X \to F (y \underset{˙}{+} z) = (A \underset{˙}{+} (y \underset{˙}{+} z)) \underset{˙}{-} A$
44	39 43	syl	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to F (y \underset{˙}{+} z) = (A \underset{˙}{+} (y \underset{˙}{+} z)) \underset{˙}{-} A$
45		oveq2	$⊢ x = y \to A \underset{˙}{+} x = A \underset{˙}{+} y$
46	45	oveq1d	$⊢ x = y \to (A \underset{˙}{+} x) \underset{˙}{-} A = (A \underset{˙}{+} y) \underset{˙}{-} A$
47		ovex	$⊢ (A \underset{˙}{+} y) \underset{˙}{-} A \in V$
48	46 4 47	fvmpt	$⊢ y \in X \to F (y) = (A \underset{˙}{+} y) \underset{˙}{-} A$
49	48	ad2antrl	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to F (y) = (A \underset{˙}{+} y) \underset{˙}{-} A$
50		oveq2	$⊢ x = z \to A \underset{˙}{+} x = A \underset{˙}{+} z$
51	50	oveq1d	$⊢ x = z \to (A \underset{˙}{+} x) \underset{˙}{-} A = (A \underset{˙}{+} z) \underset{˙}{-} A$
52		ovex	$⊢ (A \underset{˙}{+} z) \underset{˙}{-} A \in V$
53	51 4 52	fvmpt	$⊢ z \in X \to F (z) = (A \underset{˙}{+} z) \underset{˙}{-} A$
54	53	ad2antll	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to F (z) = (A \underset{˙}{+} z) \underset{˙}{-} A$
55	49 54	oveq12d	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to F (y) \underset{˙}{+} F (z) = ((A \underset{˙}{+} y) \underset{˙}{-} A) \underset{˙}{+} ((A \underset{˙}{+} z) \underset{˙}{-} A)$
56	37 44 55	3eqtr4d	$⊢ ((G \in Grp \land A \in X) \land (y \in X \land z \in X)) \to F (y \underset{˙}{+} z) = F (y) \underset{˙}{+} F (z)$
57	1 1 2 2 5 5 12 56	isghmd	$⊢ (G \in Grp \land A \in X) \to F \in (G GrpHom G)$
58	5	adantr	$⊢ ((G \in Grp \land A \in X) \land y \in X) \to G \in Grp$
59		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
60	1 59	grpinvcl	$⊢ (G \in Grp \land A \in X) \to {inv}_{g} (G) (A) \in X$
61	60	adantr	$⊢ ((G \in Grp \land A \in X) \land y \in X) \to {inv}_{g} (G) (A) \in X$
62		simpr	$⊢ ((G \in Grp \land A \in X) \land y \in X) \to y \in X$
63		simplr	$⊢ ((G \in Grp \land A \in X) \land y \in X) \to A \in X$
64	1 2	grpcl	$⊢ (G \in Grp \land y \in X \land A \in X) \to y \underset{˙}{+} A \in X$
65	58 62 63 64	syl3anc	$⊢ ((G \in Grp \land A \in X) \land y \in X) \to y \underset{˙}{+} A \in X$
66	1 2	grpcl	$⊢ (G \in Grp \land {inv}_{g} (G) (A) \in X \land y \underset{˙}{+} A \in X) \to {inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) \in X$
67	58 61 65 66	syl3anc	$⊢ ((G \in Grp \land A \in X) \land y \in X) \to {inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) \in X$
68	5	adantr	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to G \in Grp$
69	65	adantrl	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to y \underset{˙}{+} A \in X$
70	8	adantrr	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to A \underset{˙}{+} x \in X$
71	60	adantr	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to {inv}_{g} (G) (A) \in X$
72	1 2	grplcan	$⊢ (G \in Grp \land (y \underset{˙}{+} A \in X \land A \underset{˙}{+} x \in X \land {inv}_{g} (G) (A) \in X)) \to ({inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) = {inv}_{g} (G) (A) \underset{˙}{+} (A \underset{˙}{+} x) \leftrightarrow y \underset{˙}{+} A = A \underset{˙}{+} x)$
73	68 69 70 71 72	syl13anc	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to ({inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) = {inv}_{g} (G) (A) \underset{˙}{+} (A \underset{˙}{+} x) \leftrightarrow y \underset{˙}{+} A = A \underset{˙}{+} x)$
74		eqid	$⊢ 0_{G} = 0_{G}$
75	1 2 74 59	grplinv	$⊢ (G \in Grp \land A \in X) \to {inv}_{g} (G) (A) \underset{˙}{+} A = 0_{G}$
76	75	adantr	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to {inv}_{g} (G) (A) \underset{˙}{+} A = 0_{G}$
77	76	oveq1d	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to ({inv}_{g} (G) (A) \underset{˙}{+} A) \underset{˙}{+} x = 0_{G} \underset{˙}{+} x$
78		simplr	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to A \in X$
79		simprl	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to x \in X$
80	1 2	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (A) \in X \land A \in X \land x \in X)) \to ({inv}_{g} (G) (A) \underset{˙}{+} A) \underset{˙}{+} x = {inv}_{g} (G) (A) \underset{˙}{+} (A \underset{˙}{+} x)$
81	68 71 78 79 80	syl13anc	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to ({inv}_{g} (G) (A) \underset{˙}{+} A) \underset{˙}{+} x = {inv}_{g} (G) (A) \underset{˙}{+} (A \underset{˙}{+} x)$
82	1 2 74	grplid	$⊢ (G \in Grp \land x \in X) \to 0_{G} \underset{˙}{+} x = x$
83	82	ad2ant2r	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to 0_{G} \underset{˙}{+} x = x$
84	77 81 83	3eqtr3rd	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to x = {inv}_{g} (G) (A) \underset{˙}{+} (A \underset{˙}{+} x)$
85	84	eqeq2d	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to ({inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) = x \leftrightarrow {inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) = {inv}_{g} (G) (A) \underset{˙}{+} (A \underset{˙}{+} x))$
86		simprr	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to y \in X$
87	1 2 3	grpsubadd	$⊢ (G \in Grp \land (A \underset{˙}{+} x \in X \land A \in X \land y \in X)) \to ((A \underset{˙}{+} x) \underset{˙}{-} A = y \leftrightarrow y \underset{˙}{+} A = A \underset{˙}{+} x)$
88	68 70 78 86 87	syl13anc	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to ((A \underset{˙}{+} x) \underset{˙}{-} A = y \leftrightarrow y \underset{˙}{+} A = A \underset{˙}{+} x)$
89	73 85 88	3bitr4d	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to ({inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) = x \leftrightarrow (A \underset{˙}{+} x) \underset{˙}{-} A = y)$
90		eqcom	$⊢ x = {inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) \leftrightarrow {inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) = x$
91		eqcom	$⊢ y = (A \underset{˙}{+} x) \underset{˙}{-} A \leftrightarrow (A \underset{˙}{+} x) \underset{˙}{-} A = y$
92	89 90 91	3bitr4g	$⊢ ((G \in Grp \land A \in X) \land (x \in X \land y \in X)) \to (x = {inv}_{g} (G) (A) \underset{˙}{+} (y \underset{˙}{+} A) \leftrightarrow y = (A \underset{˙}{+} x) \underset{˙}{-} A)$
93	4 11 67 92	f1o2d	$⊢ (G \in Grp \land A \in X) \to F : X \underset{1-1 onto}{⟶} X$
94	57 93	jca	$⊢ (G \in Grp \land A \in X) \to (F \in (G GrpHom G) \land F : X \underset{1-1 onto}{⟶} X)$

Metamath Proof Explorer

Theorem conjghm

Proof