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		funres	$⊢ Fun N \to Fun ({N ↾}_{Y})$
18	16 17	syl	$⊢ U \in NrmCVec \to Fun ({N ↾}_{Y})$
19	18	ad2antrr	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to Fun ({N ↾}_{Y})$
20		fnresdm	$⊢ M Fn Y \to {M ↾}_{Y} = M$
21	8 20	syl	$⊢ (U \in NrmCVec \land W \in H) \to {M ↾}_{Y} = M$
22		eqid	$⊢ +_{v} (U) = +_{v} (U)$
23		eqid	$⊢ +_{v} (W) = +_{v} (W)$
24		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
25		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
26	22 23 24 25 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)))$
27	26	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)$
28	27	simp3d	$⊢ (U \in NrmCVec \land W \in H) \to M \subseteq N$
29		ssres	$⊢ M \subseteq N \to {M ↾}_{Y} \subseteq {N ↾}_{Y}$
30	28 29	syl	$⊢ (U \in NrmCVec \land W \in H) \to {M ↾}_{Y} \subseteq {N ↾}_{Y}$
31	21 30	eqsstrrd	$⊢ (U \in NrmCVec \land W \in H) \to M \subseteq {N ↾}_{Y}$
32	31	adantr	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to M \subseteq {N ↾}_{Y}$
33	6	fdmd	$⊢ W \in NrmCVec \to dom M = Y$
34	33	eleq2d	$⊢ W \in NrmCVec \to (x \in dom M \leftrightarrow x \in Y)$
35	34	biimpar	$⊢ (W \in NrmCVec \land x \in Y) \to x \in dom M$
36	5 35	sylan	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to x \in dom M$
37		funssfv	$⊢ (Fun ({N ↾}_{Y}) \land M \subseteq {N ↾}_{Y} \land x \in dom M) \to ({N ↾}_{Y}) (x) = M (x)$
38	19 32 36 37	syl3anc	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to ({N ↾}_{Y}) (x) = M (x)$
39	38	eqcomd	$⊢ ((U \in NrmCVec \land W \in H) \land x \in Y) \to M (x) = ({N ↾}_{Y}) (x)$
40	8 15 39	eqfnfvd	$⊢ (U \in NrmCVec \land W \in H) \to M = {N ↾}_{Y}$

Metamath Proof Explorer

Theorem sspn

Proof