Theorem siilem2 8512

Description: Lemma for sii 8514.

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
siii2.3	|- M = (-v` U)
siii2.4	|- S = (.s` U)

Assertion

Ref	Expression
siilem2	|- ((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))) -> ((BPA) = (C x. ((N` B)^2)) -> (sqr` ((APB) x. (C x. ((N` B)^2)))) <_ ((N` A) x. (N` B))))

Proof of Theorem siilem2

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . 4 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> (C x. ((N` B)^2)) = (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. ((N` B)^2)))
2	1	eqeq2d 1486	. . 3 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> ((BPA) = (C x. ((N` B)^2)) <-> (BPA) = (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. ((N` B)^2))))
3	1	opreq2d 3976	. . . . 5 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> ((APB) x. (C x. ((N` B)^2))) = ((APB) x. (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. ((N` B)^2))))
4	3	fveq2d 3728	. . . 4 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> (sqr` ((APB) x. (C x. ((N` B)^2)))) = (sqr` ((APB) x. (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. ((N` B)^2)))))
5	4	breq1d 2629	. . 3 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> ((sqr` ((APB) x. (C x. ((N` B)^2)))) <_ ((N` A) x. (N` B)) <-> (sqr` ((APB) x. (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. ((N` B)^2)))) <_ ((N` A) x. (N` B))))
6	2, 5	imbi12d 626	. 2 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> (((BPA) = (C x. ((N` B)^2)) -> (sqr` ((APB) x. (C x. ((N` B)^2)))) <_ ((N` A) x. (N` B))) <-> ((BPA) = (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. ((N` B)^2)) -> (sqr` ((APB) x. (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. ((N` B)^2)))) <_ ((N` A) x. (N` B)))))
7		siii.1	. . 3 |- X = (Base` U)
8		siii.6	. . 3 |- N = (norm` U)
9		siii.7	. . 3 |- P = (.i` U)
10		siii.9	. . 3 |- U e. CPreHil
11		siii.a	. . 3 |- A e. X
12		siii.b	. . 3 |- B e. X
13		siii2.3	. . 3 |- M = (-v` U)
14		siii2.4	. . 3 |- S = (.s` U)
15		eleq1 1534	. . . . . 6 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> (C e. CC <-> if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) e. CC))
16		opreq1 3968	. . . . . . 7 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> (C x. (APB)) = (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. (APB)))
17	16	eleq1d 1540	. . . . . 6 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> ((C x. (APB)) e. RR <-> (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. (APB)) e. RR))
18	16	breq2d 2630	. . . . . 6 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> (0 <_ (C x. (APB)) <-> 0 <_ (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. (APB))))
19	15, 17, 18	3anbi123d 893	. . . . 5 |- (C = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> ((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))) <-> (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) e. CC /\ (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. (APB)) e. RR /\ 0 <_ (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. (APB)))))
20		eleq1 1534	. . . . . 6 |- (0 = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> (0 e. CC <-> if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) e. CC))
21		opreq1 3968	. . . . . . 7 |- (0 = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> (0 x. (APB)) = (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. (APB)))
22	21	eleq1d 1540	. . . . . 6 |- (0 = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> ((0 x. (APB)) e. RR <-> (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. (APB)) e. RR))
23	21	breq2d 2630	. . . . . 6 |- (0 = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> (0 <_ (0 x. (APB)) <-> 0 <_ (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. (APB))))
24	20, 22, 23	3anbi123d 893	. . . . 5 |- (0 = if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) -> ((0 e. CC /\ (0 x. (APB)) e. RR /\ 0 <_ (0 x. (APB))) <-> (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) e. CC /\ (if((C e. CC /\ (C x. (APB)) e. RR /\ 0 <_ (C x. (APB))), C, 0) x. (APB)) e. RR /\