Theorem siii 8509

Description: Inference from sii 8510.

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 3975	. . . . . 6 |- (B = (0v` U) -> (APB) = (AP(0v` U)))
2		siii.9	. . . . . . . 8 |- U e. CPreHil
3	2	phnvi 8471	. . . . . . 7 |- U e. NrmCVec
4		siii.a	. . . . . . 7 |- A e. X
5		siii.1	. . . . . . . 8 |- X = (Base` U)
6		eqid 1478	. . . . . . . 8 |- (0v` U) = (0v` U)
7		siii.7	. . . . . . . 8 |- P = (.i` U)
8	5, 6, 7	ip0r 8366	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X) -> (AP(0v` U)) = 0)
9	3, 4, 8	mp2an 699	. . . . . 6 |- (AP(0v` U)) = 0
10	1, 9	syl6eq 1526	. . . . 5 |- (B = (0v` U) -> (APB) = 0)
11	10	fveq2d 3734	. . . 4 |- (B = (0v` U) -> (abs` (APB)) = (abs` 0))
12		abs0 6877	. . . 4 |- (abs` 0) = 0
13	11, 12	syl6eq 1526	. . 3 |- (B = (0v` U) -> (abs` (APB)) = 0)
14		siii.6	. . . . . 6 |- N = (norm` U)
15	5, 14	nvge0 8298	. . . . 5 |- ((U e. NrmCVec /\ A e. X) -> 0 <_ (N` A))
16	3, 4, 15	mp2an 699	. . . 4 |- 0 <_ (N` A)
17		siii.b	. . . . 5 |- B e. X
18	5, 14	nvge0 8298	. . . . 5 |- ((U e. NrmCVec /\ B e. X) -> 0 <_ (N` B))
19	3, 17, 18	mp2an 699	. . . 4 |- 0 <_ (N` B)
20	5, 14, 3, 4	nvcli 8284	. . . . 5 |- (N` A) e. RR
21	5, 14, 3, 17	nvcli 8284	. . . . 5 |- (N` B) e. RR
22	20, 21	mulge0 5619	. . . 4 |- ((0 <_ (N` A) /\ 0 <_ (N` B)) -> 0 <_ ((N` A) x. (N` B)))
23	16, 19, 22	mp2an 699	. . 3 |- 0 <_ ((N` A) x. (N` B))
24	13, 23	syl6eqbr 2657	. 2 |- (B = (0v` U) -> (abs` (APB)) <_ ((N` A) x. (N` B)))
25	21	recn 5326	. . . . . . . . . . 11 |- (N` B) e. CC
26	25	sqeq0 6617	. . . . . . . . . 10 |- (((N` B)^2) = 0 <-> (N` B) = 0)
27	5, 6, 14	nvz 8293	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ B e. X) -> ((N` B) = 0 <-> B = (0v` U)))
28	3, 17, 27	mp2an 699	. . . . . . . . . 10 |- ((N` B) = 0 <-> B = (0v` U))
29	26, 28	bitr 173	. . . . . . . . 9 |- (((N` B)^2) = 0 <-> B = (0v` U))
30	29	necon3bii 1601	. . . . . . . 8 |- (((N` B)^2) =/= 0 <-> B =/= (0v` U))
31	5, 7	ipcl 8361	. . . . . . . . . 10 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (BPA) e. CC)
32	3, 17, 4, 31	mp3an 918	. . . . . . . . 9 |- (BPA) e. CC
33	21	resqcl 6624	. . . . . . . . . 10 |- ((N` B)^2) e. RR
34	33	recn 5326	. . . . . . . . 9 |- ((N` B)^2) e. CC
35	32, 34	divcan1z 5730	. . . . . . . 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 8363	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (*` (APB)) = (BPA))
38	3, 4, 17, 37	mp3an 918	. . . . . . 7 |- (*` (APB)) = (BPA)
39	36, 38	syl6eqr 1528	. . . . . 6 |- (B =/= (0v` U) -> (((BPA) / ((N` B)^2)) x. ((N` B)^2)) = (*` (APB)))
40	39	opreq2d 3982	. . . . 5 |- (B =/= (0v` U) -> ((APB) x. (((BPA) / ((N` B)^2)) x. ((N` B)^2))) = ((APB) x. (*` (APB))))
41	40	fveq2d 3734	. . . 4 |- (B =/= (0v` U) -> (sqr` ((APB) x. (((BPA) / ((N` B)^2)) x. ((N` B)^2)))) = (sqr` ((APB) x. (*` (APB)))))
42	5, 7	ipcl 8361	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) e. CC)
43	3, 4, 17, 42	mp3an 918	. . . . 5 |- (APB) e. CC
44		absvalt 6763	. . . . 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 1529	. . 3 |- (B =/= (0v` U) -> (abs` (APB)) = (sqr` ((APB) x. (((BPA) / ((N` B)^2)) x. ((N` B)^2)))))
47	36	eqcomd 1483	. . . 4 |- (B =/= (0v` U) -> (BPA) = (((BPA) / ((N` B)^2)) x. ((N` B)^2)))
48		eqid 1478	. . . . . 6 |- (-v` U) = (-v` U)
49		eqid 1478	. . . . . 6 |- (.s` U) = (.s` U)
50	5, 14, 7, 2, 4, 17, 48, 49	siilem2 8508	. . . . 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	32, 34	divclz 5723	. . . . . 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	32, 43, 34	3pm3.2i 820	. . . . . . . . 9 |- ((BPA) e. CC /\ (APB) e. CC /\ ((N` B)^2) e. CC)
54		div23t 5749	. . . . . . . . 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 697	. . . . . . . 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	32, 43	mulcom 5335	. . . . . . . . 9 |- ((BPA) x. (APB)) = ((APB) x. (BPA))
58	5, 7	ipipcj 8364	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((APB) x. (BPA)) = ((abs` (APB))^2))
59	3, 4, 17, 58	mp3an 918	. . . . . . . . 9 |- ((APB) x. (BPA)) = ((abs` (APB))^2)
60	57, 59	eqtr 1498	. . . . . . . 8 |- ((BPA) x. (APB)) = ((abs` (APB))^2)
61	60	opreq1i 3977	. . . . . . 7 |- (((BPA) x. (APB)) / ((N` B)^2)) = (((abs` (APB))^2) / ((N` B)^2))
62	56, 61	syl5reqr 1525	. . . . . 6 |- (B =/= (0v` U) -> (((BPA) / ((N` B)^2)) x. (APB)) = (((abs` (APB))^2) / ((N` B)^2)))
63	43	abscl 6839	. . . . . . . . 9 |- (abs` (APB)) e. RR
64	63	resqcl 6624	. . . . . . . 8 |- ((abs` (APB))^2) e. RR
65	64, 33	redivclz 5801	. . . . . . 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 1551	. . . . 5 |- (B =/= (0v` U) -> (((BPA) / ((