Metamath Proof Explorer

Theorem grpraddf1o

Description: Right addition by a group element is a bijection on any group. (Contributed by SN, 28-Apr-2012)

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

Proof

Step Hyp Ref Expression
1 grpraddf1o.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpraddf1o.p ⊢ + = ( +g ‘ 𝐺 )
3 grpraddf1o.n ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 + 𝑋 ) )
4 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐺 ∈ Grp )
5 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
6 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7 1 2 4 5 6 grpcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 𝑋 ) ∈ 𝐵 )
8 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐺 ∈ Grp )
9 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
10 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
11 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12 1 10 8 11 grpinvcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 )
13 1 2 8 9 12 grpcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ∈ 𝐵 )
14 eqcom ⊢ ( 𝑥 = ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ↔ ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = 𝑥 )
15 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
16 13 adantrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ∈ 𝐵 )
17 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
18 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
19 1 2 grprcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑋 ) = ( 𝑥 + 𝑋 ) ↔ ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = 𝑥 ) )
20 15 16 17 18 19 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑋 ) = ( 𝑥 + 𝑋 ) ↔ ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = 𝑥 ) )
21 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
22 12 adantrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐵 )
23 1 2 15 21 22 18 grpassd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑋 ) = ( 𝑦 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑋 ) ) )
24 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
25 1 2 24 10 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑋 ) = ( 0g ‘ 𝐺 ) )
26 25 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑋 ) = ( 0g ‘ 𝐺 ) )
27 26 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) + 𝑋 ) ) = ( 𝑦 + ( 0g ‘ 𝐺 ) ) )
28 1 2 24 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 + ( 0g ‘ 𝐺 ) ) = 𝑦 )
29 28 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 + ( 0g ‘ 𝐺 ) ) = 𝑦 )
30 23 27 29 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑋 ) = 𝑦 )
31 30 eqeq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) + 𝑋 ) = ( 𝑥 + 𝑋 ) ↔ 𝑦 = ( 𝑥 + 𝑋 ) ) )
32 20 31 bitr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = 𝑥 ↔ 𝑦 = ( 𝑥 + 𝑋 ) ) )
33 14 32 bitrid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ↔ 𝑦 = ( 𝑥 + 𝑋 ) ) )
34 3 7 13 33 f1o2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )