Theorem sspmval

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

	Ref	Expression
Hypotheses	sspm.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	sspm.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	sspm.l	⊢ 𝐿 = ( −𝑣 ‘ 𝑊 )
	sspm.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
Assertion	sspmval	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐴 𝑀 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sspm.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
2		sspm.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		sspm.l	⊢ 𝐿 = ( −𝑣 ‘ 𝑊 )
4		sspm.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
5	4	sspnv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ NrmCVec )
6		neg1cn	⊢ - 1 ∈ ℂ
7		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
8	1 7	nvscl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑌 ) → ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 )
9	6 8	mp3an2	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝐵 ∈ 𝑌 ) → ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 )
10	9	ex	⊢ ( 𝑊 ∈ NrmCVec → ( 𝐵 ∈ 𝑌 → ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 ) )
11	5 10	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐵 ∈ 𝑌 → ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 ) )
12	11	anim2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ∈ 𝑌 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 ) ) )
13	12	imp	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ∈ 𝑌 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 ) )
14		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
15		eqid	⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
16	1 14 15 4	sspgval	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ∈ 𝑌 ) ) → ( 𝐴 ( +𝑣 ‘ 𝑊 ) ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ) )
17	13 16	syldan	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ( +𝑣 ‘ 𝑊 ) ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ) )
18		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
19	1 18 7 4	sspsval	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑌 ) ) → ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) = ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) )
20	6 19	mpanr1	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐵 ∈ 𝑌 ) → ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) = ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) )
21	20	adantrl	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) = ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) )
22	21	oveq2d	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
23	17 22	eqtrd	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ( +𝑣 ‘ 𝑊 ) ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
24	1 15 7 3	nvmval	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑊 ) ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ) )
25	24	3expb	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑊 ) ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ) )
26	5 25	sylan	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑊 ) ( - 1 ( ·𝑠OLD ‘ 𝑊 ) 𝐵 ) ) )
27		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
28	27 1 4	sspba	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) )
29	28	sseld	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐴 ∈ 𝑌 → 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ) )
30	28	sseld	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐵 ∈ 𝑌 → 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) )
31	29 30	anim12d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) ) )
32	31	imp	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) )
33	27 14 18 2	nvmval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
34	33	3expb	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
35	34	adantlr	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝐵 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
36	32 35	syldan	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
37	23 26 36	3eqtr4d	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐴 𝑀 𝐵 ) )