Step |
Hyp |
Ref |
Expression |
1 |
|
nvabs.1 |
|- X = ( BaseSet ` U ) |
2 |
|
nvabs.2 |
|- G = ( +v ` U ) |
3 |
|
nvabs.4 |
|- S = ( .sOLD ` U ) |
4 |
|
nvabs.6 |
|- N = ( normCV ` U ) |
5 |
1 2 3 4
|
nvdif |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) = ( N ` ( B G ( -u 1 S A ) ) ) ) |
6 |
5
|
negeqd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( N ` ( A G ( -u 1 S B ) ) ) = -u ( N ` ( B G ( -u 1 S A ) ) ) ) |
7 |
1 4
|
nvcl |
|- ( ( U e. NrmCVec /\ B e. X ) -> ( N ` B ) e. RR ) |
8 |
7
|
3adant2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` B ) e. RR ) |
9 |
1 4
|
nvcl |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR ) |
10 |
9
|
3adant3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` A ) e. RR ) |
11 |
|
simp1 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> U e. NrmCVec ) |
12 |
|
neg1cn |
|- -u 1 e. CC |
13 |
1 3
|
nvscl |
|- ( ( U e. NrmCVec /\ -u 1 e. CC /\ A e. X ) -> ( -u 1 S A ) e. X ) |
14 |
12 13
|
mp3an2 |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S A ) e. X ) |
15 |
14
|
3adant2 |
|- ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( -u 1 S A ) e. X ) |
16 |
1 2
|
nvgcl |
|- ( ( U e. NrmCVec /\ B e. X /\ ( -u 1 S A ) e. X ) -> ( B G ( -u 1 S A ) ) e. X ) |
17 |
15 16
|
syld3an3 |
|- ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( B G ( -u 1 S A ) ) e. X ) |
18 |
17
|
3com23 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( B G ( -u 1 S A ) ) e. X ) |
19 |
1 4
|
nvcl |
|- ( ( U e. NrmCVec /\ ( B G ( -u 1 S A ) ) e. X ) -> ( N ` ( B G ( -u 1 S A ) ) ) e. RR ) |
20 |
11 18 19
|
syl2anc |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( B G ( -u 1 S A ) ) ) e. RR ) |
21 |
20
|
renegcld |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( N ` ( B G ( -u 1 S A ) ) ) e. RR ) |
22 |
1 2
|
nvcom |
|- ( ( U e. NrmCVec /\ A e. X /\ ( B G ( -u 1 S A ) ) e. X ) -> ( A G ( B G ( -u 1 S A ) ) ) = ( ( B G ( -u 1 S A ) ) G A ) ) |
23 |
18 22
|
syld3an3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( B G ( -u 1 S A ) ) ) = ( ( B G ( -u 1 S A ) ) G A ) ) |
24 |
|
simprr |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> B e. X ) |
25 |
14
|
adantrr |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( -u 1 S A ) e. X ) |
26 |
|
simprl |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> A e. X ) |
27 |
24 25 26
|
3jca |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( B e. X /\ ( -u 1 S A ) e. X /\ A e. X ) ) |
28 |
1 2
|
nvass |
|- ( ( U e. NrmCVec /\ ( B e. X /\ ( -u 1 S A ) e. X /\ A e. X ) ) -> ( ( B G ( -u 1 S A ) ) G A ) = ( B G ( ( -u 1 S A ) G A ) ) ) |
29 |
27 28
|
syldan |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( ( B G ( -u 1 S A ) ) G A ) = ( B G ( ( -u 1 S A ) G A ) ) ) |
30 |
29
|
3impb |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( B G ( -u 1 S A ) ) G A ) = ( B G ( ( -u 1 S A ) G A ) ) ) |
31 |
|
eqid |
|- ( 0vec ` U ) = ( 0vec ` U ) |
32 |
1 2 3 31
|
nvlinv |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( -u 1 S A ) G A ) = ( 0vec ` U ) ) |
33 |
32
|
3adant3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( -u 1 S A ) G A ) = ( 0vec ` U ) ) |
34 |
33
|
oveq2d |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( B G ( ( -u 1 S A ) G A ) ) = ( B G ( 0vec ` U ) ) ) |
35 |
1 2 31
|
nv0rid |
|- ( ( U e. NrmCVec /\ B e. X ) -> ( B G ( 0vec ` U ) ) = B ) |
36 |
35
|
3adant2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( B G ( 0vec ` U ) ) = B ) |
37 |
30 34 36
|
3eqtrd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( B G ( -u 1 S A ) ) G A ) = B ) |
38 |
23 37
|
eqtrd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( B G ( -u 1 S A ) ) ) = B ) |
39 |
38
|
fveq2d |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( B G ( -u 1 S A ) ) ) ) = ( N ` B ) ) |
40 |
1 2 4
|
nvtri |
|- ( ( U e. NrmCVec /\ A e. X /\ ( B G ( -u 1 S A ) ) e. X ) -> ( N ` ( A G ( B G ( -u 1 S A ) ) ) ) <_ ( ( N ` A ) + ( N ` ( B G ( -u 1 S A ) ) ) ) ) |
41 |
18 40
|
syld3an3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( B G ( -u 1 S A ) ) ) ) <_ ( ( N ` A ) + ( N ` ( B G ( -u 1 S A ) ) ) ) ) |
42 |
39 41
|
eqbrtrrd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` B ) <_ ( ( N ` A ) + ( N ` ( B G ( -u 1 S A ) ) ) ) ) |
43 |
10
|
recnd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` A ) e. CC ) |
44 |
20
|
recnd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( B G ( -u 1 S A ) ) ) e. CC ) |
45 |
43 44
|
subnegd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` A ) - -u ( N ` ( B G ( -u 1 S A ) ) ) ) = ( ( N ` A ) + ( N ` ( B G ( -u 1 S A ) ) ) ) ) |
46 |
42 45
|
breqtrrd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` B ) <_ ( ( N ` A ) - -u ( N ` ( B G ( -u 1 S A ) ) ) ) ) |
47 |
8 10 21 46
|
lesubd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( N ` ( B G ( -u 1 S A ) ) ) <_ ( ( N ` A ) - ( N ` B ) ) ) |
48 |
6 47
|
eqbrtrd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( N ` ( A G ( -u 1 S B ) ) ) <_ ( ( N ` A ) - ( N ` B ) ) ) |
49 |
|
simp2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> A e. X ) |
50 |
1 3
|
nvscl |
|- ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 S B ) e. X ) |
51 |
12 50
|
mp3an2 |
|- ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 S B ) e. X ) |
52 |
51
|
3adant2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S B ) e. X ) |
53 |
|
simp3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> B e. X ) |
54 |
1 2
|
nvass |
|- ( ( U e. NrmCVec /\ ( A e. X /\ ( -u 1 S B ) e. X /\ B e. X ) ) -> ( ( A G ( -u 1 S B ) ) G B ) = ( A G ( ( -u 1 S B ) G B ) ) ) |
55 |
11 49 52 53 54
|
syl13anc |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G ( -u 1 S B ) ) G B ) = ( A G ( ( -u 1 S B ) G B ) ) ) |
56 |
1 2 3 31
|
nvlinv |
|- ( ( U e. NrmCVec /\ B e. X ) -> ( ( -u 1 S B ) G B ) = ( 0vec ` U ) ) |
57 |
56
|
3adant2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( -u 1 S B ) G B ) = ( 0vec ` U ) ) |
58 |
57
|
oveq2d |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( ( -u 1 S B ) G B ) ) = ( A G ( 0vec ` U ) ) ) |
59 |
1 2 31
|
nv0rid |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( 0vec ` U ) ) = A ) |
60 |
59
|
3adant3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( 0vec ` U ) ) = A ) |
61 |
55 58 60
|
3eqtrd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G ( -u 1 S B ) ) G B ) = A ) |
62 |
61
|
fveq2d |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( ( A G ( -u 1 S B ) ) G B ) ) = ( N ` A ) ) |
63 |
1 2
|
nvgcl |
|- ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 S B ) e. X ) -> ( A G ( -u 1 S B ) ) e. X ) |
64 |
52 63
|
syld3an3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( -u 1 S B ) ) e. X ) |
65 |
1 2 4
|
nvtri |
|- ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ B e. X ) -> ( N ` ( ( A G ( -u 1 S B ) ) G B ) ) <_ ( ( N ` ( A G ( -u 1 S B ) ) ) + ( N ` B ) ) ) |
66 |
64 65
|
syld3an2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( ( A G ( -u 1 S B ) ) G B ) ) <_ ( ( N ` ( A G ( -u 1 S B ) ) ) + ( N ` B ) ) ) |
67 |
62 66
|
eqbrtrrd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` A ) <_ ( ( N ` ( A G ( -u 1 S B ) ) ) + ( N ` B ) ) ) |
68 |
1 4
|
nvcl |
|- ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) e. RR ) |
69 |
11 64 68
|
syl2anc |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) e. RR ) |
70 |
10 8 69
|
lesubaddd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( N ` A ) - ( N ` B ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) <-> ( N ` A ) <_ ( ( N ` ( A G ( -u 1 S B ) ) ) + ( N ` B ) ) ) ) |
71 |
67 70
|
mpbird |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) ) |
72 |
10 8
|
resubcld |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) e. RR ) |
73 |
72 69
|
absled |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) <-> ( -u ( N ` ( A G ( -u 1 S B ) ) ) <_ ( ( N ` A ) - ( N ` B ) ) /\ ( ( N ` A ) - ( N ` B ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) ) ) ) |
74 |
48 71 73
|
mpbir2and |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) ) |