Theorem 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	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	sspg.g	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	sspg.f	⊢ 𝐹 = ( +𝑣 ‘ 𝑊 )
	sspg.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
Assertion	sspg	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sspg.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
2		sspg.g	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3		sspg.f	⊢ 𝐹 = ( +𝑣 ‘ 𝑊 )
4		sspg.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
5		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
6	5 2	nvgf	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 : ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ⟶ ( BaseSet ‘ 𝑈 ) )
7	6	ffund	⊢ ( 𝑈 ∈ NrmCVec → Fun 𝐺 )
8		funres	⊢ ( Fun 𝐺 → Fun ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )
9	7 8	syl	⊢ ( 𝑈 ∈ NrmCVec → Fun ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )
10	9	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → Fun ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )
11	4	sspnv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ NrmCVec )
12	1 3	nvgf	⊢ ( 𝑊 ∈ NrmCVec → 𝐹 : ( 𝑌 × 𝑌 ) ⟶ 𝑌 )
13	11 12	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐹 : ( 𝑌 × 𝑌 ) ⟶ 𝑌 )
14	13	ffnd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐹 Fn ( 𝑌 × 𝑌 ) )
15		fnresdm	⊢ ( 𝐹 Fn ( 𝑌 × 𝑌 ) → ( 𝐹 ↾ ( 𝑌 × 𝑌 ) ) = 𝐹 )
16	14 15	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ↾ ( 𝑌 × 𝑌 ) ) = 𝐹 )
17		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
18		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
19		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
20		eqid	⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
21	2 3 17 18 19 20 4	isssp	⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ NrmCVec ∧ ( 𝐹 ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑊 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ ( normCV ‘ 𝑊 ) ⊆ ( normCV ‘ 𝑈 ) ) ) ) )
22	21	simplbda	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑊 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ ( normCV ‘ 𝑊 ) ⊆ ( normCV ‘ 𝑈 ) ) )
23	22	simp1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐹 ⊆ 𝐺 )
24		ssres	⊢ ( 𝐹 ⊆ 𝐺 → ( 𝐹 ↾ ( 𝑌 × 𝑌 ) ) ⊆ ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )
25	23 24	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ↾ ( 𝑌 × 𝑌 ) ) ⊆ ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )
26	16 25	eqsstrrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐹 ⊆ ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )
27	10 14 26	3jca	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( Fun ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ∧ 𝐹 Fn ( 𝑌 × 𝑌 ) ∧ 𝐹 ⊆ ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ) )
28		oprssov	⊢ ( ( ( Fun ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ∧ 𝐹 Fn ( 𝑌 × 𝑌 ) ∧ 𝐹 ⊆ ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) = ( 𝑥 𝐹 𝑦 ) )
29	27 28	sylan	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) = ( 𝑥 𝐹 𝑦 ) )
30	29	eqcomd	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) )
31	30	ralrimivva	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) )
32		eqid	⊢ ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 )
33	31 32	jctil	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) ) )
34	6	ffnd	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 Fn ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) )
35	34	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐺 Fn ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) )
36	5 1 4	sspba	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) )
37		xpss12	⊢ ( ( 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) ∧ 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) ) → ( 𝑌 × 𝑌 ) ⊆ ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) )
38	36 36 37	syl2anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑌 × 𝑌 ) ⊆ ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) )
39		fnssres	⊢ ( ( 𝐺 Fn ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ∧ ( 𝑌 × 𝑌 ) ⊆ ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) Fn ( 𝑌 × 𝑌 ) )
40	35 38 39	syl2anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) Fn ( 𝑌 × 𝑌 ) )
41		eqfnov	⊢ ( ( 𝐹 Fn ( 𝑌 × 𝑌 ) ∧ ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) Fn ( 𝑌 × 𝑌 ) ) → ( 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ↔ ( ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) ) ) )
42	14 40 41	syl2anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ↔ ( ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) ) ) )
43	33 42	mpbird	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )