Metamath Proof Explorer

Theorem nvmdi

Description: Distributive law for scalar product over subtraction. (Contributed by NM, 14-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvmdi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvmdi.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
nvmdi.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
Assertion nvmdi ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝐵 𝑀 𝐶 ) ) = ( ( 𝐴 𝑆 𝐵 ) 𝑀 ( 𝐴 𝑆 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 nvmdi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvmdi.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3 nvmdi.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 simpr1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ ℂ )
5 simpr2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
6 neg1cn ⊢ - 1 ∈ ℂ
7 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( - 1 𝑆 𝐶 ) ∈ 𝑋 )
8 6 7 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋 ) → ( - 1 𝑆 𝐶 ) ∈ 𝑋 )
9 8 3ad2antr3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( - 1 𝑆 𝐶 ) ∈ 𝑋 )
10 4 5 9 3jca ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ ( - 1 𝑆 𝐶 ) ∈ 𝑋 ) )
11 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
12 1 11 3 nvdi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ ( - 1 𝑆 𝐶 ) ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 𝐶 ) ) ) = ( ( 𝐴 𝑆 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑆 ( - 1 𝑆 𝐶 ) ) ) )
13 10 12 syldan ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 𝐶 ) ) ) = ( ( 𝐴 𝑆 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑆 ( - 1 𝑆 𝐶 ) ) ) )
14 1 3 nvscom ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( - 1 𝑆 𝐶 ) ) = ( - 1 𝑆 ( 𝐴 𝑆 𝐶 ) ) )
15 6 14 mp3anr2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( - 1 𝑆 𝐶 ) ) = ( - 1 𝑆 ( 𝐴 𝑆 𝐶 ) ) )
16 15 3adantr2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( - 1 𝑆 𝐶 ) ) = ( - 1 𝑆 ( 𝐴 𝑆 𝐶 ) ) )
17 16 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑆 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑆 ( - 1 𝑆 𝐶 ) ) ) = ( ( 𝐴 𝑆 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝐴 𝑆 𝐶 ) ) ) )
18 13 17 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 𝐶 ) ) ) = ( ( 𝐴 𝑆 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝐴 𝑆 𝐶 ) ) ) )
19 1 11 3 2 nvmval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝑀 𝐶 ) = ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 𝐶 ) ) )
20 19 3adant3r1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝑀 𝐶 ) = ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 𝐶 ) ) )
21 20 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝐵 𝑀 𝐶 ) ) = ( 𝐴 𝑆 ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 𝐶 ) ) ) )
22 simpl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝑈 ∈ NrmCVec )
23 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑆 𝐵 ) ∈ 𝑋 )
24 23 3adant3r3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 𝐵 ) ∈ 𝑋 )
25 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝑆 𝐶 ) ∈ 𝑋 )
26 25 3adant3r2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 𝐶 ) ∈ 𝑋 )
27 1 11 3 2 nvmval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑆 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝑆 𝐵 ) 𝑀 ( 𝐴 𝑆 𝐶 ) ) = ( ( 𝐴 𝑆 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝐴 𝑆 𝐶 ) ) ) )
28 22 24 26 27 syl3anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑆 𝐵 ) 𝑀 ( 𝐴 𝑆 𝐶 ) ) = ( ( 𝐴 𝑆 𝐵 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝐴 𝑆 𝐶 ) ) ) )
29 18 21 28 3eqtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝐵 𝑀 𝐶 ) ) = ( ( 𝐴 𝑆 𝐵 ) 𝑀 ( 𝐴 𝑆 𝐶 ) ) )