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