Theorem siilem1 8455

Description: Lemma for 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
sii1.3	|- M = (-v` U)
sii1.4	|- S = (.s` U)
sii1.c	|- C e. CC
sii1.r	|- (C x. (APB)) e. RR
sii1.z	|- 0 <_ (C x. (APB))

Assertion

Ref	Expression
siilem1	|- ((BPA) = (C x. ((N` B)^2)) -> (sqr` ((APB) x. (C x. ((N` B)^2)))) <_ ((N` A) x. (N` B)))

Proof of Theorem siilem1

Step	Hyp	Ref	Expression
1		siii.9	. . . . . . . . . . . . 13 |- U e. CPreHil
2	1	phnvi 8419	. . . . . . . . . . . 12 |- U e. NrmCVec
3		siii.b	. . . . . . . . . . . 12 |- B e. X
4		siii.a	. . . . . . . . . . . 12 |- A e. X
5		siii.1	. . . . . . . . . . . . 13 |- X = (Base` U)
6		siii.7	. . . . . . . . . . . . 13 |- P = (.i` U)
7	5, 6	ipcl 8312	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ B e. X /\ A e. X) -> (BPA) e. CC)
8	2, 3, 4, 7	mp3an 914	. . . . . . . . . . 11 |- (BPA) e. CC
9		sii1.c	. . . . . . . . . . . 12 |- C e. CC
10		siii.6	. . . . . . . . . . . . . . 15 |- N = (norm` U)
11	5, 10, 2, 3	nvcli 8240	. . . . . . . . . . . . . 14 |- (N` B) e. RR
12	11	recn 5294	. . . . . . . . . . . . 13 |- (N` B) e. CC
13	12	sqcl 6553	. . . . . . . . . . . 12 |- ((N` B)^2) e. CC
14	9, 13	mulcl 5301	. . . . . . . . . . 11 |- (C x. ((N` B)^2)) e. CC
15	8, 14	subeq0 5385	. . . . . . . . . 10 |- (((BPA) - (C x. ((N` B)^2))) = 0 <-> (BPA) = (C x. ((N` B)^2)))
16		opreq2 3960	. . . . . . . . . . 11 |- (((BPA) - (C x. ((N` B)^2))) = 0 -> ((*` C) x. ((BPA) - (C x. ((N` B)^2)))) = ((*` C) x. 0))
17	9	cjcl 6707	. . . . . . . . . . . 12 |- (*` C) e. CC
18	17	mul01 5411	. . . . . . . . . . 11 |- ((*` C) x. 0) = 0
19	16, 18	syl6eq 1520	. . . . . . . . . 10 |- (((BPA) - (C x. ((N` B)^2))) = 0 -> ((*` C) x. ((BPA) - (C x. ((N` B)^2)))) = 0)
20	15, 19	sylbir 201	. . . . . . . . 9 |- ((BPA) = (C x. ((N` B)^2)) -> ((*` C) x. ((BPA) - (C x. ((N` B)^2)))) = 0)
21	20	opreq2d 3967	. . . . . . . 8 |- ((BPA) = (C x. ((N` B)^2)) -> ((((N` A)^2) - (C x. (APB))) - ((*` C) x. ((BPA) - (C x. ((N` B)^2))))) = ((((N` A)^2) - (C x. (APB))) - 0))
22	5, 10, 2, 4	nvcli 8240	. . . . . . . . . . . 12 |- (N` A) e. RR
23	22	resqcl 6562	. . . . . . . . . . 11 |- ((N` A)^2) e. RR
24	23	recn 5294	. . . . . . . . . 10 |- ((N` A)^2) e. CC
25		sii1.r	. . . . . . . . . . 11 |- (C x. (APB)) e. RR
26	25	recn 5294	. . . . . . . . . 10 |- (C x. (APB)) e. CC
27	24, 26	subcl 5346	. . . . . . . . 9 |- (((N` A)^2) - (C x. (APB))) e. CC
28	27	subid1 5372	. . . . . . . 8 |- ((((N` A)^2) - (C x. (APB))) - 0) = (((N` A)^2) - (C x. (APB)))
29	21, 28	syl6eq 1520	. . . . . . 7 |- ((BPA) = (C x. ((N` B)^2)) -> ((((N` A)^2) - (C x. (APB))) - ((*` C) x. ((BPA) - (C x. ((N` B)^2))))) = (((N` A)^2) - (C x. (APB))))
30		sii1.4	. . . . . . . . . . . . 13 |- S = (.s` U)
31	5, 30	nvscl 8199	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ (*` C) e. CC /\ B e. X) -> ((*` C)SB) e. X)
32	2, 17, 3, 31	mp3an 914	. . . . . . . . . . 11 |- ((*` C)SB) e. X
33		sii1.3	. . . . . . . . . . . 12 |- M = (-v` U)
34	5, 33	nvmcl 8219	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X /\ ((*` C)SB) e. X) -> (AM((*` C)SB)) e. X)
35	2, 4, 32, 34	mp3an 914	. . . . . . . . . 10 |- (AM((*` C)SB)) e. X
36	5, 10, 2, 35	nvcli 8240	. . . . . . . . 9 |- (N` (AM((*` C)SB))) e. RR
37	36	sqge0 6567	. . . . . . . 8 |- 0 <_ ((N` (AM((*` C)SB)))^2)
38	35, 4, 32	3pm3.2i 817	. . . . . . . . . 10 |- ((AM((*` C)SB)) e. X /\ A e. X /\ ((*` C)SB) e. X)
39	5, 33, 6	ipsubdi 8453	. . . . . . . . . 10 |- ((U e. CPreHil /\ ((AM((*` C)SB)) e. X /\ A e. X /\ ((*` C)SB) e. X)) -> ((AM((*` C)SB))P(AM((*` C)SB))) = (((AM((*` C)SB))PA) - ((AM((*` C)SB))P((*` C)SB))))
40	1, 38, 39	mp2an 696	. . . . . . . . 9 |- ((AM((*` C)SB))P(AM((*` C)SB))) = (((AM((*` C)SB))PA) - ((AM((*` C)SB))P((*` C)SB)))
41	5, 10, 6	ipid 8310	. . . . . . . . . 10 |- ((U e. NrmCVec /\ (AM((*` C)SB)) e. X) -> ((AM((*` C)SB))P(AM((*` C)SB))) = ((N` (AM((*` C)SB)))^2))
42	2, 35, 41	mp2an 696	. . . . . . . . 9 |- ((AM((*` C)SB))P(AM((*` C)SB))) = ((N` (AM((*` C)SB)))^2)
43	17, 3, 32	3pm3.2i 817	. . . . . . . . . . . . . . 15 |- ((*` C) e. CC /\ B e. X /\ ((*` C)SB) e. X)
44	5, 30, 6	ipass 8449	. . . . . . . . . . . . . . 15 |- ((U e. CPreHil /\ ((*` C) e. CC /\ B e. X /\ ((*` C)SB) e. X)) -> (((*` C)SB)P((*` C)SB)) = ((*` C) x. (BP((*` C)SB))))
45	1, 43, 44	mp2an 696	. . . . . . . . . . . . . 14 |- (((*` C)SB)P((*` C)SB)) = ((*` C) x. (BP((*` C)SB)))
46	3, 9, 3	3pm3.2i 817	. . . . . . . . . . . . . . . . 17 |- (B e. X /\ C e. CC /\ B e. X)
47	5, 30, 6	ipassr2 8451	. . . . . . . . . . . . . . . . 17 |- ((U e. CPreHil /\ (B e. X /\ C e. CC /\ B e. X)) -> (BP((*` C)SB)) = (C x. (BPB)))
48	1, 46, 47	mp2an 696	. . . . . . . . . . . . . . . 16 |- (BP((*` C)SB)) = (C x. (BPB))
49	5, 10, 6	ipid 8310	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ B e. X) -> (BPB) = ((N` B)^2))
50	2, 3, 49	mp2an 696	. . . . . . . . . . . . . . . . 17 |- (BPB) = ((N` B)^2)
51	50	opreq2i 3963	. . . . . . . . . . . . . . . 16 |- (C x. (BPB)) = (C x. ((N` B)^2))
52	48, 51	eqtr 1492	. . . . . . . . . . . . . . 15 |- (BP((*` C)SB)) = (C x. ((N` B)^2))
53	52	opreq2i 3963	. . . . . . . . . . . . . 14 |- ((*` C) x. (BP((*` C)SB))) = ((*` C) x. (C x. ((N` B)^2)))
54	45, 53	eqtr 1492	. . . . . . . . . . . . 13 |- (((*` C)SB)P((*` C)SB)) = ((*` C) x. (C x. ((N` B)^2)))
55	54	opreq2i 3963	. . . . . . . . . . . 12 |- ((C x. (APB)) - (((*` C)SB)P((*` C)SB))) = ((C x. (APB)) - ((*` C) x. (C x. ((N` B)^2))))
56	55	opreq2i 3963	. . . . . . . . . . 11 |- ((((N` A)^2) - ((*` C) x. (BPA))) - ((C x. (APB)) - (((*` C)SB)P((*` C)SB)))) = ((((N` A)^2) - ((*` C) x. (BPA))) - ((C x. (APB)) - ((*` C) x. (C x. ((N` B)^2)))))
57	22	recn 5294	. . . . . . . . . . . . . 14 |- (N` A) e. CC
58	57	sqcl 6553	. . . . . . . . . . . . 13 |- ((N` A)^2) e. CC
59	17, 8	mulcl 5301	. . . . . . . . . . . . 13 |- ((*` C) x. (BPA)) e. CC
60	58, 59	pm3.2i 285	. . . . . . . . . . . 12 |- (((N` A)^2) e. CC /\ ((*` C) x. (BPA)) e. CC)
61	17, 14	mulcl 5301	. . . . . . . . . . . . 13 |- ((*` C) x. (C x. ((N` B)^2))) e. CC
62	26, 61	pm3.2i 285	. . . . . . . . . . . 12