Step |
Hyp |
Ref |
Expression |
1 |
|
gasta.1 |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
gasta.2 |
⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐴 ) = 𝐴 } |
3 |
|
orbsta.r |
⊢ ∼ = ( 𝐺 ~QG 𝐻 ) |
4 |
1 2
|
gastacl |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |
5 |
4
|
adantr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |
6 |
|
subgrcl |
⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) |
7 |
5 6
|
syl |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐺 ∈ Grp ) |
8 |
1
|
subgss |
⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ⊆ 𝑋 ) |
9 |
5 8
|
syl |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐻 ⊆ 𝑋 ) |
10 |
|
eqid |
⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 ) |
11 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
12 |
1 10 11 3
|
eqgval |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ⊆ 𝑋 ) → ( 𝐵 ∼ 𝐶 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ) ) ) |
13 |
7 9 12
|
syl2anc |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ∼ 𝐶 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ) ) ) |
14 |
|
df-3an |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ) ↔ ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ) ) |
15 |
13 14
|
bitrdi |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ∼ 𝐶 ↔ ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ) ) ) |
16 |
|
simpr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) |
17 |
16
|
biantrurd |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ) ) ) |
18 |
|
simpll |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ) |
19 |
|
simprl |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 ) |
20 |
1 10
|
grpinvcl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ) |
21 |
7 19 20
|
syl2anc |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ) |
22 |
|
simprr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 ) |
23 |
|
simplr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑌 ) |
24 |
1 11
|
gaass |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ⊕ 𝐴 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ⊕ ( 𝐶 ⊕ 𝐴 ) ) ) |
25 |
18 21 22 23 24
|
syl13anc |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ⊕ 𝐴 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ⊕ ( 𝐶 ⊕ 𝐴 ) ) ) |
26 |
25
|
eqeq1d |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ⊕ 𝐴 ) = 𝐴 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ⊕ ( 𝐶 ⊕ 𝐴 ) ) = 𝐴 ) ) |
27 |
1 11
|
grpcl |
⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 ) |
28 |
7 21 22 27
|
syl3anc |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 ) |
29 |
|
oveq1 |
⊢ ( 𝑢 = ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) → ( 𝑢 ⊕ 𝐴 ) = ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ⊕ 𝐴 ) ) |
30 |
29
|
eqeq1d |
⊢ ( 𝑢 = ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) → ( ( 𝑢 ⊕ 𝐴 ) = 𝐴 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ⊕ 𝐴 ) = 𝐴 ) ) |
31 |
30 2
|
elrab2 |
⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 ∧ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ⊕ 𝐴 ) = 𝐴 ) ) |
32 |
31
|
baib |
⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ⊕ 𝐴 ) = 𝐴 ) ) |
33 |
28 32
|
syl |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ⊕ 𝐴 ) = 𝐴 ) ) |
34 |
1
|
gaf |
⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 ) |
35 |
18 34
|
syl |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 ) |
36 |
35 22 23
|
fovrnd |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐶 ⊕ 𝐴 ) ∈ 𝑌 ) |
37 |
1 10
|
gacan |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ∧ ( 𝐶 ⊕ 𝐴 ) ∈ 𝑌 ) ) → ( ( 𝐵 ⊕ 𝐴 ) = ( 𝐶 ⊕ 𝐴 ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ⊕ ( 𝐶 ⊕ 𝐴 ) ) = 𝐴 ) ) |
38 |
18 19 23 36 37
|
syl13anc |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐵 ⊕ 𝐴 ) = ( 𝐶 ⊕ 𝐴 ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ⊕ ( 𝐶 ⊕ 𝐴 ) ) = 𝐴 ) ) |
39 |
26 33 38
|
3bitr4d |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ( +g ‘ 𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( 𝐵 ⊕ 𝐴 ) = ( 𝐶 ⊕ 𝐴 ) ) ) |
40 |
15 17 39
|
3bitr2d |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ∼ 𝐶 ↔ ( 𝐵 ⊕ 𝐴 ) = ( 𝐶 ⊕ 𝐴 ) ) ) |