Theorem subgnm

Description: The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	subgngp.h	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
	subgnm.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
	subgnm.m	⊢ 𝑀 = ( norm ‘ 𝐻 )
Assertion	subgnm	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝑀 = ( 𝑁 ↾ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		subgngp.h	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2		subgnm.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
3		subgnm.m	⊢ 𝑀 = ( norm ‘ 𝐻 )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5	4	subgss	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
6	5	resmptd	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) )
7	1	subgbas	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐴 = ( Base ‘ 𝐻 ) )
8		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
9	1 8	ressds	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( dist ‘ 𝐺 ) = ( dist ‘ 𝐻 ) )
10		eqidd	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥 = 𝑥 )
11		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
12	1 11	subg0	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
13	9 10 12	oveq123d	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( 𝑥 ( dist ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) )
14	7 13	mpteq12dv	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( dist ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) ) )
15	6 14	eqtr2d	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( dist ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) ↾ 𝐴 ) )
16		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
17		eqid	⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
18		eqid	⊢ ( dist ‘ 𝐻 ) = ( dist ‘ 𝐻 )
19	3 16 17 18	nmfval	⊢ 𝑀 = ( 𝑥 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( dist ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) )
20	2 4 11 8	nmfval	⊢ 𝑁 = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
21	20	reseq1i	⊢ ( 𝑁 ↾ 𝐴 ) = ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) ↾ 𝐴 )
22	15 19 21	3eqtr4g	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝑀 = ( 𝑁 ↾ 𝐴 ) )