Step |
Hyp |
Ref |
Expression |
1 |
|
bcs.1 |
|- A e. ~H |
2 |
|
bcs.2 |
|- B e. ~H |
3 |
|
fveq2 |
|- ( ( A .ih B ) = 0 -> ( abs ` ( A .ih B ) ) = ( abs ` 0 ) ) |
4 |
|
abs0 |
|- ( abs ` 0 ) = 0 |
5 |
|
normge0 |
|- ( A e. ~H -> 0 <_ ( normh ` A ) ) |
6 |
1 5
|
ax-mp |
|- 0 <_ ( normh ` A ) |
7 |
|
normge0 |
|- ( B e. ~H -> 0 <_ ( normh ` B ) ) |
8 |
2 7
|
ax-mp |
|- 0 <_ ( normh ` B ) |
9 |
1
|
normcli |
|- ( normh ` A ) e. RR |
10 |
2
|
normcli |
|- ( normh ` B ) e. RR |
11 |
9 10
|
mulge0i |
|- ( ( 0 <_ ( normh ` A ) /\ 0 <_ ( normh ` B ) ) -> 0 <_ ( ( normh ` A ) x. ( normh ` B ) ) ) |
12 |
6 8 11
|
mp2an |
|- 0 <_ ( ( normh ` A ) x. ( normh ` B ) ) |
13 |
4 12
|
eqbrtri |
|- ( abs ` 0 ) <_ ( ( normh ` A ) x. ( normh ` B ) ) |
14 |
3 13
|
eqbrtrdi |
|- ( ( A .ih B ) = 0 -> ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) ) |
15 |
|
df-ne |
|- ( ( A .ih B ) =/= 0 <-> -. ( A .ih B ) = 0 ) |
16 |
2 1
|
his1i |
|- ( B .ih A ) = ( * ` ( A .ih B ) ) |
17 |
16
|
oveq2i |
|- ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) = ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( * ` ( A .ih B ) ) ) |
18 |
17
|
oveq2i |
|- ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) ) = ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( * ` ( A .ih B ) ) ) ) |
19 |
1 2
|
hicli |
|- ( A .ih B ) e. CC |
20 |
|
abslem2 |
|- ( ( ( A .ih B ) e. CC /\ ( A .ih B ) =/= 0 ) -> ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( * ` ( A .ih B ) ) ) ) = ( 2 x. ( abs ` ( A .ih B ) ) ) ) |
21 |
19 20
|
mpan |
|- ( ( A .ih B ) =/= 0 -> ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( * ` ( A .ih B ) ) ) ) = ( 2 x. ( abs ` ( A .ih B ) ) ) ) |
22 |
18 21
|
eqtr2id |
|- ( ( A .ih B ) =/= 0 -> ( 2 x. ( abs ` ( A .ih B ) ) ) = ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) ) ) |
23 |
19
|
abs00i |
|- ( ( abs ` ( A .ih B ) ) = 0 <-> ( A .ih B ) = 0 ) |
24 |
23
|
necon3bii |
|- ( ( abs ` ( A .ih B ) ) =/= 0 <-> ( A .ih B ) =/= 0 ) |
25 |
19
|
abscli |
|- ( abs ` ( A .ih B ) ) e. RR |
26 |
25
|
recni |
|- ( abs ` ( A .ih B ) ) e. CC |
27 |
19 26
|
divclzi |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) e. CC ) |
28 |
19 26
|
divreczi |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) = ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) |
29 |
28
|
fveq2d |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = ( abs ` ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) ) |
30 |
26
|
recclzi |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( 1 / ( abs ` ( A .ih B ) ) ) e. CC ) |
31 |
|
absmul |
|- ( ( ( A .ih B ) e. CC /\ ( 1 / ( abs ` ( A .ih B ) ) ) e. CC ) -> ( abs ` ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) = ( ( abs ` ( A .ih B ) ) x. ( abs ` ( 1 / ( abs ` ( A .ih B ) ) ) ) ) ) |
32 |
19 30 31
|
sylancr |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) = ( ( abs ` ( A .ih B ) ) x. ( abs ` ( 1 / ( abs ` ( A .ih B ) ) ) ) ) ) |
33 |
25
|
rerecclzi |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( 1 / ( abs ` ( A .ih B ) ) ) e. RR ) |
34 |
|
0re |
|- 0 e. RR |
35 |
33 34
|
jctil |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( 0 e. RR /\ ( 1 / ( abs ` ( A .ih B ) ) ) e. RR ) ) |
36 |
19
|
absgt0i |
|- ( ( A .ih B ) =/= 0 <-> 0 < ( abs ` ( A .ih B ) ) ) |
37 |
24 36
|
bitri |
|- ( ( abs ` ( A .ih B ) ) =/= 0 <-> 0 < ( abs ` ( A .ih B ) ) ) |
38 |
25
|
recgt0i |
|- ( 0 < ( abs ` ( A .ih B ) ) -> 0 < ( 1 / ( abs ` ( A .ih B ) ) ) ) |
39 |
37 38
|
sylbi |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> 0 < ( 1 / ( abs ` ( A .ih B ) ) ) ) |
40 |
|
ltle |
|- ( ( 0 e. RR /\ ( 1 / ( abs ` ( A .ih B ) ) ) e. RR ) -> ( 0 < ( 1 / ( abs ` ( A .ih B ) ) ) -> 0 <_ ( 1 / ( abs ` ( A .ih B ) ) ) ) ) |
41 |
35 39 40
|
sylc |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> 0 <_ ( 1 / ( abs ` ( A .ih B ) ) ) ) |
42 |
33 41
|
absidd |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( 1 / ( abs ` ( A .ih B ) ) ) ) = ( 1 / ( abs ` ( A .ih B ) ) ) ) |
43 |
42
|
oveq2d |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( abs ` ( A .ih B ) ) x. ( abs ` ( 1 / ( abs ` ( A .ih B ) ) ) ) ) = ( ( abs ` ( A .ih B ) ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) |
44 |
32 43
|
eqtrd |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( ( A .ih B ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) = ( ( abs ` ( A .ih B ) ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) ) |
45 |
26
|
recidzi |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( abs ` ( A .ih B ) ) x. ( 1 / ( abs ` ( A .ih B ) ) ) ) = 1 ) |
46 |
29 44 45
|
3eqtrd |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = 1 ) |
47 |
27 46
|
jca |
|- ( ( abs ` ( A .ih B ) ) =/= 0 -> ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) e. CC /\ ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = 1 ) ) |
48 |
24 47
|
sylbir |
|- ( ( A .ih B ) =/= 0 -> ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) e. CC /\ ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = 1 ) ) |
49 |
1 2
|
normlem7tALT |
|- ( ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) e. CC /\ ( abs ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) = 1 ) -> ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) ) |
50 |
48 49
|
syl |
|- ( ( A .ih B ) =/= 0 -> ( ( ( * ` ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) ) x. ( A .ih B ) ) + ( ( ( A .ih B ) / ( abs ` ( A .ih B ) ) ) x. ( B .ih A ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) ) |
51 |
22 50
|
eqbrtrd |
|- ( ( A .ih B ) =/= 0 -> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) ) |
52 |
15 51
|
sylbir |
|- ( -. ( A .ih B ) = 0 -> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) ) |
53 |
10
|
recni |
|- ( normh ` B ) e. CC |
54 |
9
|
recni |
|- ( normh ` A ) e. CC |
55 |
|
normval |
|- ( B e. ~H -> ( normh ` B ) = ( sqrt ` ( B .ih B ) ) ) |
56 |
2 55
|
ax-mp |
|- ( normh ` B ) = ( sqrt ` ( B .ih B ) ) |
57 |
|
normval |
|- ( A e. ~H -> ( normh ` A ) = ( sqrt ` ( A .ih A ) ) ) |
58 |
1 57
|
ax-mp |
|- ( normh ` A ) = ( sqrt ` ( A .ih A ) ) |
59 |
56 58
|
oveq12i |
|- ( ( normh ` B ) x. ( normh ` A ) ) = ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) |
60 |
53 54 59
|
mulcomli |
|- ( ( normh ` A ) x. ( normh ` B ) ) = ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) |
61 |
60
|
breq2i |
|- ( ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) <-> ( abs ` ( A .ih B ) ) <_ ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) |
62 |
|
2pos |
|- 0 < 2 |
63 |
|
hiidge0 |
|- ( B e. ~H -> 0 <_ ( B .ih B ) ) |
64 |
|
hiidrcl |
|- ( B e. ~H -> ( B .ih B ) e. RR ) |
65 |
2 64
|
ax-mp |
|- ( B .ih B ) e. RR |
66 |
65
|
sqrtcli |
|- ( 0 <_ ( B .ih B ) -> ( sqrt ` ( B .ih B ) ) e. RR ) |
67 |
2 63 66
|
mp2b |
|- ( sqrt ` ( B .ih B ) ) e. RR |
68 |
|
hiidge0 |
|- ( A e. ~H -> 0 <_ ( A .ih A ) ) |
69 |
|
hiidrcl |
|- ( A e. ~H -> ( A .ih A ) e. RR ) |
70 |
1 69
|
ax-mp |
|- ( A .ih A ) e. RR |
71 |
70
|
sqrtcli |
|- ( 0 <_ ( A .ih A ) -> ( sqrt ` ( A .ih A ) ) e. RR ) |
72 |
1 68 71
|
mp2b |
|- ( sqrt ` ( A .ih A ) ) e. RR |
73 |
67 72
|
remulcli |
|- ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) e. RR |
74 |
|
2re |
|- 2 e. RR |
75 |
25 73 74
|
lemul2i |
|- ( 0 < 2 -> ( ( abs ` ( A .ih B ) ) <_ ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) <-> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) ) ) |
76 |
62 75
|
ax-mp |
|- ( ( abs ` ( A .ih B ) ) <_ ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) <-> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) ) |
77 |
61 76
|
bitri |
|- ( ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) <-> ( 2 x. ( abs ` ( A .ih B ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) ) |
78 |
52 77
|
sylibr |
|- ( -. ( A .ih B ) = 0 -> ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) ) |
79 |
14 78
|
pm2.61i |
|- ( abs ` ( A .ih B ) ) <_ ( ( normh ` A ) x. ( normh ` B ) ) |