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		funres	$⊢ Fun S \to Fun ({S ↾}_{(ℂ \times Y)})$
9	7 8	syl	$⊢ U \in NrmCVec \to Fun ({S ↾}_{(ℂ \times Y)})$
10	9	adantr	$⊢ (U \in NrmCVec \land W \in H) \to Fun ({S ↾}_{(ℂ \times Y)})$
11	4	sspnv	$⊢ (U \in NrmCVec \land W \in H) \to W \in NrmCVec$
12	1 3	nvsf	$⊢ W \in NrmCVec \to R : ℂ \times Y ⟶ Y$
13	11 12	syl	$⊢ (U \in NrmCVec \land W \in H) \to R : ℂ \times Y ⟶ Y$
14	13	ffnd	$⊢ (U \in NrmCVec \land W \in H) \to R Fn (ℂ \times Y)$
15		fnresdm	$⊢ R Fn (ℂ \times Y) \to {R ↾}_{(ℂ \times Y)} = R$
16	14 15	syl	$⊢ (U \in NrmCVec \land W \in H) \to {R ↾}_{(ℂ \times Y)} = R$
17		eqid	$⊢ +_{v} (U) = +_{v} (U)$
18		eqid	$⊢ +_{v} (W) = +_{v} (W)$
19		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
20		eqid	$⊢ {norm}_{CV} (W) = {norm}_{CV} (W)$
21	17 18 2 3 19 20 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))))$
22	21	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))$
23	22	simp2d	$⊢ (U \in NrmCVec \land W \in H) \to R \subseteq S$
24		ssres	$⊢ R \subseteq S \to {R ↾}_{(ℂ \times Y)} \subseteq {S ↾}_{(ℂ \times Y)}$
25	23 24	syl	$⊢ (U \in NrmCVec \land W \in H) \to {R ↾}_{(ℂ \times Y)} \subseteq {S ↾}_{(ℂ \times Y)}$
26	16 25	eqsstrrd	$⊢ (U \in NrmCVec \land W \in H) \to R \subseteq {S ↾}_{(ℂ \times Y)}$
27	10 14 26	3jca	$⊢ (U \in NrmCVec \land W \in H) \to (Fun ({S ↾}_{(ℂ \times Y)}) \land R Fn (ℂ \times Y) \land R \subseteq {S ↾}_{(ℂ \times Y)})$
28		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$
29	27 28	sylan	$⊢ ((U \in NrmCVec \land W \in H) \land (x \in ℂ \land y \in Y)) \to x ({S ↾}_{(ℂ \times Y)}) y = x R y$
30	29	eqcomd	$⊢ ((U \in NrmCVec \land W \in H) \land (x \in ℂ \land y \in Y)) \to x R y = x ({S ↾}_{(ℂ \times Y)}) y$
31	30	ralrimivva	$⊢ (U \in NrmCVec \land W \in H) \to \forall x \in ℂ \forall y \in Y x R y = x ({S ↾}_{(ℂ \times Y)}) y$
32		eqid	$⊢ ℂ \times Y = ℂ \times Y$
33	31 32	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)$
34	6	ffnd	$⊢ U \in NrmCVec \to S Fn (ℂ \times BaseSet (U))$
35	34	adantr	$⊢ (U \in NrmCVec \land W \in H) \to S Fn (ℂ \times BaseSet (U))$
36		ssid	$⊢ ℂ \subseteq ℂ$
37	5 1 4	sspba	$⊢ (U \in NrmCVec \land W \in H) \to Y \subseteq BaseSet (U)$
38		xpss12	$⊢ (ℂ \subseteq ℂ \land Y \subseteq BaseSet (U)) \to ℂ \times Y \subseteq ℂ \times BaseSet (U)$
39	36 37 38	sylancr	$⊢ (U \in NrmCVec \land W \in H) \to ℂ \times Y \subseteq ℂ \times BaseSet (U)$
40		fnssres	$⊢ (S Fn (ℂ \times BaseSet (U)) \land ℂ \times Y \subseteq ℂ \times BaseSet (U)) \to ({S ↾}_{(ℂ \times Y)}) Fn (ℂ \times Y)$
41	35 39 40	syl2anc	$⊢ (U \in NrmCVec \land W \in H) \to ({S ↾}_{(ℂ \times Y)}) Fn (ℂ \times Y)$
42		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))$
43	14 41 42	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))$
44	33 43	mpbird	$⊢ (U \in NrmCVec \land W \in H) \to R = {S ↾}_{(ℂ \times Y)}$

Metamath Proof Explorer

Theorem ssps

Proof