Metamath Proof Explorer

Theorem ressnm

Description: The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses ressnm.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
ressnm.2 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ressnm.3 ⊢ 0 = ( 0g ‘ 𝐺 )
ressnm.4 ⊢ 𝑁 = ( norm ‘ 𝐺 )
Assertion ressnm ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑁 ↾ 𝐴 ) = ( norm ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 ressnm.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2 ressnm.2 ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 ressnm.3 ⊢ 0 = ( 0g ‘ 𝐺 )
4 ressnm.4 ⊢ 𝑁 = ( norm ‘ 𝐺 )
5 1 2 ressbas2 ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ 𝐻 ) )
6 5 3ad2ant3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 = ( Base ‘ 𝐻 ) )
7 2 fvexi ⊢ 𝐵 ∈ V
8 7 ssex ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ V )
9 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
10 1 9 ressds ⊢ ( 𝐴 ∈ V → ( dist ‘ 𝐺 ) = ( dist ‘ 𝐻 ) )
11 8 10 syl ⊢ ( 𝐴 ⊆ 𝐵 → ( dist ‘ 𝐺 ) = ( dist ‘ 𝐻 ) )
12 11 3ad2ant3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( dist ‘ 𝐺 ) = ( dist ‘ 𝐻 ) )
13 eqidd ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝑥 = 𝑥 )
14 1 2 3 ress0g ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 0 = ( 0g ‘ 𝐻 ) )
15 12 13 14 oveq123d ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ( dist ‘ 𝐺 ) 0 ) = ( 𝑥 ( dist ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) )
16 6 15 mpteq12dv ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 ( dist ‘ 𝐺 ) 0 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( dist ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) ) )
17 4 2 3 9 nmfval ⊢ 𝑁 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ( dist ‘ 𝐺 ) 0 ) )
18 17 reseq1i ⊢ ( 𝑁 ↾ 𝐴 ) = ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ( dist ‘ 𝐺 ) 0 ) ) ↾ 𝐴 )
19 resmpt ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ( dist ‘ 𝐺 ) 0 ) ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 ( dist ‘ 𝐺 ) 0 ) ) )
20 18 19 eqtrid ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑁 ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 ( dist ‘ 𝐺 ) 0 ) ) )
21 20 3ad2ant3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑁 ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 ( dist ‘ 𝐺 ) 0 ) ) )
22 eqid ⊢ ( norm ‘ 𝐻 ) = ( norm ‘ 𝐻 )
23 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
24 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
25 eqid ⊢ ( dist ‘ 𝐻 ) = ( dist ‘ 𝐻 )
26 22 23 24 25 nmfval ⊢ ( norm ‘ 𝐻 ) = ( 𝑥 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( dist ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) )
27 26 a1i ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( norm ‘ 𝐻 ) = ( 𝑥 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( dist ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) ) )
28 16 21 27 3eqtr4d ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑁 ↾ 𝐴 ) = ( norm ‘ 𝐻 ) )