Theorem ip0r 8332

Description: Inner product with a zero second argument.

Hypotheses

Ref	Expression
ip0r.1	|- X = (Base` U)
ip0r.5	|- Z = (0v` U)
ip0r.7	|- P = (.i` U)

Assertion

Ref	Expression
ip0r	|- ((U e. NrmCVec /\ A e. X) -> (APZ) = 0)

Proof of Theorem ip0r

Step	Hyp	Ref	Expression
1		ip0r.1	. . . . 5 |- X = (Base` U)
2		ip0r.5	. . . . 5 |- Z = (0v` U)
3	1, 2	nvzcl 8219	. . . 4 |- (U e. NrmCVec -> Z e. X)
4	3	adantr 389	. . 3 |- ((U e. NrmCVec /\ A e. X) -> Z e. X)
5		eqid 1474	. . . 4 |- (+v` U) = (+v` U)
6		eqid 1474	. . . 4 |- (.s` U) = (.s` U)
7		eqid 1474	. . . 4 |- (norm` U) = (norm` U)
8		ip0r.7	. . . 4 |- P = (.i` U)
9	1, 5, 6, 7, 8	ipval2 8319	. . 3 |- ((U e. NrmCVec /\ A e. X /\ Z e. X) -> (APZ) = ((((((norm` U)` (A(+v` U)Z))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)Z)))^2)) + (i x. ((((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)Z)))^2)))) / 4))
10	4, 9	mpd3an3 916	. 2 |- ((U e. NrmCVec /\ A e. X) -> (APZ) = ((((((norm` U)` (A(+v` U)Z))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)Z)))^2)) + (i x. ((((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)Z)))^2)))) / 4))
11		ax1cn 5252	. . . . . . . . . . . . . 14 |- 1 e. CC
12	11	negcl 5352	. . . . . . . . . . . . 13 |- -u1 e. CC
13	6, 2	nvsz 8223	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ -u1 e. CC) -> (-u1(.s` U)Z) = Z)
14	12, 13	mpan2 695	. . . . . . . . . . . 12 |- (U e. NrmCVec -> (-u1(.s` U)Z) = Z)
15	14	adantr 389	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X) -> (-u1(.s` U)Z) = Z)
16	15	opreq2d 3971	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X) -> (A(+v` U)(-u1(.s` U)Z)) = (A(+v` U)Z))
17	16	fveq2d 3723	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X) -> ((norm` U)` (A(+v` U)(-u1(.s` U)Z))) = ((norm` U)` (A(+v` U)Z)))
18	17	opreq1d 3970	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> (((norm` U)` (A(+v` U)(-u1(.s` U)Z)))^2) = (((norm` U)` (A(+v` U)Z))^2))
19	18	opreq2d 3971	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X) -> ((((norm` U)` (A(+v` U)Z))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)Z)))^2)) = ((((norm` U)` (A(+v` U)Z))^2) - (((norm` U)` (A(+v` U)Z))^2)))
20	1, 5, 6, 7, 8	ipval2lem3 8317	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ Z e. X) -> (((norm` U)` (A(+v` U)Z))^2) e. RR)
21	4, 20	mpd3an3 916	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X) -> (((norm` U)` (A(+v` U)Z))^2) e. RR)
22	21	recnd 5298	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> (((norm` U)` (A(+v` U)Z))^2) e. CC)
23		subidt 5378	. . . . . . . 8 |- ((((norm` U)` (A(+v` U)Z))^2) e. CC -> ((((norm` U)` (A(+v` U)Z))^2) - (((norm` U)` (A(+v` U)Z))^2)) = 0)
24	22, 23	syl 10	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X) -> ((((norm` U)` (A(+v` U)Z))^2) - (((norm` U)` (A(+v` U)Z))^2)) = 0)
25	19, 24	eqtrd 1505	. . . . . 6 |- ((U e. NrmCVec /\ A e. X) -> ((((norm` U)` (A(+v` U)Z))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)Z)))^2)) = 0)
26		axicn 5253	. . . . . . . . . . . . . . . 16 |- i e. CC
27	26	negcl 5352	. . . . . . . . . . . . . . 15 |- -ui e. CC
28	6, 2	nvsz 8223	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ -ui e. CC) -> (-ui(.s` U)Z) = Z)
29	27, 28	mpan2 695	. . . . . . . . . . . . . 14 |- (U e. NrmCVec -> (-ui(.s` U)Z) = Z)
30	6, 2	nvsz 8223	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ i e. CC) -> (i(.s` U)Z) = Z)
31	26, 30	mpan2 695	. . . . . . . . . . . . . 14 |- (U e. NrmCVec -> (i(.s` U)Z) = Z)
32	29, 31	eqtr4d 1508	. . . . . . . . . . . . 13 |- (U e. NrmCVec -> (-ui(.s` U)Z) = (i(.s` U)Z))
33	32	adantr 389	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ A e. X) -> (-ui(.s` U)Z) = (i(.s` U)Z))
34	33	opreq2d 3971	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X) -> (A(+v` U)(-ui(.s` U)Z)) = (A(+v` U)(i(.s` U)Z)))
35	34	fveq2d 3723	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X) -> ((norm` U)` (A(+v` U)(-ui(.s` U)Z))) = ((norm` U)` (A(+v` U)(i(.s` U)Z))))
36	35	opreq1d 3970	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X) -> (((norm` U)` (A(+v` U)(-ui(.s` U)Z)))^2) = (((norm` U)` (A(+v` U)(i(.s` U)Z)))^2))
37	36	opreq2d 3971	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> ((((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)Z)))^2)) = ((((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) - (((norm` U)` (A(+v` U)(i(.s` U)Z)))^2)))
38	1, 5, 6, 7, 8	ipval2lem4 8318	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ A e. X /\ Z e. X) /\ i e. CC) -> (((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) e. CC)
39	26, 38	mpan2 695	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ Z e. X) -> (((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) e. CC)
40	4, 39	mpd3an3 916	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X) -> (((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) e. CC)
41		subidt 5378	. . . . . . . . 9 |- ((((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) e. CC -> ((((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) - (((norm` U)` (A(+v` U)(i(.s` U)Z)))^2)) = 0)
42	40, 41	syl 10	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> ((((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) - (((norm` U)` (A(+v` U)(i(.s` U)Z)))^2)) = 0)
43	37, 42	eqtrd 1505	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X) -> ((((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)Z)))^2)) = 0)
44	43	opreq2d 3971	. . . . . 6 |- ((U e. NrmCVec /\ A e. X) -> (i x. ((((norm` U)` (A(+v` U)(i(.s` U)Z)))^2) - (((norm` U)` (A(+v` U)(-ui(.s` U)Z)))^2))) = (i x. 0))
45	25, 44	opreq12d 3973	. . . . 5 |- ((U e. NrmCVec /\ A e. X) -> (((((norm` U)` (A(+v` U)Z))^2) - (((norm` U)` (A(+v` U)(-u1(.s` U)Z)))^2)) + <