Theorem dip0r

Description: Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dip0r.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	dip0r.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
	dip0r.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion	dip0r	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝑍 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		dip0r.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		dip0r.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3		dip0r.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4	1 2	nvzcl	⊢ ( 𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋 )
5	4	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 𝑍 ∈ 𝑋 )
6		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
7		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
8		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
9	1 6 7 8 3	ipval2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) → ( 𝐴 𝑃 𝑍 ) = ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
10	5 9	mpd3an3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝑍 ) = ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
11		neg1cn	⊢ - 1 ∈ ℂ
12	7 2	nvsz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = 𝑍 )
13	11 12	mpan2	⊢ ( 𝑈 ∈ NrmCVec → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = 𝑍 )
14	13	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = 𝑍 )
15	14	oveq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) )
16	15	fveq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) )
17	16	oveq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) = ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) )
18	17	oveq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) ) )
19	1 6 7 8 3	ipval2lem3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) ∈ ℝ )
20	5 19	mpd3an3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) ∈ ℝ )
21	20	recnd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) ∈ ℂ )
22	21	subidd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) ) = 0 )
23	18 22	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = 0 )
24		negicn	⊢ - i ∈ ℂ
25	7 2	nvsz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ) → ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = 𝑍 )
26	24 25	mpan2	⊢ ( 𝑈 ∈ NrmCVec → ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = 𝑍 )
27		ax-icn	⊢ i ∈ ℂ
28	7 2	nvsz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ) → ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = 𝑍 )
29	27 28	mpan2	⊢ ( 𝑈 ∈ NrmCVec → ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = 𝑍 )
30	26 29	eqtr4d	⊢ ( 𝑈 ∈ NrmCVec → ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) )
31	30	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) )
32	31	oveq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) )
33	32	fveq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) )
34	33	oveq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) = ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) )
35	34	oveq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) )
36	1 6 7 8 3	ipval2lem4	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) ∧ i ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ∈ ℂ )
37	27 36	mpan2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ∈ ℂ )
38	5 37	mpd3an3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ∈ ℂ )
39	38	subidd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = 0 )
40	35 39	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) = 0 )
41	40	oveq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) = ( i · 0 ) )
42	23 41	oveq12d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) = ( 0 + ( i · 0 ) ) )
43		it0e0	⊢ ( i · 0 ) = 0
44	43	oveq2i	⊢ ( 0 + ( i · 0 ) ) = ( 0 + 0 )
45		00id	⊢ ( 0 + 0 ) = 0
46	44 45	eqtri	⊢ ( 0 + ( i · 0 ) ) = 0
47	42 46	eqtrdi	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) = 0 )
48	47	oveq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) / 4 ) = ( 0 / 4 ) )
49		4cn	⊢ 4 ∈ ℂ
50		4ne0	⊢ 4 ≠ 0
51	49 50	div0i	⊢ ( 0 / 4 ) = 0
52	48 51	eqtrdi	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) ) ↑ 2 ) ) ) ) / 4 ) = 0 )
53	10 52	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝑍 ) = 0 )