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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑀 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) − ( 𝐵 𝑃 𝐶 ) ) )