Metamath Proof Explorer

Theorem subgnm

Description: The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses subgngp.h ⊢H=G↾𝑠A
subgnm.n ⊢N=norm⁡G
subgnm.m ⊢M=norm⁡H
Assertion subgnm ⊢A∈SubGrp⁡G→M=N↾A

Proof

Step Hyp Ref Expression
1 subgngp.h ⊢H=G↾𝑠A
2 subgnm.n ⊢N=norm⁡G
3 subgnm.m ⊢M=norm⁡H
4 eqid ⊢BaseG=BaseG
5 4 subgss ⊢A∈SubGrp⁡G→A⊆BaseG
6 5 resmptd ⊢A∈SubGrp⁡G→x∈BaseG⟼xdist⁡G0G↾A=x∈A⟼xdist⁡G0G
7 1 subgbas ⊢A∈SubGrp⁡G→A=BaseH
8 eqid ⊢dist⁡G=dist⁡G
9 1 8 ressds ⊢A∈SubGrp⁡G→dist⁡G=dist⁡H
10 eqidd ⊢A∈SubGrp⁡G→x=x
11 eqid ⊢0G=0G
12 1 11 subg0 ⊢A∈SubGrp⁡G→0G=0H
13 9 10 12 oveq123d ⊢A∈SubGrp⁡G→xdist⁡G0G=xdist⁡H0H
14 7 13 mpteq12dv ⊢A∈SubGrp⁡G→x∈A⟼xdist⁡G0G=x∈BaseH⟼xdist⁡H0H
15 6 14 eqtr2d ⊢A∈SubGrp⁡G→x∈BaseH⟼xdist⁡H0H=x∈BaseG⟼xdist⁡G0G↾A
16 eqid ⊢BaseH=BaseH
17 eqid ⊢0H=0H
18 eqid ⊢dist⁡H=dist⁡H
19 3 16 17 18 nmfval ⊢M=x∈BaseH⟼xdist⁡H0H
20 2 4 11 8 nmfval ⊢N=x∈BaseG⟼xdist⁡G0G
21 20 reseq1i ⊢N↾A=x∈BaseG⟼xdist⁡G0G↾A
22 15 19 21 3eqtr4g ⊢A∈SubGrp⁡G→M=N↾A