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 | ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 ) | |
subgnm.n | ⊢ 𝑁 = ( norm ‘ 𝐺 ) | ||
subgnm.m | ⊢ 𝑀 = ( norm ‘ 𝐻 ) | ||
Assertion | subgnm2 | ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑋 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subgngp.h | ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 ) | |
2 | subgnm.n | ⊢ 𝑁 = ( norm ‘ 𝐺 ) | |
3 | subgnm.m | ⊢ 𝑀 = ( norm ‘ 𝐻 ) | |
4 | 1 2 3 | subgnm | ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝑀 = ( 𝑁 ↾ 𝐴 ) ) |
5 | 4 | fveq1d | ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑀 ‘ 𝑋 ) = ( ( 𝑁 ↾ 𝐴 ) ‘ 𝑋 ) ) |
6 | fvres | ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝑁 ↾ 𝐴 ) ‘ 𝑋 ) = ( 𝑁 ‘ 𝑋 ) ) | |
7 | 5 6 | sylan9eq | ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑋 ) ) |