# Metamath Proof Explorer

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}=\mathrm{BaseSet}\left({U}\right)$
nvpncan2.2 ${⊢}{G}={+}_{v}\left({U}\right)$
nvpncan2.3 ${⊢}{M}={-}_{v}\left({U}\right)$
Assertion nvaddsub4 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\to \left({A}{G}{B}\right){M}\left({C}{G}{D}\right)=\left({A}{M}{C}\right){G}\left({B}{M}{D}\right)$

### Proof

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