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	\|- .+ = ( +g ` G )
	conjghm.m	\|- .- = ( -g ` G )
	conjghm.f	\|- F = ( x e. X \|-> ( ( A .+ x ) .- A ) )
Assertion	conjghm	\|- ( ( G e. Grp /\ A e. X ) -> ( F e. ( G GrpHom G ) /\ F : X -1-1-onto-> X ) )

Proof

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

Metamath Proof Explorer

Theorem conjghm

Proof