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{\upharpoonright }_{𝑠}A$$
	subgnm.n	$$⊢N=\mathrm{norm}\left(G\right)$$
	subgnm.m	$$⊢M=\mathrm{norm}\left(H\right)$$
Assertion	subgnm2	$$⊢\left(A\in \mathrm{SubGrp}\left(G\right)\wedge X\in A\right)\to M\left(X\right)=N\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		subgngp.h	$$⊢H=G{\upharpoonright }_{𝑠}A$$
2		subgnm.n	$$⊢N=\mathrm{norm}\left(G\right)$$
3		subgnm.m	$$⊢M=\mathrm{norm}\left(H\right)$$
4	1 2 3	subgnm	$$⊢A\in \mathrm{SubGrp}\left(G\right)\to M={N\upharpoonright }_A$$
5	4	fveq1d	$$⊢A\in \mathrm{SubGrp}\left(G\right)\to M\left(X\right)=\left({N\upharpoonright }_A\right)\left(X\right)$$
6		fvres	$$⊢X\in A\to \left({N\upharpoonright }_A\right)\left(X\right)=N\left(X\right)$$
7	5 6	sylan9eq	$$⊢\left(A\in \mathrm{SubGrp}\left(G\right)\wedge X\in A\right)\to M\left(X\right)=N\left(X\right)$$