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 ⊢ 𝑋 = ( 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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝑀 𝐶 ) 𝐺 ( 𝐵 𝑀 𝐷 ) ) )