Step | Hyp | Ref
| Expression |
1 | | gasta.2 |
. . . 4
⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} |
2 | | ssrab2 3650 |
. . . 4
⊢ {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} ⊆ 𝑋 |
3 | 1, 2 | eqsstri 3598 |
. . 3
⊢ 𝐻 ⊆ 𝑋 |
4 | 3 | a1i 11 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ⊆ 𝑋) |
5 | | gagrp 17548 |
. . . . . 6
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp) |
6 | 5 | adantr 480 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐺 ∈ Grp) |
7 | | gasta.1 |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
8 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
9 | 7, 8 | grpidcl 17273 |
. . . . 5
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
10 | 6, 9 | syl 17 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (0g‘𝐺) ∈ 𝑋) |
11 | 8 | gagrpid 17550 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝐴) = 𝐴) |
12 | | oveq1 6556 |
. . . . . 6
⊢ (𝑢 = (0g‘𝐺) → (𝑢 ⊕ 𝐴) = ((0g‘𝐺) ⊕ 𝐴)) |
13 | 12 | eqeq1d 2612 |
. . . . 5
⊢ (𝑢 = (0g‘𝐺) → ((𝑢 ⊕ 𝐴) = 𝐴 ↔ ((0g‘𝐺) ⊕ 𝐴) = 𝐴)) |
14 | 13, 1 | elrab2 3333 |
. . . 4
⊢
((0g‘𝐺) ∈ 𝐻 ↔ ((0g‘𝐺) ∈ 𝑋 ∧ ((0g‘𝐺) ⊕ 𝐴) = 𝐴)) |
15 | 10, 11, 14 | sylanbrc 695 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (0g‘𝐺) ∈ 𝐻) |
16 | | ne0i 3880 |
. . 3
⊢
((0g‘𝐺) ∈ 𝐻 → 𝐻 ≠ ∅) |
17 | 15, 16 | syl 17 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ≠ ∅) |
18 | | simpll 786 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
19 | 18, 5 | syl 17 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → 𝐺 ∈ Grp) |
20 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → 𝑥 ∈ 𝐻) |
21 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑥 → (𝑢 ⊕ 𝐴) = (𝑥 ⊕ 𝐴)) |
22 | 21 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑥 → ((𝑢 ⊕ 𝐴) = 𝐴 ↔ (𝑥 ⊕ 𝐴) = 𝐴)) |
23 | 22, 1 | elrab2 3333 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐻 ↔ (𝑥 ∈ 𝑋 ∧ (𝑥 ⊕ 𝐴) = 𝐴)) |
24 | 20, 23 | sylib 207 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → (𝑥 ∈ 𝑋 ∧ (𝑥 ⊕ 𝐴) = 𝐴)) |
25 | 24 | simpld 474 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → 𝑥 ∈ 𝑋) |
26 | 25 | adantrr 749 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → 𝑥 ∈ 𝑋) |
27 | | simprr 792 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → 𝑦 ∈ 𝐻) |
28 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑦 → (𝑢 ⊕ 𝐴) = (𝑦 ⊕ 𝐴)) |
29 | 28 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑦 → ((𝑢 ⊕ 𝐴) = 𝐴 ↔ (𝑦 ⊕ 𝐴) = 𝐴)) |
30 | 29, 1 | elrab2 3333 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐻 ↔ (𝑦 ∈ 𝑋 ∧ (𝑦 ⊕ 𝐴) = 𝐴)) |
31 | 27, 30 | sylib 207 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑦 ∈ 𝑋 ∧ (𝑦 ⊕ 𝐴) = 𝐴)) |
32 | 31 | simpld 474 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → 𝑦 ∈ 𝑋) |
33 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
34 | 7, 33 | grpcl 17253 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(+g‘𝐺)𝑦) ∈ 𝑋) |
35 | 19, 26, 32, 34 | syl3anc 1318 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝑋) |
36 | | simplr 788 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → 𝐴 ∈ 𝑌) |
37 | 7, 33 | gaass 17553 |
. . . . . . . . 9
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌)) → ((𝑥(+g‘𝐺)𝑦) ⊕ 𝐴) = (𝑥 ⊕ (𝑦 ⊕ 𝐴))) |
38 | 18, 26, 32, 36, 37 | syl13anc 1320 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → ((𝑥(+g‘𝐺)𝑦) ⊕ 𝐴) = (𝑥 ⊕ (𝑦 ⊕ 𝐴))) |
39 | 31 | simprd 478 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑦 ⊕ 𝐴) = 𝐴) |
40 | 39 | oveq2d 6565 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ⊕ (𝑦 ⊕ 𝐴)) = (𝑥 ⊕ 𝐴)) |
41 | 24 | simprd 478 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → (𝑥 ⊕ 𝐴) = 𝐴) |
42 | 41 | adantrr 749 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ⊕ 𝐴) = 𝐴) |
43 | 38, 40, 42 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → ((𝑥(+g‘𝐺)𝑦) ⊕ 𝐴) = 𝐴) |
44 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑢 = (𝑥(+g‘𝐺)𝑦) → (𝑢 ⊕ 𝐴) = ((𝑥(+g‘𝐺)𝑦) ⊕ 𝐴)) |
45 | 44 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑢 = (𝑥(+g‘𝐺)𝑦) → ((𝑢 ⊕ 𝐴) = 𝐴 ↔ ((𝑥(+g‘𝐺)𝑦) ⊕ 𝐴) = 𝐴)) |
46 | 45, 1 | elrab2 3333 |
. . . . . . 7
⊢ ((𝑥(+g‘𝐺)𝑦) ∈ 𝐻 ↔ ((𝑥(+g‘𝐺)𝑦) ∈ 𝑋 ∧ ((𝑥(+g‘𝐺)𝑦) ⊕ 𝐴) = 𝐴)) |
47 | 35, 43, 46 | sylanbrc 695 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐻) |
48 | 47 | anassrs 678 |
. . . . 5
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) ∧ 𝑦 ∈ 𝐻) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐻) |
49 | 48 | ralrimiva 2949 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → ∀𝑦 ∈ 𝐻 (𝑥(+g‘𝐺)𝑦) ∈ 𝐻) |
50 | | simpll 786 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
51 | 50, 5 | syl 17 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → 𝐺 ∈ Grp) |
52 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
53 | 7, 52 | grpinvcl 17290 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ((invg‘𝐺)‘𝑥) ∈ 𝑋) |
54 | 51, 25, 53 | syl2anc 691 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → ((invg‘𝐺)‘𝑥) ∈ 𝑋) |
55 | | simplr 788 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → 𝐴 ∈ 𝑌) |
56 | 7, 52 | gacan 17561 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ∧ 𝐴 ∈ 𝑌)) → ((𝑥 ⊕ 𝐴) = 𝐴 ↔ (((invg‘𝐺)‘𝑥) ⊕ 𝐴) = 𝐴)) |
57 | 50, 25, 55, 55, 56 | syl13anc 1320 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → ((𝑥 ⊕ 𝐴) = 𝐴 ↔ (((invg‘𝐺)‘𝑥) ⊕ 𝐴) = 𝐴)) |
58 | 41, 57 | mpbid 221 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → (((invg‘𝐺)‘𝑥) ⊕ 𝐴) = 𝐴) |
59 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑢 = ((invg‘𝐺)‘𝑥) → (𝑢 ⊕ 𝐴) = (((invg‘𝐺)‘𝑥) ⊕ 𝐴)) |
60 | 59 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑢 = ((invg‘𝐺)‘𝑥) → ((𝑢 ⊕ 𝐴) = 𝐴 ↔ (((invg‘𝐺)‘𝑥) ⊕ 𝐴) = 𝐴)) |
61 | 60, 1 | elrab2 3333 |
. . . . 5
⊢
(((invg‘𝐺)‘𝑥) ∈ 𝐻 ↔ (((invg‘𝐺)‘𝑥) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥) ⊕ 𝐴) = 𝐴)) |
62 | 54, 58, 61 | sylanbrc 695 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → ((invg‘𝐺)‘𝑥) ∈ 𝐻) |
63 | 49, 62 | jca 553 |
. . 3
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑥 ∈ 𝐻) → (∀𝑦 ∈ 𝐻 (𝑥(+g‘𝐺)𝑦) ∈ 𝐻 ∧ ((invg‘𝐺)‘𝑥) ∈ 𝐻)) |
64 | 63 | ralrimiva 2949 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ∀𝑥 ∈ 𝐻 (∀𝑦 ∈ 𝐻 (𝑥(+g‘𝐺)𝑦) ∈ 𝐻 ∧ ((invg‘𝐺)‘𝑥) ∈ 𝐻)) |
65 | 7, 33, 52 | issubg2 17432 |
. . 3
⊢ (𝐺 ∈ Grp → (𝐻 ∈ (SubGrp‘𝐺) ↔ (𝐻 ⊆ 𝑋 ∧ 𝐻 ≠ ∅ ∧ ∀𝑥 ∈ 𝐻 (∀𝑦 ∈ 𝐻 (𝑥(+g‘𝐺)𝑦) ∈ 𝐻 ∧ ((invg‘𝐺)‘𝑥) ∈ 𝐻)))) |
66 | 6, 65 | syl 17 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (𝐻 ∈ (SubGrp‘𝐺) ↔ (𝐻 ⊆ 𝑋 ∧ 𝐻 ≠ ∅ ∧ ∀𝑥 ∈ 𝐻 (∀𝑦 ∈ 𝐻 (𝑥(+g‘𝐺)𝑦) ∈ 𝐻 ∧ ((invg‘𝐺)‘𝑥) ∈ 𝐻)))) |
67 | 4, 17, 64, 66 | mpbir3and 1238 |
1
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺)) |