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