sspg

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

	Ref	Expression
Hypotheses	sspg.y	$⊢ Y = BaseSet (W)$
	sspg.g	$⊢ G = +_{v} (U)$
	sspg.f	$⊢ F = +_{v} (W)$
	sspg.h	$⊢ H = SubSp (U)$
Assertion	sspg	$⊢ (U \in NrmCVec \land W \in H) \to F = {G ↾}_{(Y \times Y)}$

Proof

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

Metamath Proof Explorer

Theorem sspg

Proof