sspn

Description: The norm on a subspace is a restriction of the norm on the parent space. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sspn.y	$⊢ Y = BaseSet (W)$
	sspn.n	$⊢ N = {norm}_{CV} (U)$
	sspn.m	$⊢ M = {norm}_{CV} (W)$
	sspn.h	$⊢ H = SubSp (U)$
Assertion	sspn	$⊢ (U \in NrmCVec \land W \in H) \to M = {N ↾}_{Y}$

Proof

Step	Hyp	Ref	Expression
1		sspn.y	$⊢ Y = BaseSet (W)$
2		sspn.n	$⊢ N = {norm}_{CV} (U)$
3		sspn.m	$⊢ M = {norm}_{CV} (W)$
4		sspn.h	$⊢ H = SubSp (U)$
5	4	sspnv	$⊢ (U \in NrmCVec \land W \in H) \to W \in NrmCVec$
6	1 3	nvf	$⊢ W \in NrmCVec \to M : Y ⟶ ℝ$
7	5 6	syl	$⊢ (U \in NrmCVec \land W \in H) \to M : Y ⟶ ℝ$
8	7	ffnd	$⊢ (U \in NrmCVec \land W \in H) \to M Fn Y$
9		eqid	$⊢ BaseSet (U) = BaseSet (U)$
10	9 2	nvf	$⊢ U \in NrmCVec \to N : BaseSet (U) ⟶ ℝ$
11	10	ffnd	$⊢ U \in NrmCVec \to N Fn BaseSet (U)$
12	11	adantr	$⊢ (U \in NrmCVec \land W \in H) \to N Fn BaseSet (U)$
13	9 1 4	sspba	$⊢ (U \in NrmCVec \land W \in H) \to Y \subseteq BaseSet (U)$
14		fnssres	$⊢ (N Fn BaseSet (U) \land Y \subseteq BaseSet (U)) \to ({N ↾}_{Y}) Fn Y$
15	12 13 14	syl2anc	$⊢ (U \in NrmCVec \land W \in H) \to ({N ↾}_{Y}) Fn Y$
16	10	ffund	$⊢ U \in NrmCVec \to Fun N$
17	16	funresd	$⊢ U \in NrmCVec \to Fun ({N ↾}_{Y})$
18	17	ad2antrr	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to Fun ({N ↾}_{Y})$
19		fnresdm	$⊢ M Fn Y \to {M ↾}_{Y} = M$
20	8 19	syl	$⊢ (U \in NrmCVec \land W \in H) \to {M ↾}_{Y} = M$
21		eqid	$⊢ +_{v} (U) = +_{v} (U)$
22		eqid	$⊢ +_{v} (W) = +_{v} (W)$
23		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
24		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
25	21 22 23 24 2 3 4	isssp	$⊢ U \in NrmCVec \to (W \in H \leftrightarrow (W \in NrmCVec \land (+_{v} (W) \subseteq +_{v} (U) \land \cdot_{𝑠OLD} (W) \subseteq \cdot_{𝑠OLD} (U) \land M \subseteq N)))$
26	25	simplbda	$⊢ (U \in NrmCVec \land W \in H) \to (+_{v} (W) \subseteq +_{v} (U) \land \cdot_{𝑠OLD} (W) \subseteq \cdot_{𝑠OLD} (U) \land M \subseteq N)$
27	26	simp3d	$⊢ (U \in NrmCVec \land W \in H) \to M \subseteq N$
28		ssres	$⊢ M \subseteq N \to {M ↾}_{Y} \subseteq {N ↾}_{Y}$
29	27 28	syl	$⊢ (U \in NrmCVec \land W \in H) \to {M ↾}_{Y} \subseteq {N ↾}_{Y}$
30	20 29	eqsstrrd	$⊢ (U \in NrmCVec \land W \in H) \to M \subseteq {N ↾}_{Y}$
31	30	adantr	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to M \subseteq {N ↾}_{Y}$
32	6	fdmd	$⊢ W \in NrmCVec \to dom M = Y$
33	32	eleq2d	$⊢ W \in NrmCVec \to (x \in dom M \leftrightarrow x \in Y)$
34	33	biimpar	$⊢ (W \in NrmCVec \land x \in Y) \to x \in dom M$
35	5 34	sylan	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to x \in dom M$
36		funssfv	$⊢ (Fun ({N ↾}_{Y}) \land M \subseteq {N ↾}_{Y} \land x \in dom M) \to ({N ↾}_{Y}) (x) = M (x)$
37	18 31 35 36	syl3anc	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to ({N ↾}_{Y}) (x) = M (x)$
38	37	eqcomd	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to M (x) = ({N ↾}_{Y}) (x)$
39	8 15 38	eqfnfvd	$⊢ (U \in NrmCVec \land W \in H) \to M = {N ↾}_{Y}$

Metamath Proof Explorer

Theorem sspn

Proof