Metamath Proof Explorer

Theorem grplmulf1o

Description: Left multiplication by a group element is a bijection on any group. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypotheses grplmulf1o.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
grplmulf1o.p ⊢ + = ( +g ‘ 𝐺 )
grplmulf1o.n ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑋 + 𝑥 ) )
Assertion grplmulf1o ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 grplmulf1o.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grplmulf1o.p ⊢ + = ( +g ‘ 𝐺 )
3 grplmulf1o.n ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑋 + 𝑥 ) )
4 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 + 𝑥 ) ∈ 𝐵 )
5 4 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 + 𝑥 ) ∈ 𝐵 )
6 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
7 1 6 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 )
8 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ∈ 𝐵 )
9 8 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ∈ 𝐵 )
10 7 9 syldanl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ∈ 𝐵 )
11 eqcom ⊢ ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) = 𝑥 )
12 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
13 10 adantrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ∈ 𝐵 )
14 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
15 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
16 1 2 grplcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ) = ( 𝑋 + 𝑥 ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) = 𝑥 ) )
17 12 13 14 15 16 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑋 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ) = ( 𝑋 + 𝑥 ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) = 𝑥 ) )
18 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
19 1 2 18 6 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
20 19 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
21 20 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑦 ) = ( ( 0g ‘ 𝐺 ) + 𝑦 ) )
22 7 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 )
23 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
24 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑦 ) = ( 𝑋 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ) )
25 12 15 22 23 24 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑋 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑦 ) = ( 𝑋 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ) )
26 1 2 18 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑦 ) = 𝑦 )
27 26 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 0g ‘ 𝐺 ) + 𝑦 ) = 𝑦 )
28 21 25 27 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑋 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ) = 𝑦 )
29 28 eqeq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑋 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ) = ( 𝑋 + 𝑥 ) ↔ 𝑦 = ( 𝑋 + 𝑥 ) ) )
30 17 29 bitr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) = 𝑥 ↔ 𝑦 = ( 𝑋 + 𝑥 ) ) )
31 11 30 syl5bb ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑦 ) ↔ 𝑦 = ( 𝑋 + 𝑥 ) ) )
32 3 5 10 31 f1o2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )