Theorem ipid 8363

Description: The inner product of a vector with itself is the square of the vector's norm. Equation I4 of [Ponnusamy] p. 362.

Hypotheses

Ref	Expression
ipid.1	|- X = (Base` U)
ipid.6	|- N = (norm` U)
ipid.7	|- P = (.i` U)

Assertion

Ref	Expression
ipid	|- ((U e. NrmCVec /\ A e. X) -> (APA) = ((N` A)^2))

Proof of Theorem ipid

Step	Hyp	Ref	Expression
1		ipid.1	. . . 4 |- X = (Base` U)
2		eqid 1475	. . . 4 |- (+v` U) = (+v` U)
3		eqid 1475	. . . 4 |- (.s` U) = (.s` U)
4		ipid.6	. . . 4 |- N = (norm` U)
5		ipid.7	. . . 4 |- P = (.i` U)
6	1, 2, 3, 4, 5	ipval2 8357	. . 3 |- ((U e. NrmCVec /\ A e. X /\ A e. X) -> (APA) = (((((N` (A(+v` U)A))^2) - ((N` (A(+v` U)(-u1(.s` U)A)))^2)) + (i x. (((N` (A(+v` U)(i(.s` U)A)))^2) - ((N` (A(+v` U)(-ui(.s` U)A)))^2)))) / 4))
7	6	3anidm23 884	. 2 |- ((U e. NrmCVec /\ A e. X) -> (APA) = (((((N` (A(+v` U)A))^2) - ((N` (A(+v` U)(-u1(.s` U)A)))^2)) + (i x. (((N` (A(+v` U)(i(.s` U)A)))^2) - ((N` (A(+v` U)(-ui(.s` U)A)))^2)))) / 4))
8	2	vafval 8222	. . . . . . . . . . . . 13 |- (+v` U) = (1st` (1st` U))
9	3	smfval 8224	. . . . . . . . . . . . 13 |- (.s` U) = (2nd` (1st` U))
10	1, 2	bafval 8223	. . . . . . . . . . . . 13 |- X = ran (+v` U)
11	8, 9, 10	vc2 8174	. . . . . . . . . . . 12 |- (((1st` U) e. CVec /\ A e. X) -> (A(+v` U)A) = (2(.s` U)A))
12		eqid 1475	. . . . . . . . . . . . 13 |- (1st` U) = (1st` U)
13	12	nvvc 8234	. . . . . . . . . . . 12 |- (U e. NrmCVec -> (1st` U) e. CVec)
14	11, 13	sylan 448	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X) -> (A(+v` U)A) = (2(.s` U)A))
15	14	fveq2d 3728	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X) -> (N` (A(+v` U)A)) = (N` (2(.s` U)A)))
16		2nn 5999	. . . . . . . . . . . . 13 |- 2 e. NN
17	16	nnre 5931	. . . . . . . . . . . 12 |- 2 e. RR
18		0re 5440	. . . . . . . . . . . . 13 |- 0 e. RR
19		2re 5979	. . . . . . . . . . . . 13 |- 2 e. RR
20		2pos 5989	. . . . . . . . . . . . 13 |- 0 < 2
21	18, 19, 20	ltlei 5581	. . . . . . . . . . . 12 |- 0 <_ 2
22	17, 21	pm3.2i 285	. . . . . . . . . . 11 |- (2 e. RR /\ 0 <_ 2)
23	1, 3, 4	nvsge0 8291	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (2 e. RR /\ 0 <_ 2) /\ A e. X) -> (N` (2(.s` U)A)) = (2 x. (N` A)))
24	22, 23	mp3an2 904	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X) -> (N` (2(.s` U)A)) = (2 x. (N` A)))
25	15, 24	eqtrd 1507	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X) -> (N` (A(+v` U)A)) = (2 x. (N` A)))
26	25	opreq1d 3975	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> ((N` (A(+v` U)A))^2) = ((2 x. (N` A))^2))
27	1, 4	nvcl 8287	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X) -> (N` A) e. RR)
28	27	recnd 5315	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X) -> (N` A) e. CC)
29		2cn 5980	. . . . . . . . . 10 |- 2 e. CC
30		2nn0 6115	. . . . . . . . . 10 |- 2 e. NN0
31		mulexpt 6594	. . . . . . . . . 10 |- ((2 e. CC /\ (N` A) e. CC /\ 2 e. NN0) -> ((2 x. (N` A))^2) = ((2^2) x. ((N` A)^2)))
32	29, 30, 31	mp3an13 907	. . . . . . . . 9 |- ((N` A) e. CC -> ((2 x. (N` A))^2) = ((2^2) x. ((N` A)^2)))
33	28, 32	syl 10	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> ((2 x. (N` A))^2) = ((2^2) x. ((N` A)^2)))
34		sq2 6638	. . . . . . . . . 10 |- (2^2) = 4
35	34	opreq1i 3971	. . . . . . . . 9 |- ((2^2) x. ((N` A)^2)) = (4 x. ((N` A)^2))
36	35	a1i 8	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> ((2^2) x. ((N` A)^2)) = (4 x. ((N` A)^2)))
37	26, 33, 36	3eqtrd 1511	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X) -> ((N` (A(+v` U)A))^2) = (4 x. ((N` A)^2)))
38		eqid 1475	. . . . . . . . . . . 12 |- (0v` U) = (0v` U)
39	1, 2, 3, 38	nvrinv 8273	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X) -> (A(+v` U)(-u1(.s` U)A)) = (0v` U))
40	39	fveq2d 3728	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X) -> (N` (A(+v` U)(-u1(.s` U)A))) = (N` (0v` U)))
41	38, 4	nvz0 8296	. . . . . . . . . . 11 |- (U e. NrmCVec -> (N` (0v` U)) = 0)
42	41	adantr 389	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X) -> (N` (0v` U)) = 0)
43	40, 42	eqtrd 1507	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X) -> (N` (A(+v` U)(-u1(.s` U)A))) = 0)
44	43	opreq1d 3975	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> ((N` (A(+v` U)(-u1(.s` U)A)))^2) = (0^2))
45		sq0 6635	. . . . . . . 8 |- (0^2) = 0
46	44, 45	syl6eq 1523	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X) -> ((N` (A(+v` U)(-u1(.s` U)A)))^2) = 0)
47	37, 46	opreq12d 3978	. . . . . 6 |- ((U e. NrmCVec /\ A e. X) -> (((N` (A(+v` U)A))^2) - ((N` (A(+v` U)(-u1(.s` U)A)))^2)) = ((4 x. ((N` A)^2)) - 0))
48		sqclt 6611	. . . . . . . . 9 |- ((N` A) e. CC -> ((N` A)^2) e. CC)
49	28, 48	syl 10	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> ((N` A)^2) e. CC)
50		4re 5982	. . . . . . . . . 10 |- 4 e. RR
51	50	recn 5314	. . . . . . . . 9 |- 4 e. CC
52		axmulcl 5273	. . . . . . . . 9 |- ((4 e. CC /\ ((N` A)^2) e. CC) -> (4 x. ((N` A)^2)) e. CC)
53	51, 52	mpan 695	. . . . . . . 8 |- (((N` A)^2) e. CC -> (4 x. ((N` A)^2)) e. CC)
54	49, 53	syl 10	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X) -> (4 x. ((N` A)^2)) e. CC)
55		subid1t 5396	. . . . . . 7 |- ((4 x. ((N` A)^2)) e. CC -> ((4 x. ((N` A)^2)) - 0) = (4 x. ((N` A)^2)))
56	54, 55	syl 10	. . . . . 6 |- ((U e. NrmCVec /\ A e. X) -> ((4 x. ((N` A)^2)) - 0) = (4 x. ((N` A)^2)))
57	47, 56	eqtrd 1507	. . . . 5 |- ((U e. NrmCVec /\ A e. X) -> (((N` (A(+v` U)A))^2) - ((N` (A(+v` U)(-u1(.s` U)A)))^2)) = (4 x. ((N` A)^2)))
58		1re 5435	. . . . . . . . . . . . . . . 16 |- 1 e. RR
59	58	renegcl 5416	. . . . . . . . . . . . . . . 16 |- -u1 e. RR
60		absreimt 6857	. . . . . . . . . . . . . . . 16 |- ((1 e. RR /\ -u1 e. RR) -> (abs` (1 + (i x. -u1))) = (sqr` ((1^2) + (-u1^2))))
61	58, 59, 60	mp2an 697	. . . . . . . . . . . . . . 15 |- (abs` (1 + (i x. -u1))) = (sqr` ((1^2) + (-u1^2)))
62		axicn 5270	. . . . . . . . . . . . . . . . . . 19 |- i e. CC
63		ax1cn 5269	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
64	62, 63	mulneg2 5446	. . . . . . . . . . . . . . . . . 18 |- (i x. -u1) = -u(i x. 1)
65	62	mulid1 5332	. . . . . . . . . . . . . . . . . . 19 |- (i x. 1) = i
66	65	negeqi 5360	. . . . . . . . . . . . . . . . . 18 |- -u(i x. 1) = -ui
67	64, 66	eqtr 1495	. . . . . . . . . . . . . . . . 17 |- (i x. -u1) = -ui
68	67	opreq2i 3972	. . . . . . . . . . . . . . . 16 |- (1 + (i x. -u1)) = (1 + -ui)
69	68	fveq2i 3727	. . . . . . . . . . . . . . 15 |- (abs` (1 + (i x. -u1))) = (abs` (1 + -ui))
70		sqnegt 6610	. . . . . . . . . . . . . . . . . 18 |- (1 e. CC -> (-u1^2) = (1^2))
71	63, 70	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (-u1^2) = (1^2)
72	71	opreq2i 3972	. . . . . . . . . . . . . . . 16 |- ((1^2) + (-u1^2)) = ((1^2) + (1^2))
73	72	fveq2i 3727	. . . . . . . . . . . . . . 15 |- (sqr` ((1^2) + (-u1^2))) = (sqr` ((1^2) + (1^2)))
74	61, 69, 73