Step | Hyp | Ref
| Expression |
1 | | elin 3965 |
. . . . . . 7
β’ (π β (NrmVec β©
βVec) β (π
β NrmVec β§ π
β βVec)) |
2 | | nvcnlm 24213 |
. . . . . . . . 9
β’ (π β NrmVec β π β NrmMod) |
3 | | nlmngp 24194 |
. . . . . . . . 9
β’ (π β NrmMod β π β NrmGrp) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
β’ (π β NrmVec β π β NrmGrp) |
5 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β NrmVec β§ π β βVec) β π β NrmGrp) |
6 | 1, 5 | sylbi 216 |
. . . . . 6
β’ (π β (NrmVec β©
βVec) β π β
NrmGrp) |
7 | 6 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β NrmGrp) |
8 | | nvclmod 24215 |
. . . . . . . . . 10
β’ (π β NrmVec β π β LMod) |
9 | | lmodgrp 20478 |
. . . . . . . . . 10
β’ (π β LMod β π β Grp) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (π β NrmVec β π β Grp) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β NrmVec β§ π β βVec) β π β Grp) |
12 | 1, 11 | sylbi 216 |
. . . . . . 7
β’ (π β (NrmVec β©
βVec) β π β
Grp) |
13 | 12 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β Grp) |
14 | | simp2l 1200 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π΄ β π) |
15 | | id 22 |
. . . . . . . . . 10
β’ (π β βVec β π β
βVec) |
16 | 15 | cvsclm 24642 |
. . . . . . . . 9
β’ (π β βVec β π β
βMod) |
17 | 1, 16 | simplbiim 506 |
. . . . . . . 8
β’ (π β (NrmVec β©
βVec) β π β
βMod) |
18 | 17 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β βMod) |
19 | | simp3 1139 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β i β πΎ) |
20 | | simp2r 1201 |
. . . . . . 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 24604 |
. . . . . . 7
β’ ((π β βMod β§ i
β πΎ β§ π΅ β π) β (i Β· π΅) β π) |
26 | 18, 19, 20, 25 | syl3anc 1372 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (i Β· π΅) β π) |
27 | | ncvsdif.p |
. . . . . . 7
β’ + =
(+gβπ) |
28 | 21, 27 | grpcl 18827 |
. . . . . 6
β’ ((π β Grp β§ π΄ β π β§ (i Β· π΅) β π) β (π΄ + (i Β· π΅)) β π) |
29 | 13, 14, 26, 28 | syl3anc 1372 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (π΄ + (i Β· π΅)) β π) |
30 | | ncvsprp.n |
. . . . . 6
β’ π = (normβπ) |
31 | 21, 30 | nmcl 24125 |
. . . . 5
β’ ((π β NrmGrp β§ (π΄ + (i Β· π΅)) β π) β (πβ(π΄ + (i Β· π΅))) β β) |
32 | 7, 29, 31 | syl2anc 585 |
. . . 4
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(π΄ + (i Β· π΅))) β β) |
33 | 32 | recnd 11242 |
. . 3
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(π΄ + (i Β· π΅))) β β) |
34 | 33 | mullidd 11232 |
. 2
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (1 Β· (πβ(π΄ + (i Β· π΅)))) = (πβ(π΄ + (i Β· π΅)))) |
35 | | ax-icn 11169 |
. . . . . 6
β’ i β
β |
36 | 35 | absnegi 15347 |
. . . . 5
β’
(absβ-i) = (absβi) |
37 | | absi 15233 |
. . . . 5
β’
(absβi) = 1 |
38 | 36, 37 | eqtri 2761 |
. . . 4
β’
(absβ-i) = 1 |
39 | 38 | oveq1i 7419 |
. . 3
β’
((absβ-i) Β· (πβ(π΄ + (i Β· π΅)))) = (1 Β· (πβ(π΄ + (i Β· π΅)))) |
40 | | simp1 1137 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β (NrmVec β©
βVec)) |
41 | 22, 24 | clmneg 24597 |
. . . . . . . . . . 11
β’ ((π β βMod β§ i
β πΎ) β -i =
((invgβπΉ)βi)) |
42 | 16, 41 | sylan 581 |
. . . . . . . . . 10
β’ ((π β βVec β§ i
β πΎ) β -i =
((invgβπΉ)βi)) |
43 | 22 | clmfgrp 24587 |
. . . . . . . . . . . 12
β’ (π β βMod β πΉ β Grp) |
44 | 16, 43 | syl 17 |
. . . . . . . . . . 11
β’ (π β βVec β πΉ β Grp) |
45 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(invgβπΉ) = (invgβπΉ) |
46 | 24, 45 | grpinvcl 18872 |
. . . . . . . . . . 11
β’ ((πΉ β Grp β§ i β πΎ) β
((invgβπΉ)βi) β πΎ) |
47 | 44, 46 | sylan 581 |
. . . . . . . . . 10
β’ ((π β βVec β§ i
β πΎ) β
((invgβπΉ)βi) β πΎ) |
48 | 42, 47 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β βVec β§ i
β πΎ) β -i β
πΎ) |
49 | 48 | ex 414 |
. . . . . . . 8
β’ (π β βVec β (i
β πΎ β -i β
πΎ)) |
50 | 1, 49 | simplbiim 506 |
. . . . . . 7
β’ (π β (NrmVec β©
βVec) β (i β πΎ β -i β πΎ)) |
51 | 50 | imp 408 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ i β πΎ) β -i β πΎ) |
52 | 51 | 3adant2 1132 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β -i β πΎ) |
53 | 21, 30, 23, 22, 24 | ncvsprp 24669 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ -i β πΎ β§ (π΄ + (i Β· π΅)) β π) β (πβ(-i Β· (π΄ + (i Β· π΅)))) = ((absβ-i) Β· (πβ(π΄ + (i Β· π΅))))) |
54 | 40, 52, 29, 53 | syl3anc 1372 |
. . . 4
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(-i Β· (π΄ + (i Β· π΅)))) = ((absβ-i) Β· (πβ(π΄ + (i Β· π΅))))) |
55 | 21, 22, 23, 24, 27 | clmvsdi 24608 |
. . . . . . 7
β’ ((π β βMod β§ (-i
β πΎ β§ π΄ β π β§ (i Β· π΅) β π)) β (-i Β· (π΄ + (i Β· π΅))) = ((-i Β· π΄) + (-i Β· (i Β· π΅)))) |
56 | 18, 52, 14, 26, 55 | syl13anc 1373 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (-i Β· (π΄ + (i Β· π΅))) = ((-i Β· π΄) + (-i Β· (i Β· π΅)))) |
57 | 35, 35 | mulneg1i 11660 |
. . . . . . . . . 10
β’ (-i
Β· i) = -(i Β· i) |
58 | | ixi 11843 |
. . . . . . . . . . . 12
β’ (i
Β· i) = -1 |
59 | 58 | negeqi 11453 |
. . . . . . . . . . 11
β’ -(i
Β· i) = --1 |
60 | | negneg1e1 12330 |
. . . . . . . . . . 11
β’ --1 =
1 |
61 | 59, 60 | eqtri 2761 |
. . . . . . . . . 10
β’ -(i
Β· i) = 1 |
62 | 57, 61 | eqtri 2761 |
. . . . . . . . 9
β’ (-i
Β· i) = 1 |
63 | 62 | oveq1i 7419 |
. . . . . . . 8
β’ ((-i
Β· i) Β· π΅) = (1 Β· π΅) |
64 | 21, 22, 23, 24 | clmvsass 24605 |
. . . . . . . . 9
β’ ((π β βMod β§ (-i
β πΎ β§ i β
πΎ β§ π΅ β π)) β ((-i Β· i) Β· π΅) = (-i Β· (i Β· π΅))) |
65 | 18, 52, 19, 20, 64 | syl13anc 1373 |
. . . . . . . 8
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β ((-i Β· i) Β· π΅) = (-i Β· (i Β· π΅))) |
66 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ π΅ β π) β π΅ β π) |
67 | 17, 66 | anim12i 614 |
. . . . . . . . . 10
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π)) β (π β βMod β§ π΅ β π)) |
68 | 67 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (π β βMod β§ π΅ β π)) |
69 | 21, 23 | clmvs1 24609 |
. . . . . . . . 9
β’ ((π β βMod β§ π΅ β π) β (1 Β· π΅) = π΅) |
70 | 68, 69 | syl 17 |
. . . . . . . 8
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (1 Β· π΅) = π΅) |
71 | 63, 65, 70 | 3eqtr3a 2797 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (-i Β· (i Β· π΅)) = π΅) |
72 | 71 | oveq2d 7425 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β ((-i Β· π΄) + (-i Β· (i Β· π΅))) = ((-i Β· π΄) + π΅)) |
73 | | clmabl 24585 |
. . . . . . . . . 10
β’ (π β βMod β π β Abel) |
74 | 16, 73 | syl 17 |
. . . . . . . . 9
β’ (π β βVec β π β Abel) |
75 | 1, 74 | simplbiim 506 |
. . . . . . . 8
β’ (π β (NrmVec β©
βVec) β π β
Abel) |
76 | 75 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β π β Abel) |
77 | 21, 22, 23, 24 | clmvscl 24604 |
. . . . . . . 8
β’ ((π β βMod β§ -i
β πΎ β§ π΄ β π) β (-i Β· π΄) β π) |
78 | 18, 52, 14, 77 | syl3anc 1372 |
. . . . . . 7
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (-i Β· π΄) β π) |
79 | 21, 27 | ablcom 19667 |
. . . . . . 7
β’ ((π β Abel β§ (-i Β· π΄) β π β§ π΅ β π) β ((-i Β· π΄) + π΅) = (π΅ + (-i Β· π΄))) |
80 | 76, 78, 20, 79 | syl3anc 1372 |
. . . . . 6
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β ((-i Β· π΄) + π΅) = (π΅ + (-i Β· π΄))) |
81 | 56, 72, 80 | 3eqtrd 2777 |
. . . . 5
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (-i Β· (π΄ + (i Β· π΅))) = (π΅ + (-i Β· π΄))) |
82 | 81 | fveq2d 6896 |
. . . 4
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(-i Β· (π΄ + (i Β· π΅)))) = (πβ(π΅ + (-i Β· π΄)))) |
83 | 54, 82 | eqtr3d 2775 |
. . 3
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β ((absβ-i) Β· (πβ(π΄ + (i Β· π΅)))) = (πβ(π΅ + (-i Β· π΄)))) |
84 | 39, 83 | eqtr3id 2787 |
. 2
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (1 Β· (πβ(π΄ + (i Β· π΅)))) = (πβ(π΅ + (-i Β· π΄)))) |
85 | 34, 84 | eqtr3d 2775 |
1
β’ ((π β (NrmVec β©
βVec) β§ (π΄ β
π β§ π΅ β π) β§ i β πΎ) β (πβ(π΄ + (i Β· π΅))) = (πβ(π΅ + (-i Β· π΄)))) |