Metamath Proof Explorer

Theorem dipsubdir

Description: Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipsubdir.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ipsubdir.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
ipsubdir.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion dipsubdir ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑀 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) − ( 𝐵 𝑃 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ipsubdir.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ipsubdir.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3 ipsubdir.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4 idd ⊢ ( 𝑈 ∈ CPreHilOLD → ( 𝐴 ∈ 𝑋 → 𝐴 ∈ 𝑋 ) )
5 phnv ⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
6 neg1cn ⊢ - 1 ∈ ℂ
7 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
8 1 7 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 )
9 6 8 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 )
10 5 9 sylan ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐵 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 )
11 10 ex ⊢ ( 𝑈 ∈ CPreHilOLD → ( 𝐵 ∈ 𝑋 → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ) )
12 idd ⊢ ( 𝑈 ∈ CPreHilOLD → ( 𝐶 ∈ 𝑋 → 𝐶 ∈ 𝑋 ) )
13 4 11 12 3anim123d ⊢ ( 𝑈 ∈ CPreHilOLD → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) )
14 13 imp ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) )
15 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
16 1 15 3 dipdir ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) 𝑃 𝐶 ) ) )
17 14 16 syldan ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) 𝑃 𝐶 ) ) )
18 1 15 7 2 nvmval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
19 5 18 syl3an1 ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
20 19 3adant3r3 ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
21 20 oveq1d ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑀 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) 𝑃 𝐶 ) )
22 1 7 3 dipass ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) 𝑃 𝐶 ) = ( - 1 · ( 𝐵 𝑃 𝐶 ) ) )
23 6 22 mp3anr1 ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) 𝑃 𝐶 ) = ( - 1 · ( 𝐵 𝑃 𝐶 ) ) )
24 1 3 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝑃 𝐶 ) ∈ ℂ )
25 24 3expb ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝑃 𝐶 ) ∈ ℂ )
26 5 25 sylan ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝑃 𝐶 ) ∈ ℂ )
27 26 mulm1d ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( - 1 · ( 𝐵 𝑃 𝐶 ) ) = - ( 𝐵 𝑃 𝐶 ) )
28 23 27 eqtrd ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) 𝑃 𝐶 ) = - ( 𝐵 𝑃 𝐶 ) )
29 28 3adantr1 ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) 𝑃 𝐶 ) = - ( 𝐵 𝑃 𝐶 ) )
30 29 oveq2d ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑃 𝐶 ) + ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) 𝑃 𝐶 ) ) = ( ( 𝐴 𝑃 𝐶 ) + - ( 𝐵 𝑃 𝐶 ) ) )
31 1 3 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐶 ) ∈ ℂ )
32 31 3adant3r2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑃 𝐶 ) ∈ ℂ )
33 24 3adant3r1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝑃 𝐶 ) ∈ ℂ )
34 32 33 negsubd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑃 𝐶 ) + - ( 𝐵 𝑃 𝐶 ) ) = ( ( 𝐴 𝑃 𝐶 ) − ( 𝐵 𝑃 𝐶 ) ) )
35 5 34 sylan ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑃 𝐶 ) + - ( 𝐵 𝑃 𝐶 ) ) = ( ( 𝐴 𝑃 𝐶 ) − ( 𝐵 𝑃 𝐶 ) ) )
36 30 35 eqtr2d ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑃 𝐶 ) − ( 𝐵 𝑃 𝐶 ) ) = ( ( 𝐴 𝑃 𝐶 ) + ( ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) 𝑃 𝐶 ) ) )
37 17 21 36 3eqtr4d ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑀 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) − ( 𝐵 𝑃 𝐶 ) ) )