Metamath Proof Explorer

Theorem nvaddsub4

Description: Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 8-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvpncan2.1 ⊢ X = BaseSet ⁡ U
nvpncan2.2 ⊢ G = + v ⁡ U
nvpncan2.3 ⊢ M = - v ⁡ U
Assertion nvaddsub4 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B M C G D = A M C G B M D

Proof

Step Hyp Ref Expression
1 nvpncan2.1 ⊢ X = BaseSet ⁡ U
2 nvpncan2.2 ⊢ G = + v ⁡ U
3 nvpncan2.3 ⊢ M = - v ⁡ U
4 neg1cn ⊢ − 1 ∈ ℂ
5 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
6 1 2 5 nvdi ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ C ∈ X ∧ D ∈ X → -1 ⋅ 𝑠OLD ⁡ U C G D = -1 ⋅ 𝑠OLD ⁡ U C G -1 ⋅ 𝑠OLD ⁡ U D
7 4 6 mp3anr1 ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ D ∈ X → -1 ⋅ 𝑠OLD ⁡ U C G D = -1 ⋅ 𝑠OLD ⁡ U C G -1 ⋅ 𝑠OLD ⁡ U D
8 7 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → -1 ⋅ 𝑠OLD ⁡ U C G D = -1 ⋅ 𝑠OLD ⁡ U C G -1 ⋅ 𝑠OLD ⁡ U D
9 8 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G -1 ⋅ 𝑠OLD ⁡ U C G D = A G B G -1 ⋅ 𝑠OLD ⁡ U C G -1 ⋅ 𝑠OLD ⁡ U D
10 1 5 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ C ∈ X → -1 ⋅ 𝑠OLD ⁡ U C ∈ X
11 4 10 mp3an2 ⊢ U ∈ NrmCVec ∧ C ∈ X → -1 ⋅ 𝑠OLD ⁡ U C ∈ X
12 1 5 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ D ∈ X → -1 ⋅ 𝑠OLD ⁡ U D ∈ X
13 4 12 mp3an2 ⊢ U ∈ NrmCVec ∧ D ∈ X → -1 ⋅ 𝑠OLD ⁡ U D ∈ X
14 11 13 anim12dan ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ D ∈ X → -1 ⋅ 𝑠OLD ⁡ U C ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U D ∈ X
15 14 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → -1 ⋅ 𝑠OLD ⁡ U C ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U D ∈ X
16 1 2 nvadd4 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U C ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U D ∈ X → A G B G -1 ⋅ 𝑠OLD ⁡ U C G -1 ⋅ 𝑠OLD ⁡ U D = A G -1 ⋅ 𝑠OLD ⁡ U C G B G -1 ⋅ 𝑠OLD ⁡ U D
17 15 16 syld3an3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G -1 ⋅ 𝑠OLD ⁡ U C G -1 ⋅ 𝑠OLD ⁡ U D = A G -1 ⋅ 𝑠OLD ⁡ U C G B G -1 ⋅ 𝑠OLD ⁡ U D
18 9 17 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G -1 ⋅ 𝑠OLD ⁡ U C G D = A G -1 ⋅ 𝑠OLD ⁡ U C G B G -1 ⋅ 𝑠OLD ⁡ U D
19 simp1 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → U ∈ NrmCVec
20 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B ∈ X
21 20 3expb ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B ∈ X
22 21 3adant3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B ∈ X
23 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ D ∈ X → C G D ∈ X
24 23 3expb ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ D ∈ X → C G D ∈ X
25 24 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → C G D ∈ X
26 1 2 5 3 nvmval ⊢ U ∈ NrmCVec ∧ A G B ∈ X ∧ C G D ∈ X → A G B M C G D = A G B G -1 ⋅ 𝑠OLD ⁡ U C G D
27 19 22 25 26 syl3anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B M C G D = A G B G -1 ⋅ 𝑠OLD ⁡ U C G D
28 1 2 5 3 nvmval ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ C ∈ X → A M C = A G -1 ⋅ 𝑠OLD ⁡ U C
29 28 3adant3r ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ C ∈ X ∧ D ∈ X → A M C = A G -1 ⋅ 𝑠OLD ⁡ U C
30 29 3adant2r ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A M C = A G -1 ⋅ 𝑠OLD ⁡ U C
31 1 2 5 3 nvmval ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ D ∈ X → B M D = B G -1 ⋅ 𝑠OLD ⁡ U D
32 31 3adant3l ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → B M D = B G -1 ⋅ 𝑠OLD ⁡ U D
33 32 3adant2l ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → B M D = B G -1 ⋅ 𝑠OLD ⁡ U D
34 30 33 oveq12d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A M C G B M D = A G -1 ⋅ 𝑠OLD ⁡ U C G B G -1 ⋅ 𝑠OLD ⁡ U D
35 18 27 34 3eqtr4d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B M C G D = A M C G B M D