Theorem siii 8457

Description: Inference from sii 8458.

Hypotheses

Ref	Expression
siii.1	|- X = (Base` U)
siii.6	|- N = (norm` U)
siii.7	|- P = (.i` U)
siii.9	|- U e. CPreHil
siii.a	|- A e. X
siii.b	|- B e. X

Assertion

Ref	Expression
siii	|- (abs` (APB)) <_ ((N` A) x. (N` B))

Proof of Theorem siii

Step	Hyp	Ref	Expression
1		opreq2 3960	. . . . . 6 |- (B = (0v` U) -> (APB) = (AP(0v` U)))
2		siii.9	. . . . . . . 8 |- U e. CPreHil
3	2	phnvi 8419	. . . . . . 7 |- U e. NrmCVec
4		siii.a	. . . . . . 7 |- A e. X
5		siii.1	. . . . . . . 8 |- X = (Base` U)
6		eqid 1473	. . . . . . . 8 |- (0v` U) = (0v` U)
7		siii.7	. . . . . . . 8 |- P = (.i` U)
8	5, 6, 7	ip0r 8317	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X) -> (AP(0v` U)) = 0)
9	3, 4, 8	mp2an 696	. . . . . 6 |- (AP(0v` U)) = 0
10	1, 9	syl6eq 1520	. . . . 5 |- (B = (0v` U) -> (APB) = 0)
11	10	fveq2d 3719	. . . 4 |- (B = (0v` U) -> (abs` (APB)) = (abs` 0))
12		abs0 6822	. . . 4 |- (abs` 0) = 0
13	11, 12	syl6eq 1520	. . 3 |- (B = (0v` U) -> (abs` (APB)) = 0)
14		siii.6	. . . . . 6 |- N = (norm` U)
15	5, 14	nvge0 8254	. . . . 5 |- ((U e. NrmCVec /\ A e. X) -> 0 <_ (N` A))
16	3, 4, 15	mp2an 696	. . . 4 |- 0 <_ (N` A)
17		siii.b	. . . . 5 |- B e. X
18	5, 14	nvge0 8254	. . . . 5 |- ((U e. NrmCVec /\ B e. X) -> 0 <_ (N` B))
19	3, 17, 18	mp2an 696	. . . 4 |- 0 <_ (N` B)
20	5, 14, 3, 4	nvcli 8240	. . . . 5 |- (N` A) e. RR
21	5, 14, 3, 17	nvcli 8240	. . . . 5 |- (N` B) e. RR
22	20, 21	mulge0 5589	. . . 4 |- ((0 <_ (N` A) /\ 0 <_ (N` B)) -> 0 <_ ((N` A) x. (N` B)))
23	16, 19, 22	mp2an 696	. . 3 |- 0 <_ ((N` A) x. (N` B))
24	13, 23	syl6eqbr 2647	. 2 |- (B = (0v` U) -> (abs` (APB)) <_ ((N` A) x. (N` B)))
25	21	recn 5294	. . . . . . . . . . 11 |- (N` B) e. CC
26	25	sq00 6554	. . . . . . . . . 10 |- (((N` B)^2) = 0 <-> (N` B) = 0)
27	5, 6, 14	nvz 8249	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ B e. X) -> ((N` B) = 0 <-> B = (0v` U)))
28	3, 17, 27	mp2an 696	. . . . . . . . . 10 |- ((N` B) = 0 <-> B = (0v` U))
29	26, 28	bitr 173	. . . . . . . . 9 |- (((N` B)^2) = 0 <-> B = (0v` U))
30	29	necon3bii 1595	. . . . . . . 8 |- (((N` B)^2) =/= 0 <-> B =/= (0v` U))
31	21	resqcl 6562	. . . . . . . . . 10 |- ((N` B)^2) e. RR
32	31	recn 5294	. . . . . . . . 9 |- ((N` B)^2) e. CC
33	5, 7	ipcl 8312	. . . . . . . . . 10 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (BPA) e. CC)
34	3, 17, 4, 33	mp3an 914	. . . . . . . . 9 |- (BPA) e. CC
35	32, 34	divcan1z 5695	. . . . . . . 8 |- (((N` B)^2) =/= 0 -> (((BPA) / ((N` B)^2)) x. ((N` B)^2)) = (BPA))
36	30, 35	sylbir 201	. . . . . . 7 |- (B =/= (0v` U) -> (((BPA) / ((N` B)^2)) x. ((N` B)^2)) = (BPA))
37	5, 7	ipcj 8314	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (*` (APB)) = (BPA))
38	3, 4, 17, 37	mp3an 914	. . . . . . 7 |- (*` (APB)) = (BPA)
39	36, 38	syl6eqr 1522	. . . . . 6 |- (B =/= (0v` U) -> (((BPA) / ((N` B)^2)) x. ((N` B)^2)) = (*` (APB)))
40	39	opreq2d 3967	. . . . 5 |- (B =/= (0v` U) -> ((APB) x. (((BPA) / ((N` B)^2)) x. ((N` B)^2))) = ((APB) x. (*` (APB))))
41	40	fveq2d 3719	. . . 4 |- (B =/= (0v` U) -> (sqr` ((APB) x. (((BPA) / ((N` B)^2)) x. ((N` B)^2)))) = (sqr` ((APB) x. (*` (APB)))))
42	5, 7	ipcl 8312	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) e. CC)
43	3, 4, 17, 42	mp3an 914	. . . . 5 |- (APB) e. CC
44		absvalt 6702	. . . . 5 |- ((APB) e. CC -> (abs` (APB)) = (sqr` ((APB) x. (*` (APB)))))
45	43, 44	ax-mp 7	. . . 4 |- (abs` (APB)) = (sqr` ((APB) x. (*` (APB))))
46	41, 45	syl6reqr 1523	. . 3 |- (B =/= (0v` U) -> (abs` (APB)) = (sqr` ((APB) x. (((BPA) / ((N` B)^2)) x. ((N` B)^2)))))
47	36	eqcomd 1477	. . . 4 |- (B =/= (0v` U) -> (BPA) = (((BPA) / ((N` B)^2)) x. ((N` B)^2)))
48		eqid 1473	. . . . . 6 |- (-v` U) = (-v` U)
49		eqid 1473	. . . . . 6 |- (.s` U) = (.s` U)
50	5, 14, 7, 2, 4, 17, 48, 49	siilem2 8456	. . . . 5 |- ((((BPA) / ((N` B)^2)) e. CC /\ (((BPA) / ((N` B)^2)) x. (APB)) e. RR /\ 0 <_ (((BPA) / ((N` B)^2)) x. (APB))) -> ((BPA) = (((BPA) / ((N` B)^2)) x. ((N` B)^2)) -> (sqr` ((APB) x. (((BPA) / ((N` B)^2)) x. ((N` B)^2)))) <_ ((N` A) x. (N` B))))
51	34, 32	divclz 5688	. . . . . 6 |- (((N` B)^2) =/= 0 -> ((BPA) / ((N` B)^2)) e. CC)
52	30, 51	sylbir 201	. . . . 5 |- (B =/= (0v` U) -> ((BPA) / ((N` B)^2)) e. CC)
53	34, 43, 32	3pm3.2i 817	. . . . . . . . 9 |- ((BPA) e. CC /\ (APB) e. CC /\ ((N` B)^2) e. CC)
54		div23t 5713	. . . . . . . . 9 |- ((((BPA) e. CC /\ (APB) e. CC /\ ((N` B)^2) e. CC) /\ ((N` B)^2) =/= 0) -> (((BPA) x. (APB)) / ((N` B)^2)) = (((BPA) / ((N` B)^2)) x. (APB)))
55	53, 54	mpan 694	. . . . . . . 8 |- (((N` B)^2) =/= 0 -> (((BPA) x. (APB)) / ((N` B)^2)) = (((BPA) / ((N` B)^2)) x. (APB)))
56	30, 55	sylbir 201	. . . . . . 7 |- (B =/= (0v` U) -> (((BPA) x. (APB)) / ((N` B)^2)) = (((BPA) / ((N` B)^2)) x. (APB)))
57	34, 43	mulcom 5303	. . . . . . . . 9 |- ((BPA) x. (APB)) = ((APB) x. (BPA))
58	5, 7	ipipcj 8315	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((APB) x. (BPA)) = ((abs` (APB))^2))
59	3, 4, 17, 58	mp3an 914	. . . . . . . . 9 |- ((APB) x. (BPA)) = ((abs` (APB))^2)
60	57, 59	eqtr 1492	. . . . . . . 8 |- ((BPA) x. (APB)) = ((abs` (APB))^2)
61	60	opreq1i 3962	. . . . . . 7 |- (((BPA) x. (APB)) / ((N` B)^2)) = (((abs` (APB))^2) / ((N` B)^2))
62	56, 61	syl5reqr 1519	. . . . . 6 |- (B =/= (0v` U) -> (((BPA) / ((N` B)^2)) x. (APB)) = (((abs` (APB))^2) / ((N` B)^2)))
63	43	abscl 6782	. . . . . . . . 9 |- (abs` (APB)) e. RR
64	63	resqcl 6562	. . . . . . . 8 |- ((abs` (APB))^2) e. RR
65	64, 31	redivclz 5763	. . . . . . 7 |- (((N` B)^2) =/= 0 -> (((abs` (APB))^2) / ((N` B)^2)) e. RR)
66	30, 65	sylbir 201	. . . . . 6 |- (B =/= (0v` U) -> (((abs` (APB))^2) / ((N` B)^2)) e. RR)
67	62, 66	eqeltrd 1545	. . . . 5 |- (B =/= (0v` U) -> (((BPA) / ((N`