Step |
Hyp |
Ref |
Expression |
1 |
|
subgacs.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
1
|
subgss |
⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → 𝑠 ⊆ 𝐵 ) |
3 |
|
velpw |
⊢ ( 𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵 ) |
4 |
2 3
|
sylibr |
⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → 𝑠 ∈ 𝒫 𝐵 ) |
5 |
|
eleq2w |
⊢ ( 𝑧 = 𝑠 → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) ) |
6 |
5
|
raleqbi1dv |
⊢ ( 𝑧 = 𝑠 → ( ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) ) |
7 |
6
|
ralbidv |
⊢ ( 𝑧 = 𝑠 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) ) |
8 |
7
|
elrab3 |
⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) ) |
9 |
4 8
|
syl |
⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) ) |
10 |
9
|
bicomd |
⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ↔ 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ) |
11 |
10
|
pm5.32i |
⊢ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ) |
12 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
13 |
|
eqid |
⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 ) |
14 |
1 12 13
|
isnsg3 |
⊢ ( 𝑠 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) ) |
15 |
|
elin |
⊢ ( 𝑠 ∈ ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ) |
16 |
11 14 15
|
3bitr4i |
⊢ ( 𝑠 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ 𝑠 ∈ ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ) |
17 |
16
|
eqriv |
⊢ ( NrmSGrp ‘ 𝐺 ) = ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) |
18 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
19 |
|
mreacs |
⊢ ( 𝐵 ∈ V → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ) |
20 |
18 19
|
mp1i |
⊢ ( 𝐺 ∈ Grp → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ) |
21 |
1
|
subgacs |
⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) ) |
22 |
|
simpl |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐺 ∈ Grp ) |
23 |
1 12
|
grpcl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 ) |
24 |
23
|
3expb |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 ) |
25 |
|
simprl |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 ) |
26 |
1 13
|
grpsubcl |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 ) |
27 |
22 24 25 26
|
syl3anc |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 ) |
28 |
27
|
ralrimivva |
⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 ) |
29 |
|
acsfn1c |
⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 ) → { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ∈ ( ACS ‘ 𝐵 ) ) |
30 |
18 28 29
|
sylancr |
⊢ ( 𝐺 ∈ Grp → { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ∈ ( ACS ‘ 𝐵 ) ) |
31 |
|
mreincl |
⊢ ( ( ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ∧ ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ∈ ( ACS ‘ 𝐵 ) ) → ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ∈ ( ACS ‘ 𝐵 ) ) |
32 |
20 21 30 31
|
syl3anc |
⊢ ( 𝐺 ∈ Grp → ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ∈ ( ACS ‘ 𝐵 ) ) |
33 |
17 32
|
eqeltrid |
⊢ ( 𝐺 ∈ Grp → ( NrmSGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) ) |