Metamath Proof Explorer

Theorem 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 ) )