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 fovrnd ( ( ( ∈ ( 𝐺 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 fovrnd ( ( ( ∈ ( 𝐺 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𝑌 )