Step |
Hyp |
Ref |
Expression |
1 |
|
grpissubg.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
grpissubg.s |
⊢ 𝑆 = ( Base ‘ 𝐻 ) |
3 |
|
simpl |
⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ⊆ 𝐵 ) |
4 |
3
|
adantl |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ⊆ 𝐵 ) |
5 |
2
|
grpbn0 |
⊢ ( 𝐻 ∈ Grp → 𝑆 ≠ ∅ ) |
6 |
5
|
ad2antlr |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ≠ ∅ ) |
7 |
|
grpmnd |
⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd ) |
8 |
|
mndmgm |
⊢ ( 𝐺 ∈ Mnd → 𝐺 ∈ Mgm ) |
9 |
7 8
|
syl |
⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mgm ) |
10 |
|
grpmnd |
⊢ ( 𝐻 ∈ Grp → 𝐻 ∈ Mnd ) |
11 |
|
mndmgm |
⊢ ( 𝐻 ∈ Mnd → 𝐻 ∈ Mgm ) |
12 |
10 11
|
syl |
⊢ ( 𝐻 ∈ Grp → 𝐻 ∈ Mgm ) |
13 |
9 12
|
anim12i |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ) |
14 |
13
|
adantr |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ) |
15 |
14
|
ad2antrr |
⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝑆 ) → ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ) |
16 |
|
simpr |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) |
17 |
16
|
ad2antrr |
⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝑆 ) → ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) |
18 |
|
simpr |
⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝑆 ) |
19 |
18
|
anim1i |
⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) |
20 |
1 2
|
mgmsscl |
⊢ ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ) |
21 |
15 17 19 20
|
syl3anc |
⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ) |
22 |
21
|
ralrimiva |
⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ) |
23 |
|
simpl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → 𝐺 ∈ Grp ) |
24 |
23
|
adantr |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝐺 ∈ Grp ) |
25 |
|
simplr |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝐻 ∈ Grp ) |
26 |
1
|
sseq2i |
⊢ ( 𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
27 |
26
|
biimpi |
⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
28 |
27
|
adantr |
⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
29 |
28
|
adantl |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
30 |
|
ovres |
⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) |
31 |
30
|
adantl |
⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) |
32 |
|
oveq |
⊢ ( ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ) |
33 |
32
|
adantl |
⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) ) |
34 |
33
|
eqcomd |
⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) |
35 |
34
|
ad2antlr |
⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) |
36 |
31 35
|
eqtr3d |
⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) |
37 |
36
|
ralrimivva |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) |
38 |
24 25 2 29 37
|
grpinvssd |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝑎 ∈ 𝑆 → ( ( invg ‘ 𝐻 ) ‘ 𝑎 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ) ) |
39 |
38
|
imp |
⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → ( ( invg ‘ 𝐻 ) ‘ 𝑎 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ) |
40 |
|
eqid |
⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 ) |
41 |
2 40
|
grpinvcl |
⊢ ( ( 𝐻 ∈ Grp ∧ 𝑎 ∈ 𝑆 ) → ( ( invg ‘ 𝐻 ) ‘ 𝑎 ) ∈ 𝑆 ) |
42 |
41
|
ad4ant24 |
⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → ( ( invg ‘ 𝐻 ) ‘ 𝑎 ) ∈ 𝑆 ) |
43 |
39 42
|
eqeltrrd |
⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) |
44 |
22 43
|
jca |
⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → ( ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) |
45 |
44
|
ralrimiva |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ∀ 𝑎 ∈ 𝑆 ( ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) |
46 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
47 |
|
eqid |
⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 ) |
48 |
1 46 47
|
issubg2 |
⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝑆 ( ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) ) ) |
49 |
48
|
ad2antrr |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝑆 ( ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) ) ) |
50 |
4 6 45 49
|
mpbir3and |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |
51 |
50
|
ex |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ) |