This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐴 𝑀 𝐵 ) )