Step | Hyp | Ref
| Expression |
1 | | elin 3960 |
. . . . . . 7
β’ (π β (NrmVec β©
βVec) β (π
β NrmVec β§ π
β βVec)) |
2 | | nvcnlm 24600 |
. . . . . . . . 9
β’ (π β NrmVec β π β NrmMod) |
3 | | nlmngp 24581 |
. . . . . . . . 9
β’ (π β NrmMod β π β NrmGrp) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
β’ (π β NrmVec β π β NrmGrp) |
5 | 4 | adantr 480 |
. . . . . . 7
β’ ((π β NrmVec β§ π β βVec) β π β NrmGrp) |
6 | 1, 5 | sylbi 216 |
. . . . . 6
β’ (π β (NrmVec β©
βVec) β π β
NrmGrp) |
7 | 6 | 3ad2ant1 1131 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β NrmGrp) |
8 | | nvclmod 24602 |
. . . . . . . . . 10
β’ (π β NrmVec β π β LMod) |
9 | | lmodgrp 20739 |
. . . . . . . . . 10
β’ (π β LMod β π β Grp) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (π β NrmVec β π β Grp) |
11 | 10 | adantr 480 |
. . . . . . . 8
β’ ((π β NrmVec β§ π β βVec) β π β Grp) |
12 | 1, 11 | sylbi 216 |
. . . . . . 7
β’ (π β (NrmVec β©
βVec) β π β
Grp) |
13 | 12 | 3ad2ant1 1131 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β Grp) |
14 | | simp2l 1197 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π΄ β π) |
15 | | id 22 |
. . . . . . . . . 10
β’ (π β βVec β π β
βVec) |
16 | 15 | cvsclm 25040 |
. . . . . . . . 9
β’ (π β βVec β π β
βMod) |
17 | 1, 16 | simplbiim 504 |
. . . . . . . 8
β’ (π β (NrmVec β©
βVec) β π β
βMod) |
18 | 17 | 3ad2ant1 1131 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β βMod) |
19 | | simp3 1136 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β i β πΎ) |
20 | | simp2r 1198 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π΅ β π) |
21 | | ncvsprp.v |
. . . . . . . 8
β’ π = (Baseβπ) |
22 | | ncvspi.f |
. . . . . . . 8
β’ πΉ = (Scalarβπ) |
23 | | ncvsprp.s |
. . . . . . . 8
β’ Β· = (
Β·π βπ) |
24 | | ncvspi.k |
. . . . . . . 8
β’ πΎ = (BaseβπΉ) |
25 | 21, 22, 23, 24 | clmvscl 25002 |
. . . . . . 7
β’ ((π β βMod β§ i
β πΎ β§ π΅ β π) β (i Β· π΅) β π) |
26 | 18, 19, 20, 25 | syl3anc 1369 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (i Β· π΅) β π) |
27 | | ncvsdif.p |
. . . . . . 7
β’ + =
(+gβπ) |
28 | 21, 27 | grpcl 18889 |
. . . . . 6
β’ ((π β Grp β§ π΄ β π β§ (i Β· π΅) β π) β (π΄ + (i Β· π΅)) β π) |
29 | 13, 14, 26, 28 | syl3anc 1369 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (π΄ + (i Β· π΅)) β π) |
30 | | ncvsprp.n |
. . . . . 6
β’ π = (normβπ) |
31 | 21, 30 | nmcl 24512 |
. . . . 5
β’ ((π β NrmGrp β§ (π΄ + (i Β· π΅)) β π) β (πβ(π΄ + (i Β· π΅))) β β) |
32 | 7, 29, 31 | syl2anc 583 |
. . . 4
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(π΄ + (i Β· π΅))) β β) |
33 | 32 | recnd 11264 |
. . 3
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(π΄ + (i Β· π΅))) β β) |
34 | 33 | mullidd 11254 |
. 2
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (1 Β· (πβ(π΄ + (i Β· π΅)))) = (πβ(π΄ + (i Β· π΅)))) |
35 | | ax-icn 11189 |
. . . . . 6
β’ i β
β |
36 | 35 | absnegi 15371 |
. . . . 5
β’
(absβ-i) = (absβi) |
37 | | absi 15257 |
. . . . 5
β’
(absβi) = 1 |
38 | 36, 37 | eqtri 2755 |
. . . 4
β’
(absβ-i) = 1 |
39 | 38 | oveq1i 7424 |
. . 3
β’
((absβ-i) Β· (πβ(π΄ + (i Β· π΅)))) = (1 Β· (πβ(π΄ + (i Β· π΅)))) |
40 | | simp1 1134 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β (NrmVec β©
βVec)) |
41 | 22, 24 | clmneg 24995 |
. . . . . . . . . . 11
β’ ((π β βMod β§ i
β πΎ) β -i =
((invgβπΉ)βi)) |
42 | 16, 41 | sylan 579 |
. . . . . . . . . 10
β’ ((π β βVec β§ i
β πΎ) β -i =
((invgβπΉ)βi)) |
43 | 22 | clmfgrp 24985 |
. . . . . . . . . . . 12
β’ (π β βMod β πΉ β Grp) |
44 | 16, 43 | syl 17 |
. . . . . . . . . . 11
β’ (π β βVec β πΉ β Grp) |
45 | | eqid 2727 |
. . . . . . . . . . . 12
β’
(invgβπΉ) = (invgβπΉ) |
46 | 24, 45 | grpinvcl 18935 |
. . . . . . . . . . 11
β’ ((πΉ β Grp β§ i β πΎ) β
((invgβπΉ)βi) β πΎ) |
47 | 44, 46 | sylan 579 |
. . . . . . . . . 10
β’ ((π β βVec β§ i
β πΎ) β
((invgβπΉ)βi) β πΎ) |
48 | 42, 47 | eqeltrd 2828 |
. . . . . . . . 9
β’ ((π β βVec β§ i
β πΎ) β -i β
πΎ) |
49 | 48 | ex 412 |
. . . . . . . 8
β’ (π β βVec β (i
β πΎ β -i β
πΎ)) |
50 | 1, 49 | simplbiim 504 |
. . . . . . 7
β’ (π β (NrmVec β©
βVec) β (i β πΎ β -i β πΎ)) |
51 | 50 | imp 406 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ i β πΎ) β -i β πΎ) |
52 | 51 | 3adant2 1129 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β -i β πΎ) |
53 | 21, 30, 23, 22, 24 | ncvsprp 25067 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ -i β πΎ β§ (π΄ + (i Β· π΅)) β π) β (πβ(-i Β· (π΄ + (i Β· π΅)))) = ((absβ-i) Β· (πβ(π΄ + (i Β· π΅))))) |
54 | 40, 52, 29, 53 | syl3anc 1369 |
. . . 4
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(-i Β· (π΄ + (i Β· π΅)))) = ((absβ-i) Β· (πβ(π΄ + (i Β· π΅))))) |
55 | 21, 22, 23, 24, 27 | clmvsdi 25006 |
. . . . . . 7
β’ ((π β βMod β§ (-i
β πΎ β§ π΄ β π β§ (i Β· π΅) β π)) β (-i Β· (π΄ + (i Β· π΅))) = ((-i Β· π΄) + (-i Β· (i Β· π΅)))) |
56 | 18, 52, 14, 26, 55 | syl13anc 1370 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (-i Β· (π΄ + (i Β· π΅))) = ((-i Β· π΄) + (-i Β· (i Β· π΅)))) |
57 | 35, 35 | mulneg1i 11682 |
. . . . . . . . . 10
β’ (-i
Β· i) = -(i Β· i) |
58 | | ixi 11865 |
. . . . . . . . . . . 12
β’ (i
Β· i) = -1 |
59 | 58 | negeqi 11475 |
. . . . . . . . . . 11
β’ -(i
Β· i) = --1 |
60 | | negneg1e1 12352 |
. . . . . . . . . . 11
β’ --1 =
1 |
61 | 59, 60 | eqtri 2755 |
. . . . . . . . . 10
β’ -(i
Β· i) = 1 |
62 | 57, 61 | eqtri 2755 |
. . . . . . . . 9
β’ (-i
Β· i) = 1 |
63 | 62 | oveq1i 7424 |
. . . . . . . 8
β’ ((-i
Β· i) Β· π΅) = (1 Β· π΅) |
64 | 21, 22, 23, 24 | clmvsass 25003 |
. . . . . . . . 9
β’ ((π β βMod β§ (-i
β πΎ β§ i β
πΎ β§ π΅ β π)) β ((-i Β· i) Β· π΅) = (-i Β· (i Β· π΅))) |
65 | 18, 52, 19, 20, 64 | syl13anc 1370 |
. . . . . . . 8
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β ((-i Β· i) Β· π΅) = (-i Β· (i Β· π΅))) |
66 | | simpr 484 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ π΅ β π) β π΅ β π) |
67 | 17, 66 | anim12i 612 |
. . . . . . . . . 10
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π)) β (π β βMod β§ π΅ β π)) |
68 | 67 | 3adant3 1130 |
. . . . . . . . 9
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (π β βMod β§ π΅ β π)) |
69 | 21, 23 | clmvs1 25007 |
. . . . . . . . 9
β’ ((π β βMod β§ π΅ β π) β (1 Β· π΅) = π΅) |
70 | 68, 69 | syl 17 |
. . . . . . . 8
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (1 Β· π΅) = π΅) |
71 | 63, 65, 70 | 3eqtr3a 2791 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (-i Β· (i Β· π΅)) = π΅) |
72 | 71 | oveq2d 7430 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β ((-i Β· π΄) + (-i Β· (i Β· π΅))) = ((-i Β· π΄) + π΅)) |
73 | | clmabl 24983 |
. . . . . . . . . 10
β’ (π β βMod β π β Abel) |
74 | 16, 73 | syl 17 |
. . . . . . . . 9
β’ (π β βVec β π β Abel) |
75 | 1, 74 | simplbiim 504 |
. . . . . . . 8
β’ (π β (NrmVec β©
βVec) β π β
Abel) |
76 | 75 | 3ad2ant1 1131 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β Abel) |
77 | 21, 22, 23, 24 | clmvscl 25002 |
. . . . . . . 8
β’ ((π β βMod β§ -i
β πΎ β§ π΄ β π) β (-i Β· π΄) β π) |
78 | 18, 52, 14, 77 | syl3anc 1369 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (-i Β· π΄) β π) |
79 | 21, 27 | ablcom 19745 |
. . . . . . 7
β’ ((π β Abel β§ (-i Β· π΄) β π β§ π΅ β π) β ((-i Β· π΄) + π΅) = (π΅ + (-i Β· π΄))) |
80 | 76, 78, 20, 79 | syl3anc 1369 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β ((-i Β· π΄) + π΅) = (π΅ + (-i Β· π΄))) |
81 | 56, 72, 80 | 3eqtrd 2771 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (-i Β· (π΄ + (i Β· π΅))) = (π΅ + (-i Β· π΄))) |
82 | 81 | fveq2d 6895 |
. . . 4
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(-i Β· (π΄ + (i Β· π΅)))) = (πβ(π΅ + (-i Β· π΄)))) |
83 | 54, 82 | eqtr3d 2769 |
. . 3
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β ((absβ-i) Β· (πβ(π΄ + (i Β· π΅)))) = (πβ(π΅ + (-i Β· π΄)))) |
84 | 39, 83 | eqtr3id 2781 |
. 2
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (1 Β· (πβ(π΄ + (i Β· π΅)))) = (πβ(π΅ + (-i Β· π΄)))) |
85 | 34, 84 | eqtr3d 2769 |
1
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(π΄ + (i Β· π΅))) = (πβ(π΅ + (-i Β· π΄)))) |