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	$⊢ \underset{˙}{0} = 0_{G}$
	ressnm.4	$⊢ N = norm (G)$
Assertion	ressnm	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to {N ↾}_{A} = norm (H)$

Proof

Step	Hyp	Ref	Expression
1		ressnm.1	$⊢ H = G ↾_{𝑠} A$
2		ressnm.2	$⊢ B = {Base}_{G}$
3		ressnm.3	$⊢ \underset{˙}{0} = 0_{G}$
4		ressnm.4	$⊢ N = norm (G)$
5	1 2	ressbas2	$⊢ A \subseteq B \to A = {Base}_{H}$
6	5	3ad2ant3	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to A = {Base}_{H}$
7	2	fvexi	$⊢ B \in V$
8	7	ssex	$⊢ A \subseteq B \to A \in V$
9		eqid	$⊢ dist (G) = dist (G)$
10	1 9	ressds	$⊢ A \in V \to dist (G) = dist (H)$
11	8 10	syl	$⊢ A \subseteq B \to dist (G) = dist (H)$
12	11	3ad2ant3	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to dist (G) = dist (H)$
13		eqidd	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to x = x$
14	1 2 3	ress0g	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to \underset{˙}{0} = 0_{H}$
15	12 13 14	oveq123d	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to x dist (G) \underset{˙}{0} = x dist (H) 0_{H}$
16	6 15	mpteq12dv	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to (x \in A ⟼ x dist (G) \underset{˙}{0}) = (x \in {Base}_{H} ⟼ x dist (H) 0_{H})$
17	4 2 3 9	nmfval	$⊢ N = (x \in B ⟼ x dist (G) \underset{˙}{0})$
18	17	reseq1i	$⊢ {N ↾}_{A} = {(x \in B ⟼ x dist (G) \underset{˙}{0}) ↾}_{A}$
19		resmpt	$⊢ A \subseteq B \to {(x \in B ⟼ x dist (G) \underset{˙}{0}) ↾}_{A} = (x \in A ⟼ x dist (G) \underset{˙}{0})$
20	18 19	eqtrid	$⊢ A \subseteq B \to {N ↾}_{A} = (x \in A ⟼ x dist (G) \underset{˙}{0})$
21	20	3ad2ant3	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to {N ↾}_{A} = (x \in A ⟼ x dist (G) \underset{˙}{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 \in {Base}_{H} ⟼ x dist (H) 0_{H})$
27	26	a1i	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to norm (H) = (x \in {Base}_{H} ⟼ x dist (H) 0_{H})$
28	16 21 27	3eqtr4d	$⊢ (G \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to {N ↾}_{A} = norm (H)$

Metamath Proof Explorer

Theorem ressnm

Proof