ssps

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

	Ref	Expression
Hypotheses	ssps.y	$⊢ Y = BaseSet (W)$
	ssps.s	$⊢ S = \cdot_{𝑠OLD} (U)$
	ssps.r	$⊢ R = \cdot_{𝑠OLD} (W)$
	ssps.h	$⊢ H = SubSp (U)$
Assertion	ssps	$⊢ (U \in NrmCVec \land W \in H) \to R = {S ↾}_{(ℂ \times Y)}$

Proof

Step	Hyp	Ref	Expression
1		ssps.y	$⊢ Y = BaseSet (W)$
2		ssps.s	$⊢ S = \cdot_{𝑠OLD} (U)$
3		ssps.r	$⊢ R = \cdot_{𝑠OLD} (W)$
4		ssps.h	$⊢ H = SubSp (U)$
5		eqid	$⊢ BaseSet (U) = BaseSet (U)$
6	5 2	nvsf	$⊢ U \in NrmCVec \to S : ℂ \times BaseSet (U) ⟶ BaseSet (U)$
7	6	ffund	$⊢ U \in NrmCVec \to Fun S$
8	7	funresd	$⊢ U \in NrmCVec \to Fun ({S ↾}_{(ℂ \times Y)})$
9	8	adantr	$⊢ (U \in NrmCVec \land W \in H) \to Fun ({S ↾}_{(ℂ \times Y)})$
10	4	sspnv	$⊢ (U \in NrmCVec \land W \in H) \to W \in NrmCVec$
11	1 3	nvsf	$⊢ W \in NrmCVec \to R : ℂ \times Y ⟶ Y$
12	10 11	syl	$⊢ (U \in NrmCVec \land W \in H) \to R : ℂ \times Y ⟶ Y$
13	12	ffnd	$⊢ (U \in NrmCVec \land W \in H) \to R Fn (ℂ \times Y)$
14		fnresdm	$⊢ R Fn (ℂ \times Y) \to {R ↾}_{(ℂ \times Y)} = R$
15	13 14	syl	$⊢ (U \in NrmCVec \land W \in H) \to {R ↾}_{(ℂ \times Y)} = R$
16		eqid	$⊢ +_{v} (U) = +_{v} (U)$
17		eqid	$⊢ +_{v} (W) = +_{v} (W)$
18		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
19		eqid	$⊢ {norm}_{CV} (W) = {norm}_{CV} (W)$
20	16 17 2 3 18 19 4	isssp	$⊢ U \in NrmCVec \to (W \in H \leftrightarrow (W \in NrmCVec \land (+_{v} (W) \subseteq +_{v} (U) \land R \subseteq S \land {norm}_{CV} (W) \subseteq {norm}_{CV} (U))))$
21	20	simplbda	$⊢ (U \in NrmCVec \land W \in H) \to (+_{v} (W) \subseteq +_{v} (U) \land R \subseteq S \land {norm}_{CV} (W) \subseteq {norm}_{CV} (U))$
22	21	simp2d	$⊢ (U \in NrmCVec \land W \in H) \to R \subseteq S$
23		ssres	$⊢ R \subseteq S \to {R ↾}_{(ℂ \times Y)} \subseteq {S ↾}_{(ℂ \times Y)}$
24	22 23	syl	$⊢ (U \in NrmCVec \land W \in H) \to {R ↾}_{(ℂ \times Y)} \subseteq {S ↾}_{(ℂ \times Y)}$
25	15 24	eqsstrrd	$⊢ (U \in NrmCVec \land W \in H) \to R \subseteq {S ↾}_{(ℂ \times Y)}$
26	9 13 25	3jca	$⊢ (U \in NrmCVec \land W \in H) \to (Fun ({S ↾}_{(ℂ \times Y)}) \land R Fn (ℂ \times Y) \land R \subseteq {S ↾}_{(ℂ \times Y)})$
27		oprssov	$⊢ ((Fun ({S ↾}_{(ℂ \times Y)}) \land R Fn (ℂ \times Y) \land R \subseteq {S ↾}_{(ℂ \times Y)}) \land (x \in ℂ \land y \in Y)) \to x ({S ↾}_{(ℂ \times Y)}) y = x R y$
28	26 27	sylan	$⊢ ((U \in NrmCVec \land W \in H) \land (x \in ℂ \land y \in Y)) \to x ({S ↾}_{(ℂ \times Y)}) y = x R y$
29	28	eqcomd	$⊢ ((U \in NrmCVec \land W \in H) \land (x \in ℂ \land y \in Y)) \to x R y = x ({S ↾}_{(ℂ \times Y)}) y$
30	29	ralrimivva	$⊢ (U \in NrmCVec \land W \in H) \to \forall x \in ℂ \forall y \in Y x R y = x ({S ↾}_{(ℂ \times Y)}) y$
31		eqid	$⊢ ℂ \times Y = ℂ \times Y$
32	30 31	jctil	$⊢ (U \in NrmCVec \land W \in H) \to (ℂ \times Y = ℂ \times Y \land \forall x \in ℂ \forall y \in Y x R y = x ({S ↾}_{(ℂ \times Y)}) y)$
33	6	ffnd	$⊢ U \in NrmCVec \to S Fn (ℂ \times BaseSet (U))$
34	33	adantr	$⊢ (U \in NrmCVec \land W \in H) \to S Fn (ℂ \times BaseSet (U))$
35		ssid	$⊢ ℂ \subseteq ℂ$
36	5 1 4	sspba	$⊢ (U \in NrmCVec \land W \in H) \to Y \subseteq BaseSet (U)$
37		xpss12	$⊢ (ℂ \subseteq ℂ \land Y \subseteq BaseSet (U)) \to ℂ \times Y \subseteq ℂ \times BaseSet (U)$
38	35 36 37	sylancr	$⊢ (U \in NrmCVec \land W \in H) \to ℂ \times Y \subseteq ℂ \times BaseSet (U)$
39		fnssres	$⊢ (S Fn (ℂ \times BaseSet (U)) \land ℂ \times Y \subseteq ℂ \times BaseSet (U)) \to ({S ↾}_{(ℂ \times Y)}) Fn (ℂ \times Y)$
40	34 38 39	syl2anc	$⊢ (U \in NrmCVec \land W \in H) \to ({S ↾}_{(ℂ \times Y)}) Fn (ℂ \times Y)$
41		eqfnov	$⊢ (R Fn (ℂ \times Y) \land ({S ↾}_{(ℂ \times Y)}) Fn (ℂ \times Y)) \to (R = {S ↾}_{(ℂ \times Y)} \leftrightarrow (ℂ \times Y = ℂ \times Y \land \forall x \in ℂ \forall y \in Y x R y = x ({S ↾}_{(ℂ \times Y)}) y))$
42	13 40 41	syl2anc	$⊢ (U \in NrmCVec \land W \in H) \to (R = {S ↾}_{(ℂ \times Y)} \leftrightarrow (ℂ \times Y = ℂ \times Y \land \forall x \in ℂ \forall y \in Y x R y = x ({S ↾}_{(ℂ \times Y)}) y))$
43	32 42	mpbird	$⊢ (U \in NrmCVec \land W \in H) \to R = {S ↾}_{(ℂ \times Y)}$

Metamath Proof Explorer

Theorem ssps

Proof