Metamath Proof Explorer

Theorem siilem2

Description: Lemma for sii . (Contributed by NM, 24-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
siii2.3 
|- M = ( -v ` U )
siii2.4 
|- S = ( .sOLD ` U )
Assertion siilem2 
|- ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) -> ( ( 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 siii2.3 
 |-  M = ( -v ` U )
8 siii2.4 
 |-  S = ( .sOLD ` U )
9 oveq1 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( C x. ( ( N ` B ) ^ 2 ) ) = ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( ( N ` B ) ^ 2 ) ) )
10 9 eqeq2d 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) <-> ( B P A ) = ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( ( N ` B ) ^ 2 ) ) ) )
11 9 oveq2d 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) = ( ( A P B ) x. ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( ( N ` B ) ^ 2 ) ) ) )
12 11 fveq2d 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) = ( sqrt ` ( ( A P B ) x. ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( ( N ` B ) ^ 2 ) ) ) ) )
13 12 breq1d 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) <-> ( sqrt ` ( ( A P B ) x. ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) ) )
14 10 13 imbi12d 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) ) <-> ( ( B P A ) = ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) ) ) )
15 eleq1 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( C e. CC <-> if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) e. CC ) )
16 oveq1 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( C x. ( A P B ) ) = ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) )
17 16 eleq1d 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( ( C x. ( A P B ) ) e. RR <-> ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) e. RR ) )
18 16 breq2d 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( 0 <_ ( C x. ( A P B ) ) <-> 0 <_ ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) ) )
19 15 17 18 3anbi123d 
 |-  ( C = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) <-> ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) e. CC /\ ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) e. RR /\ 0 <_ ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) ) ) )
20 eleq1 
 |-  ( 0 = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( 0 e. CC <-> if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) e. CC ) )
21 oveq1 
 |-  ( 0 = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( 0 x. ( A P B ) ) = ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) )
22 21 eleq1d 
 |-  ( 0 = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( ( 0 x. ( A P B ) ) e. RR <-> ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) e. RR ) )
23 21 breq2d 
 |-  ( 0 = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( 0 <_ ( 0 x. ( A P B ) ) <-> 0 <_ ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) ) )
24 20 22 23 3anbi123d 
 |-  ( 0 = if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) -> ( ( 0 e. CC /\ ( 0 x. ( A P B ) ) e. RR /\ 0 <_ ( 0 x. ( A P B ) ) ) <-> ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) e. CC /\ ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) e. RR /\ 0 <_ ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) ) ) )
25 0cn 
 |-  0 e. CC
26 4 phnvi 
 |-  U e. NrmCVec
27 1 3 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
28 26 5 6 27 mp3an 
 |-  ( A P B ) e. CC
29 28 mul02i 
 |-  ( 0 x. ( A P B ) ) = 0
30 0re 
 |-  0 e. RR
31 29 30 eqeltri 
 |-  ( 0 x. ( A P B ) ) e. RR
32 0le0 
 |-  0 <_ 0
33 32 29 breqtrri 
 |-  0 <_ ( 0 x. ( A P B ) )
34 25 31 33 3pm3.2i 
 |-  ( 0 e. CC /\ ( 0 x. ( A P B ) ) e. RR /\ 0 <_ ( 0 x. ( A P B ) ) )
35 19 24 34 elimhyp 
 |-  ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) e. CC /\ ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) e. RR /\ 0 <_ ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) )
36 35 simp1i 
 |-  if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) e. CC
37 35 simp2i 
 |-  ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) ) e. RR
38 35 simp3i 
 |-  0 <_ ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( A P B ) )
39 1 2 3 4 5 6 7 8 36 37 38 siilem1 
 |-  ( ( B P A ) = ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( if ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) , C , 0 ) x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) )
40 14 39 dedth 
 |-  ( ( C e. CC /\ ( C x. ( A P B ) ) e. RR /\ 0 <_ ( C x. ( A P B ) ) ) -> ( ( B P A ) = ( C x. ( ( N ` B ) ^ 2 ) ) -> ( sqrt ` ( ( A P B ) x. ( C x. ( ( N ` B ) ^ 2 ) ) ) ) <_ ( ( N ` A ) x. ( N ` B ) ) ) )