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 𝐻 = ( 𝐺s 𝐴 )
subgnm.n 𝑁 = ( norm ‘ 𝐺 )
subgnm.m 𝑀 = ( norm ‘ 𝐻 )
Assertion subgnm2 ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → ( 𝑀𝑋 ) = ( 𝑁𝑋 ) )

Proof

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 ‘ 𝐺 ) ∧ 𝑋𝐴 ) → ( 𝑀𝑋 ) = ( 𝑁𝑋 ) )