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		funres	$⊢ Fun G \to Fun ({G ↾}_{(Y \times Y)})$
9	7 8	syl	$⊢ U \in NrmCVec \to Fun ({G ↾}_{(Y \times Y)})$
10	9	adantr	$⊢ (U \in NrmCVec \land W \in H) \to Fun ({G ↾}_{(Y \times Y)})$
11	4	sspnv	$⊢ (U \in NrmCVec \land W \in H) \to W \in NrmCVec$
12	1 3	nvgf	$⊢ W \in NrmCVec \to F : Y \times Y ⟶ Y$
13	11 12	syl	$⊢ (U \in NrmCVec \land W \in H) \to F : Y \times Y ⟶ Y$
14	13	ffnd	$⊢ (U \in NrmCVec \land W \in H) \to F Fn (Y \times Y)$
15		fnresdm	$⊢ F Fn (Y \times Y) \to {F ↾}_{(Y \times Y)} = F$
16	14 15	syl	$⊢ (U \in NrmCVec \land W \in H) \to {F ↾}_{(Y \times Y)} = F$
17		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
18		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
19		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
20		eqid	$⊢ {norm}_{CV} (W) = {norm}_{CV} (W)$
21	2 3 17 18 19 20 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))))$
22	21	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))$
23	22	simp1d	$⊢ (U \in NrmCVec \land W \in H) \to F \subseteq G$
24		ssres	$⊢ F \subseteq G \to {F ↾}_{(Y \times Y)} \subseteq {G ↾}_{(Y \times Y)}$
25	23 24	syl	$⊢ (U \in NrmCVec \land W \in H) \to {F ↾}_{(Y \times Y)} \subseteq {G ↾}_{(Y \times Y)}$
26	16 25	eqsstrrd	$⊢ (U \in NrmCVec \land W \in H) \to F \subseteq {G ↾}_{(Y \times Y)}$
27	10 14 26	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)})$
28		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$
29	27 28	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$
30	29	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$
31	30	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$
32		eqid	$⊢ Y \times Y = Y \times Y$
33	31 32	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)$
34	6	ffnd	$⊢ U \in NrmCVec \to G Fn (BaseSet (U) \times BaseSet (U))$
35	34	adantr	$⊢ (U \in NrmCVec \land W \in H) \to G Fn (BaseSet (U) \times BaseSet (U))$
36	5 1 4	sspba	$⊢ (U \in NrmCVec \land W \in H) \to Y \subseteq BaseSet (U)$
37		xpss12	$⊢ (Y \subseteq BaseSet (U) \land Y \subseteq BaseSet (U)) \to Y \times Y \subseteq BaseSet (U) \times BaseSet (U)$
38	36 36 37	syl2anc	$⊢ (U \in NrmCVec \land W \in H) \to Y \times Y \subseteq BaseSet (U) \times BaseSet (U)$
39		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)$
40	35 38 39	syl2anc	$⊢ (U \in NrmCVec \land W \in H) \to ({G ↾}_{(Y \times Y)}) Fn (Y \times Y)$
41		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))$
42	14 40 41	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))$
43	33 42	mpbird	$⊢ (U \in NrmCVec \land W \in H) \to F = {G ↾}_{(Y \times Y)}$

Metamath Proof Explorer

Theorem sspg

Proof