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 |`s A )
	subgnm.n	|- N = ( norm ` G )
	subgnm.m	|- M = ( norm ` H )
Assertion	subgnm2	|- ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> ( M ` X ) = ( N ` X ) )

Proof

Step	Hyp	Ref	Expression
1		subgngp.h	|- H = ( G |`s A )
2		subgnm.n	|- N = ( norm ` G )
3		subgnm.m	|- M = ( norm ` H )
4	1 2 3	subgnm	|- ( A e. ( SubGrp ` G ) -> M = ( N |` A ) )
5	4	fveq1d	|- ( A e. ( SubGrp ` G ) -> ( M ` X ) = ( ( N |` A ) ` X ) )
6		fvres	|- ( X e. A -> ( ( N |` A ) ` X ) = ( N ` X ) )
7	5 6	sylan9eq	|- ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> ( M ` X ) = ( N ` X ) )