Step |
Hyp |
Ref |
Expression |
1 |
|
cntrnsg.z |
⊢ 𝑍 = ( Cntr ‘ 𝑀 ) |
2 |
|
simpl |
⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) → 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ) |
3 |
|
simplr |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → 𝑋 ⊆ 𝑍 ) |
4 |
|
simprr |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 ) |
5 |
3 4
|
sseldd |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑍 ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
7 |
|
eqid |
⊢ ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 ) |
8 |
6 7
|
cntrval |
⊢ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) = ( Cntr ‘ 𝑀 ) |
9 |
8 1
|
eqtr4i |
⊢ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) = 𝑍 |
10 |
5 9
|
eleqtrrdi |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ) |
11 |
|
simprl |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) ) |
12 |
|
eqid |
⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 ) |
13 |
12 7
|
cntzi |
⊢ ( ( 𝑦 ∈ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) |
14 |
10 11 13
|
syl2anc |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) |
15 |
14
|
oveq1d |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( -g ‘ 𝑀 ) 𝑥 ) = ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( -g ‘ 𝑀 ) 𝑥 ) ) |
16 |
|
subgrcl |
⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) → 𝑀 ∈ Grp ) |
17 |
16
|
ad2antrr |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → 𝑀 ∈ Grp ) |
18 |
6
|
subgss |
⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) ) |
19 |
18
|
ad2antrr |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) ) |
20 |
19 4
|
sseldd |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ ( Base ‘ 𝑀 ) ) |
21 |
|
eqid |
⊢ ( -g ‘ 𝑀 ) = ( -g ‘ 𝑀 ) |
22 |
6 12 21
|
grppncan |
⊢ ( ( 𝑀 ∈ Grp ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( -g ‘ 𝑀 ) 𝑥 ) = 𝑦 ) |
23 |
17 20 11 22
|
syl3anc |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( -g ‘ 𝑀 ) 𝑥 ) = 𝑦 ) |
24 |
15 23
|
eqtr3d |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( -g ‘ 𝑀 ) 𝑥 ) = 𝑦 ) |
25 |
24 4
|
eqeltrd |
⊢ ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( -g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 ) |
26 |
25
|
ralrimivva |
⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( -g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 ) |
27 |
6 12 21
|
isnsg3 |
⊢ ( 𝑋 ∈ ( NrmSGrp ‘ 𝑀 ) ↔ ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( -g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 ) ) |
28 |
2 26 27
|
sylanbrc |
⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋 ⊆ 𝑍 ) → 𝑋 ∈ ( NrmSGrp ‘ 𝑀 ) ) |