# 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 𝑋 = ( BaseSet ‘ 𝑈 )
nvpncan2.2 𝐺 = ( +𝑣𝑈 )
nvpncan2.3 𝑀 = ( −𝑣𝑈 )
Assertion nvaddsub4 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝑀 𝐶 ) 𝐺 ( 𝐵 𝑀 𝐷 ) ) )

### Proof

Step Hyp Ref Expression
1 nvpncan2.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvpncan2.2 𝐺 = ( +𝑣𝑈 )
3 nvpncan2.3 𝑀 = ( −𝑣𝑈 )
4 neg1cn - 1 ∈ ℂ
5 eqid ( ·𝑠OLD𝑈 ) = ( ·𝑠OLD𝑈 )
6 1 2 5 nvdi ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ 𝐶𝑋𝐷𝑋 ) ) → ( - 1 ( ·𝑠OLD𝑈 ) ( 𝐶 𝐺 𝐷 ) ) = ( ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) )
7 4 6 mp3anr1 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( - 1 ( ·𝑠OLD𝑈 ) ( 𝐶 𝐺 𝐷 ) ) = ( ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) )
8 7 3adant2 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( - 1 ( ·𝑠OLD𝑈 ) ( 𝐶 𝐺 𝐷 ) ) = ( ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) )
9 8 oveq2d ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) ( 𝐶 𝐺 𝐷 ) ) ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) ) )
10 1 5 nvscl ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐶𝑋 ) → ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ∈ 𝑋 )
11 4 10 mp3an2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐶𝑋 ) → ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ∈ 𝑋 )
12 1 5 nvscl ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐷𝑋 ) → ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ∈ 𝑋 )
13 4 12 mp3an2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐷𝑋 ) → ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ∈ 𝑋 )
14 11 13 anim12dan ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ∈ 𝑋 ) )
15 14 3adant2 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ∈ 𝑋 ) )
16 1 2 nvadd4 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) ) = ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ) 𝐺 ( 𝐵 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) ) )
17 15 16 syld3an3 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) ) = ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ) 𝐺 ( 𝐵 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) ) )
18 9 17 eqtrd ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) ( 𝐶 𝐺 𝐷 ) ) ) = ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ) 𝐺 ( 𝐵 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) ) )
19 simp1 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → 𝑈 ∈ NrmCVec )
20 1 2 nvgcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
21 20 3expb ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
22 21 3adant3 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
23 1 2 nvgcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐶𝑋𝐷𝑋 ) → ( 𝐶 𝐺 𝐷 ) ∈ 𝑋 )
24 23 3expb ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( 𝐶 𝐺 𝐷 ) ∈ 𝑋 )
25 24 3adant2 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( 𝐶 𝐺 𝐷 ) ∈ 𝑋 )
26 1 2 5 3 nvmval ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 𝐺 𝐷 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) ( 𝐶 𝐺 𝐷 ) ) ) )
27 19 22 25 26 syl3anc ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) ( 𝐶 𝐺 𝐷 ) ) ) )
28 1 2 5 3 nvmval ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐶𝑋 ) → ( 𝐴 𝑀 𝐶 ) = ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ) )
29 28 3adant3r ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( 𝐴 𝑀 𝐶 ) = ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ) )
30 29 3adant2r ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( 𝐴 𝑀 𝐶 ) = ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ) )
31 1 2 5 3 nvmval ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋𝐷𝑋 ) → ( 𝐵 𝑀 𝐷 ) = ( 𝐵 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) )
32 31 3adant3l ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋 ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( 𝐵 𝑀 𝐷 ) = ( 𝐵 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) )
33 32 3adant2l ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( 𝐵 𝑀 𝐷 ) = ( 𝐵 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) )
34 30 33 oveq12d ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( 𝐴 𝑀 𝐶 ) 𝐺 ( 𝐵 𝑀 𝐷 ) ) = ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐶 ) ) 𝐺 ( 𝐵 𝐺 ( - 1 ( ·𝑠OLD𝑈 ) 𝐷 ) ) ) )
35 18 27 34 3eqtr4d ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝑀 𝐶 ) 𝐺 ( 𝐵 𝑀 𝐷 ) ) )