Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. 2
⊢ ((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) → 𝑋 ∈ (SubGrp‘𝑀)) |
2 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → 𝑋 ⊆ 𝑍) |
3 | | simprr 796 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
4 | 2, 3 | sseldd 3604 |
. . . . . . . 8
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑍) |
5 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Base‘𝑀) =
(Base‘𝑀) |
6 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Cntz‘𝑀) =
(Cntz‘𝑀) |
7 | 5, 6 | cntrval 17752 |
. . . . . . . . 9
⊢
((Cntz‘𝑀)‘(Base‘𝑀)) = (Cntr‘𝑀) |
8 | | cntrnsg.z |
. . . . . . . . 9
⊢ 𝑍 = (Cntr‘𝑀) |
9 | 7, 8 | eqtr4i 2647 |
. . . . . . . 8
⊢
((Cntz‘𝑀)‘(Base‘𝑀)) = 𝑍 |
10 | 4, 9 | syl6eleqr 2712 |
. . . . . . 7
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ((Cntz‘𝑀)‘(Base‘𝑀))) |
11 | | simprl 794 |
. . . . . . 7
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ (Base‘𝑀)) |
12 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘𝑀) = (+g‘𝑀) |
13 | 12, 6 | cntzi 17762 |
. . . . . . 7
⊢ ((𝑦 ∈ ((Cntz‘𝑀)‘(Base‘𝑀)) ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑦(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)𝑦)) |
14 | 10, 11, 13 | syl2anc 693 |
. . . . . 6
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → (𝑦(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)𝑦)) |
15 | 14 | oveq1d 6665 |
. . . . 5
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → ((𝑦(+g‘𝑀)𝑥)(-g‘𝑀)𝑥) = ((𝑥(+g‘𝑀)𝑦)(-g‘𝑀)𝑥)) |
16 | | subgrcl 17599 |
. . . . . . 7
⊢ (𝑋 ∈ (SubGrp‘𝑀) → 𝑀 ∈ Grp) |
17 | 16 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → 𝑀 ∈ Grp) |
18 | 5 | subgss 17595 |
. . . . . . . 8
⊢ (𝑋 ∈ (SubGrp‘𝑀) → 𝑋 ⊆ (Base‘𝑀)) |
19 | 18 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝑀)) |
20 | 19, 3 | sseldd 3604 |
. . . . . 6
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ (Base‘𝑀)) |
21 | | eqid 2622 |
. . . . . . 7
⊢
(-g‘𝑀) = (-g‘𝑀) |
22 | 5, 12, 21 | grppncan 17506 |
. . . . . 6
⊢ ((𝑀 ∈ Grp ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝑦(+g‘𝑀)𝑥)(-g‘𝑀)𝑥) = 𝑦) |
23 | 17, 20, 11, 22 | syl3anc 1326 |
. . . . 5
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → ((𝑦(+g‘𝑀)𝑥)(-g‘𝑀)𝑥) = 𝑦) |
24 | 15, 23 | eqtr3d 2658 |
. . . 4
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → ((𝑥(+g‘𝑀)𝑦)(-g‘𝑀)𝑥) = 𝑦) |
25 | 24, 3 | eqeltrd 2701 |
. . 3
⊢ (((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ 𝑋)) → ((𝑥(+g‘𝑀)𝑦)(-g‘𝑀)𝑥) ∈ 𝑋) |
26 | 25 | ralrimivva 2971 |
. 2
⊢ ((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) → ∀𝑥 ∈ (Base‘𝑀)∀𝑦 ∈ 𝑋 ((𝑥(+g‘𝑀)𝑦)(-g‘𝑀)𝑥) ∈ 𝑋) |
27 | 5, 12, 21 | isnsg3 17628 |
. 2
⊢ (𝑋 ∈ (NrmSGrp‘𝑀) ↔ (𝑋 ∈ (SubGrp‘𝑀) ∧ ∀𝑥 ∈ (Base‘𝑀)∀𝑦 ∈ 𝑋 ((𝑥(+g‘𝑀)𝑦)(-g‘𝑀)𝑥) ∈ 𝑋)) |
28 | 1, 26, 27 | sylanbrc 698 |
1
⊢ ((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) → 𝑋 ∈ (NrmSGrp‘𝑀)) |