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 ⊢ Y = BaseSet ⁡ W
sspm.m ⊢ M = - v ⁡ U
sspm.l ⊢ L = - v ⁡ W
sspm.h ⊢ H = SubSp ⁡ U
Assertion sspmval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A L B = A M B

Proof

Step Hyp Ref Expression
1 sspm.y ⊢ Y = BaseSet ⁡ W
2 sspm.m ⊢ M = - v ⁡ U
3 sspm.l ⊢ L = - v ⁡ W
4 sspm.h ⊢ H = SubSp ⁡ U
5 4 sspnv ⊢ U ∈ NrmCVec ∧ W ∈ H → W ∈ NrmCVec
6 neg1cn ⊢ − 1 ∈ ℂ
7 eqid ⊢ ⋅ 𝑠OLD ⁡ W = ⋅ 𝑠OLD ⁡ W
8 1 7 nvscl ⊢ W ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ B ∈ Y → -1 ⋅ 𝑠OLD ⁡ W B ∈ Y
9 6 8 mp3an2 ⊢ W ∈ NrmCVec ∧ B ∈ Y → -1 ⋅ 𝑠OLD ⁡ W B ∈ Y
10 9 ex ⊢ W ∈ NrmCVec → B ∈ Y → -1 ⋅ 𝑠OLD ⁡ W B ∈ Y
11 5 10 syl ⊢ U ∈ NrmCVec ∧ W ∈ H → B ∈ Y → -1 ⋅ 𝑠OLD ⁡ W B ∈ Y
12 11 anim2d ⊢ U ∈ NrmCVec ∧ W ∈ H → A ∈ Y ∧ B ∈ Y → A ∈ Y ∧ -1 ⋅ 𝑠OLD ⁡ W B ∈ Y
13 12 imp ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A ∈ Y ∧ -1 ⋅ 𝑠OLD ⁡ W B ∈ Y
14 eqid ⊢ + v ⁡ U = + v ⁡ U
15 eqid ⊢ + v ⁡ W = + v ⁡ W
16 1 14 15 4 sspgval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ -1 ⋅ 𝑠OLD ⁡ W B ∈ Y → A + v ⁡ W -1 ⋅ 𝑠OLD ⁡ W B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ W B
17 13 16 syldan ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A + v ⁡ W -1 ⋅ 𝑠OLD ⁡ W B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ W B
18 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
19 1 18 7 4 sspsval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ − 1 ∈ ℂ ∧ B ∈ Y → -1 ⋅ 𝑠OLD ⁡ W B = -1 ⋅ 𝑠OLD ⁡ U B
20 6 19 mpanr1 ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ B ∈ Y → -1 ⋅ 𝑠OLD ⁡ W B = -1 ⋅ 𝑠OLD ⁡ U B
21 20 adantrl ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → -1 ⋅ 𝑠OLD ⁡ W B = -1 ⋅ 𝑠OLD ⁡ U B
22 21 oveq2d ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ W B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B
23 17 22 eqtrd ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A + v ⁡ W -1 ⋅ 𝑠OLD ⁡ W B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B
24 1 15 7 3 nvmval ⊢ W ∈ NrmCVec ∧ A ∈ Y ∧ B ∈ Y → A L B = A + v ⁡ W -1 ⋅ 𝑠OLD ⁡ W B
25 24 3expb ⊢ W ∈ NrmCVec ∧ A ∈ Y ∧ B ∈ Y → A L B = A + v ⁡ W -1 ⋅ 𝑠OLD ⁡ W B
26 5 25 sylan ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A L B = A + v ⁡ W -1 ⋅ 𝑠OLD ⁡ W B
27 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
28 27 1 4 sspba ⊢ U ∈ NrmCVec ∧ W ∈ H → Y ⊆ BaseSet ⁡ U
29 28 sseld ⊢ U ∈ NrmCVec ∧ W ∈ H → A ∈ Y → A ∈ BaseSet ⁡ U
30 28 sseld ⊢ U ∈ NrmCVec ∧ W ∈ H → B ∈ Y → B ∈ BaseSet ⁡ U
31 29 30 anim12d ⊢ U ∈ NrmCVec ∧ W ∈ H → A ∈ Y ∧ B ∈ Y → A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U
32 31 imp ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U
33 27 14 18 2 nvmval ⊢ U ∈ NrmCVec ∧ A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U → A M B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B
34 33 3expb ⊢ U ∈ NrmCVec ∧ A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U → A M B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B
35 34 adantlr ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ BaseSet ⁡ U ∧ B ∈ BaseSet ⁡ U → A M B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B
36 32 35 syldan ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A M B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B
37 23 26 36 3eqtr4d ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y ∧ B ∈ Y → A L B = A M B