Metamath Proof Explorer

Theorem ressnm

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

Ref Expression
Hypotheses ressnm.1 ⊢ H = G ↾ 𝑠 A
ressnm.2 ⊢ B = Base G
ressnm.3 ⊢ 0 ˙ = 0 G
ressnm.4 ⊢ N = norm ⁡ G
Assertion ressnm ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → N ↾ A = norm ⁡ H

Proof

Step Hyp Ref Expression
1 ressnm.1 ⊢ H = G ↾ 𝑠 A
2 ressnm.2 ⊢ B = Base G
3 ressnm.3 ⊢ 0 ˙ = 0 G
4 ressnm.4 ⊢ N = norm ⁡ G
5 1 2 ressbas2 ⊢ A ⊆ B → A = Base H
6 5 3ad2ant3 ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → A = Base H
7 2 fvexi ⊢ B ∈ V
8 7 ssex ⊢ A ⊆ B → A ∈ V
9 eqid ⊢ dist ⁡ G = dist ⁡ G
10 1 9 ressds ⊢ A ∈ V → dist ⁡ G = dist ⁡ H
11 8 10 syl ⊢ A ⊆ B → dist ⁡ G = dist ⁡ H
12 11 3ad2ant3 ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → dist ⁡ G = dist ⁡ H
13 eqidd ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → x = x
14 1 2 3 ress0g ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → 0 ˙ = 0 H
15 12 13 14 oveq123d ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → x dist ⁡ G 0 ˙ = x dist ⁡ H 0 H
16 6 15 mpteq12dv ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → x ∈ A ⟼ x dist ⁡ G 0 ˙ = x ∈ Base H ⟼ x dist ⁡ H 0 H
17 4 2 3 9 nmfval ⊢ N = x ∈ B ⟼ x dist ⁡ G 0 ˙
18 17 reseq1i ⊢ N ↾ A = x ∈ B ⟼ x dist ⁡ G 0 ˙ ↾ A
19 resmpt ⊢ A ⊆ B → x ∈ B ⟼ x dist ⁡ G 0 ˙ ↾ A = x ∈ A ⟼ x dist ⁡ G 0 ˙
20 18 19 syl5eq ⊢ A ⊆ B → N ↾ A = x ∈ A ⟼ x dist ⁡ G 0 ˙
21 20 3ad2ant3 ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → N ↾ A = x ∈ A ⟼ x dist ⁡ G 0 ˙
22 eqid ⊢ norm ⁡ H = norm ⁡ H
23 eqid ⊢ Base H = Base H
24 eqid ⊢ 0 H = 0 H
25 eqid ⊢ dist ⁡ H = dist ⁡ H
26 22 23 24 25 nmfval ⊢ norm ⁡ H = x ∈ Base H ⟼ x dist ⁡ H 0 H
27 26 a1i ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → norm ⁡ H = x ∈ Base H ⟼ x dist ⁡ H 0 H
28 16 21 27 3eqtr4d ⊢ G ∈ Mnd ∧ 0 ˙ ∈ A ∧ A ⊆ B → N ↾ A = norm ⁡ H