Theorem 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	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	ssps.s	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	ssps.r	⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑊 )
	ssps.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
Assertion	ssps	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑅 = ( 𝑆 ↾ ( ℂ × 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssps.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
2		ssps.s	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3		ssps.r	⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑊 )
4		ssps.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
5		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
6	5 2	nvsf	⊢ ( 𝑈 ∈ NrmCVec → 𝑆 : ( ℂ × ( 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	nvsf	⊢ ( 𝑊 ∈ NrmCVec → 𝑅 : ( ℂ × 𝑌 ) ⟶ 𝑌 )
13	11 12	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑅 : ( ℂ × 𝑌 ) ⟶ 𝑌 )
14	13	ffnd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑅 Fn ( ℂ × 𝑌 ) )
15		fnresdm	⊢ ( 𝑅 Fn ( ℂ × 𝑌 ) → ( 𝑅 ↾ ( ℂ × 𝑌 ) ) = 𝑅 )
16	14 15	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑅 ↾ ( ℂ × 𝑌 ) ) = 𝑅 )
17		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
18		eqid	⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
19		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
20		eqid	⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
21	17 18 2 3 19 20 4	isssp	⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ 𝑅 ⊆ 𝑆 ∧ ( normCV ‘ 𝑊 ) ⊆ ( normCV ‘ 𝑈 ) ) ) ) )
22	21	simplbda	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ 𝑅 ⊆ 𝑆 ∧ ( normCV ‘ 𝑊 ) ⊆ ( normCV ‘ 𝑈 ) ) )
23	22	simp2d	⊢ ( ( 𝑈 ∈ 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 ‘ 𝑈 ) ) )
35	34	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑆 Fn ( ℂ × ( BaseSet ‘ 𝑈 ) ) )
36		ssid	⊢ ℂ ⊆ ℂ
37	5 1 4	sspba	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) )
38		xpss12	⊢ ( ( ℂ ⊆ ℂ ∧ 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) ) → ( ℂ × 𝑌 ) ⊆ ( ℂ × ( BaseSet ‘ 𝑈 ) ) )
39	36 37 38	sylancr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ℂ × 𝑌 ) ⊆ ( ℂ × ( BaseSet ‘ 𝑈 ) ) )
40		fnssres	⊢ ( ( 𝑆 Fn ( ℂ × ( BaseSet ‘ 𝑈 ) ) ∧ ( ℂ × 𝑌 ) ⊆ ( ℂ × ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑆 ↾ ( ℂ × 𝑌 ) ) Fn ( ℂ × 𝑌 ) )
41	35 39 40	syl2anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ↾ ( ℂ × 𝑌 ) ) Fn ( ℂ × 𝑌 ) )
42		eqfnov	⊢ ( ( 𝑅 Fn ( ℂ × 𝑌 ) ∧ ( 𝑆 ↾ ( ℂ × 𝑌 ) ) Fn ( ℂ × 𝑌 ) ) → ( 𝑅 = ( 𝑆 ↾ ( ℂ × 𝑌 ) ) ↔ ( ( ℂ × 𝑌 ) = ( ℂ × 𝑌 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑅 𝑦 ) = ( 𝑥 ( 𝑆 ↾ ( ℂ × 𝑌 ) ) 𝑦 ) ) ) )
43	14 41 42	syl2anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑅 = ( 𝑆 ↾ ( ℂ × 𝑌 ) ) ↔ ( ( ℂ × 𝑌 ) = ( ℂ × 𝑌 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑅 𝑦 ) = ( 𝑥 ( 𝑆 ↾ ( ℂ × 𝑌 ) ) 𝑦 ) ) ) )
44	33 43	mpbird	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑅 = ( 𝑆 ↾ ( ℂ × 𝑌 ) ) )