This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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