Metamath Proof Explorer

Theorem 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 ⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
grplact.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
grplact.3 ⊢ + = ( +g ‘ 𝐺 )
grplactcnv.4 ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion grplactcnv ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐼 ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 grplact.1 ⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
2 grplact.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 grplact.3 ⊢ + = ( +g ‘ 𝐺 )
4 grplactcnv.4 ⊢ 𝐼 = ( invg ‘ 𝐺 )
5 eqid ⊢ ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) )
6 2 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) → ( 𝐴 + 𝑎 ) ∈ 𝑋 )
7 6 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝐴 + 𝑎 ) ∈ 𝑋 )
8 2 4 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 )
9 2 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ∈ 𝑋 )
10 9 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ∈ 𝑋 )
11 8 10 syldanl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ∈ 𝑋 )
12 eqcom ⊢ ( 𝑎 = ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ↔ ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) = 𝑎 )
13 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
14 2 3 13 4 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐼 ‘ 𝐴 ) + 𝐴 ) = ( 0g ‘ 𝐺 ) )
15 14 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝐼 ‘ 𝐴 ) + 𝐴 ) = ( 0g ‘ 𝐺 ) )
16 15 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( 𝐼 ‘ 𝐴 ) + 𝐴 ) + 𝑎 ) = ( ( 0g ‘ 𝐺 ) + 𝑎 ) )
17 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝐺 ∈ Grp )
18 8 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 )
19 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
20 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑎 ∈ 𝑋 )
21 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) ) → ( ( ( 𝐼 ‘ 𝐴 ) + 𝐴 ) + 𝑎 ) = ( ( 𝐼 ‘ 𝐴 ) + ( 𝐴 + 𝑎 ) ) )
22 17 18 19 20 21 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( 𝐼 ‘ 𝐴 ) + 𝐴 ) + 𝑎 ) = ( ( 𝐼 ‘ 𝐴 ) + ( 𝐴 + 𝑎 ) ) )
23 2 3 13 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑎 ) = 𝑎 )
24 23 ad2ant2r ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 0g ‘ 𝐺 ) + 𝑎 ) = 𝑎 )
25 16 22 24 3eqtr3rd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑎 = ( ( 𝐼 ‘ 𝐴 ) + ( 𝐴 + 𝑎 ) ) )
26 25 eqeq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) = 𝑎 ↔ ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) = ( ( 𝐼 ‘ 𝐴 ) + ( 𝐴 + 𝑎 ) ) ) )
27 12 26 bitrid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 = ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ↔ ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) = ( ( 𝐼 ‘ 𝐴 ) + ( 𝐴 + 𝑎 ) ) ) )
28 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑏 ∈ 𝑋 )
29 7 adantrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐴 + 𝑎 ) ∈ 𝑋 )
30 2 3 grplcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑏 ∈ 𝑋 ∧ ( 𝐴 + 𝑎 ) ∈ 𝑋 ∧ ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 ) ) → ( ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) = ( ( 𝐼 ‘ 𝐴 ) + ( 𝐴 + 𝑎 ) ) ↔ 𝑏 = ( 𝐴 + 𝑎 ) ) )
31 17 28 29 18 30 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) = ( ( 𝐼 ‘ 𝐴 ) + ( 𝐴 + 𝑎 ) ) ↔ 𝑏 = ( 𝐴 + 𝑎 ) ) )
32 27 31 bitrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 = ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ↔ 𝑏 = ( 𝐴 + 𝑎 ) ) )
33 5 7 11 32 f1ocnv2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) = ( 𝑏 ∈ 𝑋 ↦ ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ) ) )
34 1 2 grplactfval ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐹 ‘ 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) )
35 34 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) )
36 35 f1oeq1d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ↔ ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) : 𝑋 –1-1-onto→ 𝑋 ) )
37 35 cnveqd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ◡ ( 𝐹 ‘ 𝐴 ) = ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) )
38 1 2 grplactfval ⊢ ( ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 → ( 𝐹 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑎 ∈ 𝑋 ↦ ( ( 𝐼 ‘ 𝐴 ) + 𝑎 ) ) )
39 oveq2 ⊢ ( 𝑎 = 𝑏 → ( ( 𝐼 ‘ 𝐴 ) + 𝑎 ) = ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) )
40 39 cbvmptv ⊢ ( 𝑎 ∈ 𝑋 ↦ ( ( 𝐼 ‘ 𝐴 ) + 𝑎 ) ) = ( 𝑏 ∈ 𝑋 ↦ ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) )
41 38 40 eqtrdi ⊢ ( ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 → ( 𝐹 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑏 ∈ 𝑋 ↦ ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ) )
42 8 41 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑏 ∈ 𝑋 ↦ ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ) )
43 37 42 eqeq12d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ◡ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐼 ‘ 𝐴 ) ) ↔ ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) = ( 𝑏 ∈ 𝑋 ↦ ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ) ) )
44 36 43 anbi12d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐼 ‘ 𝐴 ) ) ) ↔ ( ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝐴 + 𝑎 ) ) = ( 𝑏 ∈ 𝑋 ↦ ( ( 𝐼 ‘ 𝐴 ) + 𝑏 ) ) ) ) )
45 33 44 mpbird ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐼 ‘ 𝐴 ) ) ) )