Metamath Proof Explorer

Theorem gapm

Description: The action of a particular group element is a permutation of the base set. (Contributed by Jeff Hankins, 11-Aug-2009) (Proof shortened by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses gapm.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gapm.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑌 ↦ ( 𝐴 ⊕ 𝑥 ) )
Assertion gapm ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐹 : 𝑌 –1-1-onto→ 𝑌 )

Proof

Step Hyp Ref Expression
1 gapm.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gapm.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑌 ↦ ( 𝐴 ⊕ 𝑥 ) )
3 1 gaf ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
4 3 ad2antrr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
5 simplr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
6 simpr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑌 )
7 4 5 6 fovcdmd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 ⊕ 𝑥 ) ∈ 𝑌 )
8 3 ad2antrr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
9 gagrp ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐺 ∈ Grp )
10 9 ad2antrr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐺 ∈ Grp )
11 simplr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
12 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
13 1 12 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
14 10 11 13 syl2anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
15 simpr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
16 8 14 15 fovcdmd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ 𝑦 ) ∈ 𝑌 )
17 simpll ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
18 simplr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → 𝐴 ∈ 𝑋 )
19 simprl ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑥 ∈ 𝑌 )
20 simprr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑦 ∈ 𝑌 )
21 1 12 gacan ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝑥 ) = 𝑦 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ 𝑦 ) = 𝑥 ) )
22 17 18 19 20 21 syl13anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝑥 ) = 𝑦 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ 𝑦 ) = 𝑥 ) )
23 22 bicomd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ 𝑦 ) = 𝑥 ↔ ( 𝐴 ⊕ 𝑥 ) = 𝑦 ) )
24 eqcom ⊢ ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ 𝑦 ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ 𝑦 ) = 𝑥 )
25 eqcom ⊢ ( 𝑦 = ( 𝐴 ⊕ 𝑥 ) ↔ ( 𝐴 ⊕ 𝑥 ) = 𝑦 )
26 23 24 25 3bitr4g ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ 𝑦 ) ↔ 𝑦 = ( 𝐴 ⊕ 𝑥 ) ) )
27 2 7 16 26 f1o2d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐹 : 𝑌 –1-1-onto→ 𝑌 )