Step |
Hyp |
Ref |
Expression |
1 |
|
ncvsprp.v |
โข ๐ = ( Base โ ๐ ) |
2 |
|
ncvsprp.n |
โข ๐ = ( norm โ ๐ ) |
3 |
|
ncvsprp.s |
โข ยท = ( ยท๐ โ ๐ ) |
4 |
|
ncvsdif.p |
โข + = ( +g โ ๐ ) |
5 |
|
ncvspi.f |
โข ๐น = ( Scalar โ ๐ ) |
6 |
|
ncvspi.k |
โข ๐พ = ( Base โ ๐น ) |
7 |
|
elin |
โข ( ๐ โ ( NrmVec โฉ โVec ) โ ( ๐ โ NrmVec โง ๐ โ โVec ) ) |
8 |
|
nvcnlm |
โข ( ๐ โ NrmVec โ ๐ โ NrmMod ) |
9 |
|
nlmngp |
โข ( ๐ โ NrmMod โ ๐ โ NrmGrp ) |
10 |
8 9
|
syl |
โข ( ๐ โ NrmVec โ ๐ โ NrmGrp ) |
11 |
10
|
adantr |
โข ( ( ๐ โ NrmVec โง ๐ โ โVec ) โ ๐ โ NrmGrp ) |
12 |
7 11
|
sylbi |
โข ( ๐ โ ( NrmVec โฉ โVec ) โ ๐ โ NrmGrp ) |
13 |
12
|
3ad2ant1 |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ๐ โ NrmGrp ) |
14 |
|
nvclmod |
โข ( ๐ โ NrmVec โ ๐ โ LMod ) |
15 |
|
lmodgrp |
โข ( ๐ โ LMod โ ๐ โ Grp ) |
16 |
14 15
|
syl |
โข ( ๐ โ NrmVec โ ๐ โ Grp ) |
17 |
16
|
adantr |
โข ( ( ๐ โ NrmVec โง ๐ โ โVec ) โ ๐ โ Grp ) |
18 |
7 17
|
sylbi |
โข ( ๐ โ ( NrmVec โฉ โVec ) โ ๐ โ Grp ) |
19 |
18
|
3ad2ant1 |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ๐ โ Grp ) |
20 |
|
simp2l |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ๐ด โ ๐ ) |
21 |
|
id |
โข ( ๐ โ โVec โ ๐ โ โVec ) |
22 |
21
|
cvsclm |
โข ( ๐ โ โVec โ ๐ โ โMod ) |
23 |
7 22
|
simplbiim |
โข ( ๐ โ ( NrmVec โฉ โVec ) โ ๐ โ โMod ) |
24 |
23
|
3ad2ant1 |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ๐ โ โMod ) |
25 |
|
simp3 |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ i โ ๐พ ) |
26 |
|
simp2r |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ๐ต โ ๐ ) |
27 |
1 5 3 6
|
clmvscl |
โข ( ( ๐ โ โMod โง i โ ๐พ โง ๐ต โ ๐ ) โ ( i ยท ๐ต ) โ ๐ ) |
28 |
24 25 26 27
|
syl3anc |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( i ยท ๐ต ) โ ๐ ) |
29 |
1 4
|
grpcl |
โข ( ( ๐ โ Grp โง ๐ด โ ๐ โง ( i ยท ๐ต ) โ ๐ ) โ ( ๐ด + ( i ยท ๐ต ) ) โ ๐ ) |
30 |
19 20 28 29
|
syl3anc |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ๐ด + ( i ยท ๐ต ) ) โ ๐ ) |
31 |
1 2
|
nmcl |
โข ( ( ๐ โ NrmGrp โง ( ๐ด + ( i ยท ๐ต ) ) โ ๐ ) โ ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) โ โ ) |
32 |
13 30 31
|
syl2anc |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) โ โ ) |
33 |
32
|
recnd |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) โ โ ) |
34 |
33
|
mulid2d |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( 1 ยท ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) ) = ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) ) |
35 |
|
ax-icn |
โข i โ โ |
36 |
35
|
absnegi |
โข ( abs โ - i ) = ( abs โ i ) |
37 |
|
absi |
โข ( abs โ i ) = 1 |
38 |
36 37
|
eqtri |
โข ( abs โ - i ) = 1 |
39 |
38
|
oveq1i |
โข ( ( abs โ - i ) ยท ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) ) = ( 1 ยท ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) ) |
40 |
|
simp1 |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ๐ โ ( NrmVec โฉ โVec ) ) |
41 |
5 6
|
clmneg |
โข ( ( ๐ โ โMod โง i โ ๐พ ) โ - i = ( ( invg โ ๐น ) โ i ) ) |
42 |
22 41
|
sylan |
โข ( ( ๐ โ โVec โง i โ ๐พ ) โ - i = ( ( invg โ ๐น ) โ i ) ) |
43 |
5
|
clmfgrp |
โข ( ๐ โ โMod โ ๐น โ Grp ) |
44 |
22 43
|
syl |
โข ( ๐ โ โVec โ ๐น โ Grp ) |
45 |
|
eqid |
โข ( invg โ ๐น ) = ( invg โ ๐น ) |
46 |
6 45
|
grpinvcl |
โข ( ( ๐น โ Grp โง i โ ๐พ ) โ ( ( invg โ ๐น ) โ i ) โ ๐พ ) |
47 |
44 46
|
sylan |
โข ( ( ๐ โ โVec โง i โ ๐พ ) โ ( ( invg โ ๐น ) โ i ) โ ๐พ ) |
48 |
42 47
|
eqeltrd |
โข ( ( ๐ โ โVec โง i โ ๐พ ) โ - i โ ๐พ ) |
49 |
48
|
ex |
โข ( ๐ โ โVec โ ( i โ ๐พ โ - i โ ๐พ ) ) |
50 |
7 49
|
simplbiim |
โข ( ๐ โ ( NrmVec โฉ โVec ) โ ( i โ ๐พ โ - i โ ๐พ ) ) |
51 |
50
|
imp |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง i โ ๐พ ) โ - i โ ๐พ ) |
52 |
51
|
3adant2 |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ - i โ ๐พ ) |
53 |
1 2 3 5 6
|
ncvsprp |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง - i โ ๐พ โง ( ๐ด + ( i ยท ๐ต ) ) โ ๐ ) โ ( ๐ โ ( - i ยท ( ๐ด + ( i ยท ๐ต ) ) ) ) = ( ( abs โ - i ) ยท ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) ) ) |
54 |
40 52 30 53
|
syl3anc |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ๐ โ ( - i ยท ( ๐ด + ( i ยท ๐ต ) ) ) ) = ( ( abs โ - i ) ยท ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) ) ) |
55 |
1 5 3 6 4
|
clmvsdi |
โข ( ( ๐ โ โMod โง ( - i โ ๐พ โง ๐ด โ ๐ โง ( i ยท ๐ต ) โ ๐ ) ) โ ( - i ยท ( ๐ด + ( i ยท ๐ต ) ) ) = ( ( - i ยท ๐ด ) + ( - i ยท ( i ยท ๐ต ) ) ) ) |
56 |
24 52 20 28 55
|
syl13anc |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( - i ยท ( ๐ด + ( i ยท ๐ต ) ) ) = ( ( - i ยท ๐ด ) + ( - i ยท ( i ยท ๐ต ) ) ) ) |
57 |
35 35
|
mulneg1i |
โข ( - i ยท i ) = - ( i ยท i ) |
58 |
|
ixi |
โข ( i ยท i ) = - 1 |
59 |
58
|
negeqi |
โข - ( i ยท i ) = - - 1 |
60 |
|
negneg1e1 |
โข - - 1 = 1 |
61 |
59 60
|
eqtri |
โข - ( i ยท i ) = 1 |
62 |
57 61
|
eqtri |
โข ( - i ยท i ) = 1 |
63 |
62
|
oveq1i |
โข ( ( - i ยท i ) ยท ๐ต ) = ( 1 ยท ๐ต ) |
64 |
1 5 3 6
|
clmvsass |
โข ( ( ๐ โ โMod โง ( - i โ ๐พ โง i โ ๐พ โง ๐ต โ ๐ ) ) โ ( ( - i ยท i ) ยท ๐ต ) = ( - i ยท ( i ยท ๐ต ) ) ) |
65 |
24 52 25 26 64
|
syl13anc |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ( - i ยท i ) ยท ๐ต ) = ( - i ยท ( i ยท ๐ต ) ) ) |
66 |
|
simpr |
โข ( ( ๐ด โ ๐ โง ๐ต โ ๐ ) โ ๐ต โ ๐ ) |
67 |
23 66
|
anim12i |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) ) โ ( ๐ โ โMod โง ๐ต โ ๐ ) ) |
68 |
67
|
3adant3 |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ๐ โ โMod โง ๐ต โ ๐ ) ) |
69 |
1 3
|
clmvs1 |
โข ( ( ๐ โ โMod โง ๐ต โ ๐ ) โ ( 1 ยท ๐ต ) = ๐ต ) |
70 |
68 69
|
syl |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( 1 ยท ๐ต ) = ๐ต ) |
71 |
63 65 70
|
3eqtr3a |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( - i ยท ( i ยท ๐ต ) ) = ๐ต ) |
72 |
71
|
oveq2d |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ( - i ยท ๐ด ) + ( - i ยท ( i ยท ๐ต ) ) ) = ( ( - i ยท ๐ด ) + ๐ต ) ) |
73 |
|
clmabl |
โข ( ๐ โ โMod โ ๐ โ Abel ) |
74 |
22 73
|
syl |
โข ( ๐ โ โVec โ ๐ โ Abel ) |
75 |
7 74
|
simplbiim |
โข ( ๐ โ ( NrmVec โฉ โVec ) โ ๐ โ Abel ) |
76 |
75
|
3ad2ant1 |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ๐ โ Abel ) |
77 |
1 5 3 6
|
clmvscl |
โข ( ( ๐ โ โMod โง - i โ ๐พ โง ๐ด โ ๐ ) โ ( - i ยท ๐ด ) โ ๐ ) |
78 |
24 52 20 77
|
syl3anc |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( - i ยท ๐ด ) โ ๐ ) |
79 |
1 4
|
ablcom |
โข ( ( ๐ โ Abel โง ( - i ยท ๐ด ) โ ๐ โง ๐ต โ ๐ ) โ ( ( - i ยท ๐ด ) + ๐ต ) = ( ๐ต + ( - i ยท ๐ด ) ) ) |
80 |
76 78 26 79
|
syl3anc |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ( - i ยท ๐ด ) + ๐ต ) = ( ๐ต + ( - i ยท ๐ด ) ) ) |
81 |
56 72 80
|
3eqtrd |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( - i ยท ( ๐ด + ( i ยท ๐ต ) ) ) = ( ๐ต + ( - i ยท ๐ด ) ) ) |
82 |
81
|
fveq2d |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ๐ โ ( - i ยท ( ๐ด + ( i ยท ๐ต ) ) ) ) = ( ๐ โ ( ๐ต + ( - i ยท ๐ด ) ) ) ) |
83 |
54 82
|
eqtr3d |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ( abs โ - i ) ยท ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) ) = ( ๐ โ ( ๐ต + ( - i ยท ๐ด ) ) ) ) |
84 |
39 83
|
eqtr3id |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( 1 ยท ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) ) = ( ๐ โ ( ๐ต + ( - i ยท ๐ด ) ) ) ) |
85 |
34 84
|
eqtr3d |
โข ( ( ๐ โ ( NrmVec โฉ โVec ) โง ( ๐ด โ ๐ โง ๐ต โ ๐ ) โง i โ ๐พ ) โ ( ๐ โ ( ๐ด + ( i ยท ๐ต ) ) ) = ( ๐ โ ( ๐ต + ( - i ยท ๐ด ) ) ) ) |