This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subgnm2

Description: A substructure assigns the same values to the norms of elements of 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 subgnm2 ⊢ A ∈ SubGrp ⁡ G ∧ X ∈ A → M ⁡ X = N ⁡ X

Proof

Step Hyp Ref Expression
1 subgngp.h ⊢ H = G ↾ 𝑠 A
2 subgnm.n ⊢ N = norm ⁡ G
3 subgnm.m ⊢ M = norm ⁡ H
4 1 2 3 subgnm ⊢ A ∈ SubGrp ⁡ G → M = N ↾ A
5 4 fveq1d ⊢ A ∈ SubGrp ⁡ G → M ⁡ X = N ↾ A ⁡ X
6 fvres ⊢ X ∈ A → N ↾ A ⁡ X = N ⁡ X
7 5 6 sylan9eq ⊢ A ∈ SubGrp ⁡ G ∧ X ∈ A → M ⁡ X = N ⁡ X