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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
conjghm.p ⊢ + = ( +g ‘ 𝐺 )
conjghm.m ⊢ − = ( -g ‘ 𝐺 )
conjghm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
Assertion conjghm ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑋 ) )

Proof

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