Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . 4
⊢ ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ⊆ 𝐵) |
2 | 1 | adantl 481 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆 ⊆ 𝐵) |
3 | | grpissubg.s |
. . . . 5
⊢ 𝑆 = (Base‘𝐻) |
4 | 3 | grpbn0 17274 |
. . . 4
⊢ (𝐻 ∈ Grp → 𝑆 ≠ ∅) |
5 | 4 | ad2antlr 759 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆 ≠ ∅) |
6 | | ovres 6698 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑏) = (𝑎(+g‘𝐺)𝑏)) |
7 | 6 | adantll 746 |
. . . . . . 7
⊢
(((((𝐺 ∈ Grp
∧ 𝐻 ∈ Grp) ∧
(𝑆 ⊆ 𝐵 ∧
(+g‘𝐻) =
((+g‘𝐺)
↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → (𝑎((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑏) = (𝑎(+g‘𝐺)𝑏)) |
8 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → 𝐻 ∈ Grp) |
9 | 8 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝐺 ∈ Grp
∧ 𝐻 ∈ Grp) ∧
(𝑆 ⊆ 𝐵 ∧
(+g‘𝐻) =
((+g‘𝐺)
↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → 𝐻 ∈ Grp) |
10 | | simplr 788 |
. . . . . . . . 9
⊢
(((((𝐺 ∈ Grp
∧ 𝐻 ∈ Grp) ∧
(𝑆 ⊆ 𝐵 ∧
(+g‘𝐻) =
((+g‘𝐺)
↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
11 | | simpr 476 |
. . . . . . . . 9
⊢
(((((𝐺 ∈ Grp
∧ 𝐻 ∈ Grp) ∧
(𝑆 ⊆ 𝐵 ∧
(+g‘𝐻) =
((+g‘𝐺)
↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → 𝑏 ∈ 𝑆) |
12 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+g‘𝐻) = (+g‘𝐻) |
13 | 3, 12 | grpcl 17253 |
. . . . . . . . 9
⊢ ((𝐻 ∈ Grp ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎(+g‘𝐻)𝑏) ∈ 𝑆) |
14 | 9, 10, 11, 13 | syl3anc 1318 |
. . . . . . . 8
⊢
(((((𝐺 ∈ Grp
∧ 𝐻 ∈ Grp) ∧
(𝑆 ⊆ 𝐵 ∧
(+g‘𝐻) =
((+g‘𝐺)
↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → (𝑎(+g‘𝐻)𝑏) ∈ 𝑆) |
15 | | oveq 6555 |
. . . . . . . . . . . . 13
⊢
((+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)) → (𝑎(+g‘𝐻)𝑏) = (𝑎((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑏)) |
16 | 15 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢
((+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)) → (𝑎((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑏) = (𝑎(+g‘𝐻)𝑏)) |
17 | 16 | eleq1d 2672 |
. . . . . . . . . . 11
⊢
((+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)) → ((𝑎((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑏) ∈ 𝑆 ↔ (𝑎(+g‘𝐻)𝑏) ∈ 𝑆)) |
18 | 17 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → ((𝑎((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑏) ∈ 𝑆 ↔ (𝑎(+g‘𝐻)𝑏) ∈ 𝑆)) |
19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → ((𝑎((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑏) ∈ 𝑆 ↔ (𝑎(+g‘𝐻)𝑏) ∈ 𝑆)) |
20 | 19 | ad2antrr 758 |
. . . . . . . 8
⊢
(((((𝐺 ∈ Grp
∧ 𝐻 ∈ Grp) ∧
(𝑆 ⊆ 𝐵 ∧
(+g‘𝐻) =
((+g‘𝐺)
↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → ((𝑎((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑏) ∈ 𝑆 ↔ (𝑎(+g‘𝐻)𝑏) ∈ 𝑆)) |
21 | 14, 20 | mpbird 246 |
. . . . . . 7
⊢
(((((𝐺 ∈ Grp
∧ 𝐻 ∈ Grp) ∧
(𝑆 ⊆ 𝐵 ∧
(+g‘𝐻) =
((+g‘𝐺)
↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → (𝑎((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑏) ∈ 𝑆) |
22 | 7, 21 | eqeltrrd 2689 |
. . . . . 6
⊢
(((((𝐺 ∈ Grp
∧ 𝐻 ∈ Grp) ∧
(𝑆 ⊆ 𝐵 ∧
(+g‘𝐻) =
((+g‘𝐺)
↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → (𝑎(+g‘𝐺)𝑏) ∈ 𝑆) |
23 | 22 | ralrimiva 2949 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) → ∀𝑏 ∈ 𝑆 (𝑎(+g‘𝐺)𝑏) ∈ 𝑆) |
24 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → 𝐺 ∈ Grp) |
25 | 24 | adantr 480 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → 𝐺 ∈ Grp) |
26 | | grpissubg.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐺) |
27 | 26 | sseq2i 3593 |
. . . . . . . . . . 11
⊢ (𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ (Base‘𝐺)) |
28 | 27 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝐵 → 𝑆 ⊆ (Base‘𝐺)) |
29 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ⊆ (Base‘𝐺)) |
30 | 29 | adantl 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆 ⊆ (Base‘𝐺)) |
31 | | ovres 6698 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑦) = (𝑥(+g‘𝐺)𝑦)) |
32 | 31 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑦) = (𝑥(+g‘𝐺)𝑦)) |
33 | | oveq 6555 |
. . . . . . . . . . . . 13
⊢
((+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)) → (𝑥(+g‘𝐻)𝑦) = (𝑥((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑦)) |
34 | 33 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → (𝑥(+g‘𝐻)𝑦) = (𝑥((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑦)) |
35 | 34 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → (𝑥((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑦) = (𝑥(+g‘𝐻)𝑦)) |
36 | 35 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥((+g‘𝐺) ↾ (𝑆 × 𝑆))𝑦) = (𝑥(+g‘𝐻)𝑦)) |
37 | 32, 36 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
38 | 37 | ralrimivva 2954 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
39 | 25, 8, 3, 30, 38 | grpinvssd 17315 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → (𝑎 ∈ 𝑆 → ((invg‘𝐻)‘𝑎) = ((invg‘𝐺)‘𝑎))) |
40 | 39 | imp 444 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) → ((invg‘𝐻)‘𝑎) = ((invg‘𝐺)‘𝑎)) |
41 | | eqid 2610 |
. . . . . . . . . 10
⊢
(invg‘𝐻) = (invg‘𝐻) |
42 | 3, 41 | grpinvcl 17290 |
. . . . . . . . 9
⊢ ((𝐻 ∈ Grp ∧ 𝑎 ∈ 𝑆) → ((invg‘𝐻)‘𝑎) ∈ 𝑆) |
43 | 42 | ex 449 |
. . . . . . . 8
⊢ (𝐻 ∈ Grp → (𝑎 ∈ 𝑆 → ((invg‘𝐻)‘𝑎) ∈ 𝑆)) |
44 | 43 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → (𝑎 ∈ 𝑆 → ((invg‘𝐻)‘𝑎) ∈ 𝑆)) |
45 | 44 | imp 444 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) → ((invg‘𝐻)‘𝑎) ∈ 𝑆) |
46 | 40, 45 | eqeltrrd 2689 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) → ((invg‘𝐺)‘𝑎) ∈ 𝑆) |
47 | 23, 46 | jca 553 |
. . . 4
⊢ ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎 ∈ 𝑆) → (∀𝑏 ∈ 𝑆 (𝑎(+g‘𝐺)𝑏) ∈ 𝑆 ∧ ((invg‘𝐺)‘𝑎) ∈ 𝑆)) |
48 | 47 | ralrimiva 2949 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → ∀𝑎 ∈ 𝑆 (∀𝑏 ∈ 𝑆 (𝑎(+g‘𝐺)𝑏) ∈ 𝑆 ∧ ((invg‘𝐺)‘𝑎) ∈ 𝑆)) |
49 | | eqid 2610 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
50 | | eqid 2610 |
. . . . 5
⊢
(invg‘𝐺) = (invg‘𝐺) |
51 | 26, 49, 50 | issubg2 17432 |
. . . 4
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑎 ∈ 𝑆 (∀𝑏 ∈ 𝑆 (𝑎(+g‘𝐺)𝑏) ∈ 𝑆 ∧ ((invg‘𝐺)‘𝑎) ∈ 𝑆)))) |
52 | 51 | ad2antrr 758 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑎 ∈ 𝑆 (∀𝑏 ∈ 𝑆 (𝑎(+g‘𝐺)𝑏) ∈ 𝑆 ∧ ((invg‘𝐺)‘𝑎) ∈ 𝑆)))) |
53 | 2, 5, 48, 52 | mpbir3and 1238 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆 ∈ (SubGrp‘𝐺)) |
54 | 53 | ex 449 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubGrp‘𝐺))) |