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→ 𝑌 ) |