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 ⊢ Base G = Base G
5 4 subgss ⊢ A ∈ SubGrp ⁡ G → A ⊆ Base G
6 5 resmptd ⊢ A ∈ SubGrp ⁡ G → x ∈ Base G ⟼ x dist ⁡ G 0 G ↾ A = x ∈ A ⟼ x dist ⁡ G 0 G
7 1 subgbas ⊢ A ∈ SubGrp ⁡ G → A = Base H
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 ⊢ 0 G = 0 G
12 1 11 subg0 ⊢ A ∈ SubGrp ⁡ G → 0 G = 0 H
13 9 10 12 oveq123d ⊢ A ∈ SubGrp ⁡ G → x dist ⁡ G 0 G = x dist ⁡ H 0 H
14 7 13 mpteq12dv ⊢ A ∈ SubGrp ⁡ G → x ∈ A ⟼ x dist ⁡ G 0 G = x ∈ Base H ⟼ x dist ⁡ H 0 H
15 6 14 eqtr2d ⊢ A ∈ SubGrp ⁡ G → x ∈ Base H ⟼ x dist ⁡ H 0 H = x ∈ Base G ⟼ x dist ⁡ G 0 G ↾ A
16 eqid ⊢ Base H = Base H
17 eqid ⊢ 0 H = 0 H
18 eqid ⊢ dist ⁡ H = dist ⁡ H
19 3 16 17 18 nmfval ⊢ M = x ∈ Base H ⟼ x dist ⁡ H 0 H
20 2 4 11 8 nmfval ⊢ N = x ∈ Base G ⟼ x dist ⁡ G 0 G
21 20 reseq1i ⊢ N ↾ A = x ∈ Base G ⟼ x dist ⁡ G 0 G ↾ A
22 15 19 21 3eqtr4g ⊢ A ∈ SubGrp ⁡ G → M = N ↾ A