Theorem siilem1

Description: Lemma for sii . (Contributed by NM, 23-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	siii.1	|- X = ( BaseSet ` U )
	siii.6	|- N = ( normCV ` U )
	siii.7	|- P = ( .iOLD ` U )
	siii.9	|- U e. CPreHilOLD
	siii.a	|- A e. X
	siii.b	|- B e. X
	sii1.3	|- M = ( -v ` U )
	sii1.4	|- S = ( .sOLD ` U )
	sii1.c	|- C e. CC
	sii1.r	|- ( C x. ( A P B ) ) e. RR
	sii1.z	|- 0 <_ ( C x. ( A P B ) )
Assertion	siilem1	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		siii.1	|- X = ( BaseSet ` U )
2		siii.6	|- N = ( normCV ` U )
3		siii.7	|- P = ( .iOLD ` U )
4		siii.9	|- U e. CPreHilOLD
5		siii.a	|- A e. X
6		siii.b	|- B e. X
7		sii1.3	|- M = ( -v ` U )
8		sii1.4	|- S = ( .sOLD ` U )
9		sii1.c	|- C e. CC
10		sii1.r	|- ( C x. ( A P B ) ) e. RR
11		sii1.z	|- 0 <_ ( C x. ( A P B ) )
12	4	phnvi	|- U e. NrmCVec
13	9	cjcli	|- ( * ` C ) e. CC
14	1 8	nvscl	|- ( ( U e. NrmCVec /\ ( * ` C ) e. CC /\ B e. X ) -> ( ( * ` C ) S B ) e. X )
15	12 13 6 14	mp3an	|- ( ( * ` C ) S B ) e. X
16	1 7	nvmcl	|- ( ( U e. NrmCVec /\ A e. X /\ ( ( * ` C ) S B ) e. X ) -> ( A M ( ( * ` C ) S B ) ) e. X )
17	12 5 15 16	mp3an	|- ( A M ( ( * ` C ) S B ) ) e. X
18	1 2 12 17	nvcli	|- ( N ` ( A M ( ( * ` C ) S B ) ) ) e. RR
19	18	sqge0i	|- 0 <_ ( ( N ` ( A M ( ( * ` C ) S B ) ) ) ^ 2 )
20	17 5 15	3pm3.2i	|- ( ( A M ( ( * ` C ) S B ) ) e. X /\ A e. X /\ ( ( * ` C ) S B ) e. X )
21	1 7 3	dipsubdi	|- ( ( U e. CPreHilOLD /\ ( ( A M ( ( * ` C ) S B ) ) e. X /\ A e. X /\ ( ( * ` C ) S B ) e. X ) ) -> ( ( A M ( ( * ` C ) S B ) ) P ( A M ( ( * ` C ) S B ) ) ) = ( ( ( A M ( ( * ` C ) S B ) ) P A ) - ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) ) )
22	4 20 21	mp2an	|- ( ( A M ( ( * ` C ) S B ) ) P ( A M ( ( * ` C ) S B ) ) ) = ( ( ( A M ( ( * ` C ) S B ) ) P A ) - ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) )
23	1 2 3	ipidsq	|- ( ( U e. NrmCVec /\ ( A M ( ( * ` C ) S B ) ) e. X ) -> ( ( A M ( ( * ` C ) S B ) ) P ( A M ( ( * ` C ) S B ) ) ) = ( ( N ` ( A M ( ( * ` C ) S B ) ) ) ^ 2 ) )
24	12 17 23	mp2an	|- ( ( A M ( ( * ` C ) S B ) ) P ( A M ( ( * ` C ) S B ) ) ) = ( ( N ` ( A M ( ( * ` C ) S B ) ) ) ^ 2 )
25	13 6 15	3pm3.2i	|- ( ( * ` C ) e. CC /\ B e. X /\ ( ( * ` C ) S B ) e. X )
26	1 8 3	dipass	|- ( ( U e. CPreHilOLD /\ ( ( * ` C ) e. CC /\ B e. X /\ ( ( * ` C ) S B ) e. X ) ) -> ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) = ( ( * ` C ) x. ( B P ( ( * ` C ) S B ) ) ) )
27	4 25 26	mp2an	|- ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) = ( ( * ` C ) x. ( B P ( ( * ` C ) S B ) ) )
28	6 9 6	3pm3.2i	|- ( B e. X /\ C e. CC /\ B e. X )
29	1 8 3	dipassr2	|- ( ( U e. CPreHilOLD /\ ( B e. X /\ C e. CC /\ B e. X ) ) -> ( B P ( ( * ` C ) S B ) ) = ( C x. ( B P B ) ) )
30	4 28 29	mp2an	|- ( B P ( ( * ` C ) S B ) ) = ( C x. ( B P B ) )
31	1 2 3	ipidsq	|- ( ( U e. NrmCVec /\ B e. X ) -> ( B P B ) = ( ( N ` B ) ^ 2 ) )
32	12 6 31	mp2an	|- ( B P B ) = ( ( N ` B ) ^ 2 )
33	32	oveq2i	|- ( C x. ( B P B ) ) = ( C x. ( ( N ` B ) ^ 2 ) )
34	30 33	eqtri	|- ( B P ( ( * ` C ) S B ) ) = ( C x. ( ( N ` B ) ^ 2 ) )
35	34	oveq2i	|- ( ( * ` C ) x. ( B P ( ( * ` C ) S B ) ) ) = ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) )
36	27 35	eqtri	|- ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) = ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) )
37	36	oveq2i	|- ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) = ( ( C x. ( A P B ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) )
38	37	oveq2i	|- ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
39	1 2 12 5	nvcli	|- ( N ` A ) e. RR
40	39	recni	|- ( N ` A ) e. CC
41	40	sqcli	|- ( ( N ` A ) ^ 2 ) e. CC
42	1 3	dipcl	|- ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( B P A ) e. CC )
43	12 6 5 42	mp3an	|- ( B P A ) e. CC
44	13 43	mulcli	|- ( ( * ` C ) x. ( B P A ) ) e. CC
45	10	recni	|- ( C x. ( A P B ) ) e. CC
46	1 2 12 6	nvcli	|- ( N ` B ) e. RR
47	46	recni	|- ( N ` B ) e. CC
48	47	sqcli	|- ( ( N ` B ) ^ 2 ) e. CC
49	9 48	mulcli	|- ( C x. ( ( N ` B ) ^ 2 ) ) e. CC
50	13 49	mulcli	|- ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) e. CC
51		sub4	|- ( ( ( ( ( N ` A ) ^ 2 ) e. CC /\ ( ( * ` C ) x. ( B P A ) ) e. CC ) /\ ( ( C x. ( A P B ) ) e. CC /\ ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) e. CC ) ) -> ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) )
52	41 44 45 50 51	mp4an	|- ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
53	38 52	eqtri	|- ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
54	5 15 5	3pm3.2i	|- ( A e. X /\ ( ( * ` C ) S B ) e. X /\ A e. X )
55	1 7 3	dipsubdir	|- ( ( U e. CPreHilOLD /\ ( A e. X /\ ( ( * ` C ) S B ) e. X /\ A e. X ) ) -> ( ( A M ( ( * ` C ) S B ) ) P A ) = ( ( A P A ) - ( ( ( * ` C ) S B ) P A ) ) )
56	4 54 55	mp2an	|- ( ( A M ( ( * ` C ) S B ) ) P A ) = ( ( A P A ) - ( ( ( * ` C ) S B ) P A ) )
57	1 2 3	ipidsq	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A P A ) = ( ( N ` A ) ^ 2 ) )
58	12 5 57	mp2an	|- ( A P A ) = ( ( N ` A ) ^ 2 )
59	13 6 5	3pm3.2i	|- ( ( * ` C ) e. CC /\ B e. X /\ A e. X )
60	1 8 3	dipass	|- ( ( U e. CPreHilOLD /\ ( ( * ` C ) e. CC /\ B e. X /\ A e. X ) ) -> ( ( ( * ` C ) S B ) P A ) = ( ( * ` C ) x. ( B P A ) ) )
61	4 59 60	mp2an	|- ( ( ( * ` C ) S B ) P A ) = ( ( * ` C ) x. ( B P A ) )
62	58 61	oveq12i	|- ( ( A P A ) - ( ( ( * ` C ) S B ) P A ) ) = ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) )
63	56 62	eqtri	|- ( ( A M ( ( * ` C ) S B ) ) P A ) = ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) )
64	5 15 15	3pm3.2i	|- ( A e. X /\ ( ( * ` C ) S B ) e. X /\ ( ( * ` C ) S B ) e. X )
65	1 7 3	dipsubdir	|- ( ( U e. CPreHilOLD /\ ( A e. X /\ ( ( * ` C ) S B ) e. X /\ ( ( * ` C ) S B ) e. X ) ) -> ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) = ( ( A P ( ( * ` C ) S B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) )
66	4 64 65	mp2an	|- ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) = ( ( A P ( ( * ` C ) S B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) )
67	5 9 6	3pm3.2i	|- ( A e. X /\ C e. CC /\ B e. X )
68	1 8 3	dipassr2	|- ( ( U e. CPreHilOLD /\ ( A e. X /\ C e. CC /\ B e. X ) ) -> ( A P ( ( * ` C ) S B ) ) = ( C x. ( A P B ) ) )
69	4 67 68	mp2an	|- ( A P ( ( * ` C ) S B ) ) = ( C x. ( A P B ) )
70	69	oveq1i	|- ( ( A P ( ( * ` C ) S B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) = ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) )
71	66 70	eqtri	|- ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) = ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) )
72	63 71	oveq12i	|- ( ( ( A M ( ( * ` C ) S B ) ) P A ) - ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( ( * ` C ) x. ( B P A ) ) ) - ( ( C x. ( A P B ) ) - ( ( ( * ` C ) S B ) P ( ( * ` C ) S B ) ) ) )
73	13 43 49	subdii	|- ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) = ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) )
74	73	oveq2i	|- ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( ( * ` C ) x. ( B P A ) ) - ( ( * ` C ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
75	53 72 74	3eqtr4i	|- ( ( ( A M ( ( * ` C ) S B ) ) P A ) - ( ( A M ( ( * ` C ) S B ) ) P ( ( * ` C ) S B ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
76	22 24 75	3eqtr3i	|- ( ( N ` ( A M ( ( * ` C ) S B ) ) ) ^ 2 ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
77	19 76	breqtri	|- 0 <_ ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) )
78	43 49	subeq0i	|- ( ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) = 0 <-> ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) )
79		oveq2	|- ( ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) = 0 -> ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) = ( ( * ` C ) x. 0 ) )
80	13	mul01i	|- ( ( * ` C ) x. 0 ) = 0
81	79 80	eqtrdi	|- ( ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) = 0 -> ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) = 0 )
82	78 81	sylbir	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) = 0 )
83	82	oveq2d	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - 0 ) )
84	39	resqcli	|- ( ( N ` A ) ^ 2 ) e. RR
85	84	recni	|- ( ( N ` A ) ^ 2 ) e. CC
86	85 45	subcli	|- ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) e. CC
87	86	subid1i	|- ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - 0 ) = ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) )
88	83 87	eqtrdi	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) - ( ( * ` C ) x. ( ( B P A ) - ( C x. ( ( N ` B ) ^ 2 ) ) ) ) ) = ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) )
89	77 88	breqtrid	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> 0 <_ ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) )
90	84 10	subge0i	|- ( 0 <_ ( ( ( N ` A ) ^ 2 ) - ( C x. ( A P B ) ) ) <-> ( C x. ( A P B ) ) <_ ( ( N ` A ) ^ 2 ) )
91	89 90	sylib	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( C x. ( A P B ) ) <_ ( ( N ` A ) ^ 2 ) )
92	46	resqcli	|- ( ( N ` B ) ^ 2 ) e. RR
93	46	sqge0i	|- 0 <_ ( ( N ` B ) ^ 2 )
94	92 93	pm3.2i	|- ( ( ( N ` B ) ^ 2 ) e. RR /\ 0 <_ ( ( N ` B ) ^ 2 ) )
95	10 84 94	3pm3.2i	|- ( ( C x. ( A P B ) ) e. RR /\ ( ( N ` A ) ^ 2 ) e. RR /\ ( ( ( N ` B ) ^ 2 ) e. RR /\ 0 <_ ( ( N ` B ) ^ 2 ) ) )
96		lemul1a	|- ( ( ( ( C x. ( A P B ) ) e. RR /\ ( ( N ` A ) ^ 2 ) e. RR /\ ( ( ( N ` B ) ^ 2 ) e. RR /\ 0 <_ ( ( N ` B ) ^ 2 ) ) ) /\ ( C x. ( A P B ) ) <_ ( ( N ` A ) ^ 2 ) ) -> ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) ^ 2 ) x. ( ( N ` B ) ^ 2 ) ) )
97	95 96	mpan	|- ( ( C x. ( A P B ) ) <_ ( ( N ` A ) ^ 2 ) -> ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) ^ 2 ) x. ( ( N ` B ) ^ 2 ) ) )
98	91 97	syl	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) ^ 2 ) x. ( ( N ` B ) ^ 2 ) ) )
99	40 47	sqmuli	|- ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) = ( ( ( N ` A ) ^ 2 ) x. ( ( N ` B ) ^ 2 ) )
100	98 99	breqtrrdi	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) )
101	10 92	mulge0i	|- ( ( 0 <_ ( C x. ( A P B ) ) /\ 0 <_ ( ( N ` B ) ^ 2 ) ) -> 0 <_ ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) )
102	11 93 101	mp2an	|- 0 <_ ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) )
103	39 46	remulcli	|- ( ( N ` A ) x. ( N ` B ) ) e. RR
104	103	sqge0i	|- 0 <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 )
105	10 92	remulcli	|- ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) e. RR
106	103	resqcli	|- ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) e. RR
107	105 106	sqrtlei	|- ( ( 0 <_ ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) /\ 0 <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) -> ( ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) <-> ( sqrt ` ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) ) <_ ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) ) )
108	102 104 107	mp2an	|- ( ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) <_ ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) <-> ( sqrt ` ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) ) <_ ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) )
109	100 108	sylib	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) ) <_ ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) )
110	1 3	dipcl	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
111	12 5 6 110	mp3an	|- ( A P B ) e. CC
112	9 111	mulcomi	|- ( C x. ( A P B ) ) = ( ( A P B ) x. C )
113	112	oveq1i	|- ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) = ( ( ( A P B ) x. C ) x. ( ( N ` B ) ^ 2 ) )
114	92	recni	|- ( ( N ` B ) ^ 2 ) e. CC
115	111 9 114	mulassi	|- ( ( ( A P B ) x. C ) x. ( ( N ` B ) ^ 2 ) ) = ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) )
116	113 115	eqtri	|- ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) = ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) )
117	116	fveq2i	|- ( sqrt ` ( ( C x. ( A P B ) ) x. ( ( N ` B ) ^ 2 ) ) ) = ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) )
118	1 2	nvge0	|- ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) )
119	12 5 118	mp2an	|- 0 <_ ( N ` A )
120	1 2	nvge0	|- ( ( U e. NrmCVec /\ B e. X ) -> 0 <_ ( N ` B ) )
121	12 6 120	mp2an	|- 0 <_ ( N ` B )
122	39 46	mulge0i	|- ( ( 0 <_ ( N ` A ) /\ 0 <_ ( N ` B ) ) -> 0 <_ ( ( N ` A ) x. ( N ` B ) ) )
123	119 121 122	mp2an	|- 0 <_ ( ( N ` A ) x. ( N ` B ) )
124	103	sqrtsqi	|- ( 0 <_ ( ( N ` A ) x. ( N ` B ) ) -> ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) = ( ( N ` A ) x. ( N ` B ) ) )
125	123 124	ax-mp	|- ( sqrt ` ( ( ( N ` A ) x. ( N ` B ) ) ^ 2 ) ) = ( ( N ` A ) x. ( N ` B ) )
126	109 117 125	3brtr3g	|- ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) )