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→ALB=AMB

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⁡WB∈Y
9 6 8 mp3an2 ⊢W∈NrmCVec∧B∈Y→-1⋅𝑠OLD⁡WB∈Y
10 9 ex ⊢W∈NrmCVec→B∈Y→-1⋅𝑠OLD⁡WB∈Y
11 5 10 syl ⊢U∈NrmCVec∧W∈H→B∈Y→-1⋅𝑠OLD⁡WB∈Y
12 11 anim2d ⊢U∈NrmCVec∧W∈H→A∈Y∧B∈Y→A∈Y∧-1⋅𝑠OLD⁡WB∈Y
13 12 imp ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→A∈Y∧-1⋅𝑠OLD⁡WB∈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⁡WB∈Y→A+v⁡W-1⋅𝑠OLD⁡WB=A+v⁡U-1⋅𝑠OLD⁡WB
17 13 16 syldan ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→A+v⁡W-1⋅𝑠OLD⁡WB=A+v⁡U-1⋅𝑠OLD⁡WB
18 eqid ⊢⋅𝑠OLD⁡U=⋅𝑠OLD⁡U
19 1 18 7 4 sspsval ⊢U∈NrmCVec∧W∈H∧−1∈ℂ∧B∈Y→-1⋅𝑠OLD⁡WB=-1⋅𝑠OLD⁡UB
20 6 19 mpanr1 ⊢U∈NrmCVec∧W∈H∧B∈Y→-1⋅𝑠OLD⁡WB=-1⋅𝑠OLD⁡UB
21 20 adantrl ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→-1⋅𝑠OLD⁡WB=-1⋅𝑠OLD⁡UB
22 21 oveq2d ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→A+v⁡U-1⋅𝑠OLD⁡WB=A+v⁡U-1⋅𝑠OLD⁡UB
23 17 22 eqtrd ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→A+v⁡W-1⋅𝑠OLD⁡WB=A+v⁡U-1⋅𝑠OLD⁡UB
24 1 15 7 3 nvmval ⊢W∈NrmCVec∧A∈Y∧B∈Y→ALB=A+v⁡W-1⋅𝑠OLD⁡WB
25 24 3expb ⊢W∈NrmCVec∧A∈Y∧B∈Y→ALB=A+v⁡W-1⋅𝑠OLD⁡WB
26 5 25 sylan ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→ALB=A+v⁡W-1⋅𝑠OLD⁡WB
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→AMB=A+v⁡U-1⋅𝑠OLD⁡UB
34 33 3expb ⊢U∈NrmCVec∧A∈BaseSet⁡U∧B∈BaseSet⁡U→AMB=A+v⁡U-1⋅𝑠OLD⁡UB
35 34 adantlr ⊢U∈NrmCVec∧W∈H∧A∈BaseSet⁡U∧B∈BaseSet⁡U→AMB=A+v⁡U-1⋅𝑠OLD⁡UB
36 32 35 syldan ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→AMB=A+v⁡U-1⋅𝑠OLD⁡UB
37 23 26 36 3eqtr4d ⊢U∈NrmCVec∧W∈H∧A∈Y∧B∈Y→ALB=AMB