Proof of Theorem ncvspi
| Step | Hyp | Ref
| Expression |
| 1 | | elin 3967 |
. . . . . . 7
⊢ (𝑊 ∈ (NrmVec ∩
ℂVec) ↔ (𝑊
∈ NrmVec ∧ 𝑊
∈ ℂVec)) |
| 2 | | nvcnlm 24717 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod) |
| 3 | | nlmngp 24698 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
| 4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmGrp) |
| 5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec) → 𝑊 ∈ NrmGrp) |
| 6 | 1, 5 | sylbi 217 |
. . . . . 6
⊢ (𝑊 ∈ (NrmVec ∩
ℂVec) → 𝑊 ∈
NrmGrp) |
| 7 | 6 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → 𝑊 ∈ NrmGrp) |
| 8 | | nvclmod 24719 |
. . . . . . . . . 10
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod) |
| 9 | | lmodgrp 20865 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ Grp) |
| 11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec) → 𝑊 ∈ Grp) |
| 12 | 1, 11 | sylbi 217 |
. . . . . . 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 25159 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂVec → 𝑊 ∈
ℂMod) |
| 17 | 1, 16 | simplbiim 504 |
. . . . . . . 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 25121 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂMod ∧ i
∈ 𝐾 ∧ 𝐵 ∈ 𝑉) → (i · 𝐵) ∈ 𝑉) |
| 26 | 18, 19, 20, 25 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (i · 𝐵) ∈ 𝑉) |
| 27 | | ncvsdif.p |
. . . . . . 7
⊢ + =
(+g‘𝑊) |
| 28 | 21, 27 | grpcl 18959 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ (i · 𝐵) ∈ 𝑉) → (𝐴 + (i · 𝐵)) ∈ 𝑉) |
| 29 | 13, 14, 26, 28 | syl3anc 1373 |
. . . . 5
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (𝐴 + (i · 𝐵)) ∈ 𝑉) |
| 30 | | ncvsprp.n |
. . . . . 6
⊢ 𝑁 = (norm‘𝑊) |
| 31 | 21, 30 | nmcl 24629 |
. . . . 5
⊢ ((𝑊 ∈ NrmGrp ∧ (𝐴 + (i · 𝐵)) ∈ 𝑉) → (𝑁‘(𝐴 + (i · 𝐵))) ∈ ℝ) |
| 32 | 7, 29, 31 | syl2anc 584 |
. . . 4
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (𝑁‘(𝐴 + (i · 𝐵))) ∈ ℝ) |
| 33 | 32 | recnd 11289 |
. . 3
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (𝑁‘(𝐴 + (i · 𝐵))) ∈ ℂ) |
| 34 | 33 | mullidd 11279 |
. 2
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (1 · (𝑁‘(𝐴 + (i · 𝐵)))) = (𝑁‘(𝐴 + (i · 𝐵)))) |
| 35 | | ax-icn 11214 |
. . . . . 6
⊢ i ∈
ℂ |
| 36 | 35 | absnegi 15439 |
. . . . 5
⊢
(abs‘-i) = (abs‘i) |
| 37 | | absi 15325 |
. . . . 5
⊢
(abs‘i) = 1 |
| 38 | 36, 37 | eqtri 2765 |
. . . 4
⊢
(abs‘-i) = 1 |
| 39 | 38 | oveq1i 7441 |
. . 3
⊢
((abs‘-i) · (𝑁‘(𝐴 + (i · 𝐵)))) = (1 · (𝑁‘(𝐴 + (i · 𝐵)))) |
| 40 | | simp1 1137 |
. . . . 5
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → 𝑊 ∈ (NrmVec ∩
ℂVec)) |
| 41 | 22, 24 | clmneg 25114 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ ℂMod ∧ i
∈ 𝐾) → -i =
((invg‘𝐹)‘i)) |
| 42 | 16, 41 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ℂVec ∧ i
∈ 𝐾) → -i =
((invg‘𝐹)‘i)) |
| 43 | 22 | clmfgrp 25104 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Grp) |
| 44 | 16, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ ℂVec → 𝐹 ∈ Grp) |
| 45 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(invg‘𝐹) = (invg‘𝐹) |
| 46 | 24, 45 | grpinvcl 19005 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Grp ∧ i ∈ 𝐾) →
((invg‘𝐹)‘i) ∈ 𝐾) |
| 47 | 44, 46 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ℂVec ∧ i
∈ 𝐾) →
((invg‘𝐹)‘i) ∈ 𝐾) |
| 48 | 42, 47 | eqeltrd 2841 |
. . . . . . . . 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 1132 |
. . . . 5
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → -i ∈ 𝐾) |
| 53 | 21, 30, 23, 22, 24 | ncvsprp 25186 |
. . . . 5
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ -i ∈ 𝐾 ∧ (𝐴 + (i · 𝐵)) ∈ 𝑉) → (𝑁‘(-i · (𝐴 + (i · 𝐵)))) = ((abs‘-i) · (𝑁‘(𝐴 + (i · 𝐵))))) |
| 54 | 40, 52, 29, 53 | syl3anc 1373 |
. . . 4
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (𝑁‘(-i · (𝐴 + (i · 𝐵)))) = ((abs‘-i) · (𝑁‘(𝐴 + (i · 𝐵))))) |
| 55 | 21, 22, 23, 24, 27 | clmvsdi 25125 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂMod ∧ (-i
∈ 𝐾 ∧ 𝐴 ∈ 𝑉 ∧ (i · 𝐵) ∈ 𝑉)) → (-i · (𝐴 + (i · 𝐵))) = ((-i · 𝐴) + (-i · (i · 𝐵)))) |
| 56 | 18, 52, 14, 26, 55 | syl13anc 1374 |
. . . . . 6
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (-i · (𝐴 + (i · 𝐵))) = ((-i · 𝐴) + (-i · (i · 𝐵)))) |
| 57 | 35, 35 | mulneg1i 11709 |
. . . . . . . . . 10
⊢ (-i
· i) = -(i · i) |
| 58 | | ixi 11892 |
. . . . . . . . . . . 12
⊢ (i
· i) = -1 |
| 59 | 58 | negeqi 11501 |
. . . . . . . . . . 11
⊢ -(i
· i) = --1 |
| 60 | | negneg1e1 12384 |
. . . . . . . . . . 11
⊢ --1 =
1 |
| 61 | 59, 60 | eqtri 2765 |
. . . . . . . . . 10
⊢ -(i
· i) = 1 |
| 62 | 57, 61 | eqtri 2765 |
. . . . . . . . 9
⊢ (-i
· i) = 1 |
| 63 | 62 | oveq1i 7441 |
. . . . . . . 8
⊢ ((-i
· i) · 𝐵) = (1 · 𝐵) |
| 64 | 21, 22, 23, 24 | clmvsass 25122 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℂMod ∧ (-i
∈ 𝐾 ∧ i ∈
𝐾 ∧ 𝐵 ∈ 𝑉)) → ((-i · i) · 𝐵) = (-i · (i · 𝐵))) |
| 65 | 18, 52, 19, 20, 64 | syl13anc 1374 |
. . . . . . . 8
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → ((-i · i) · 𝐵) = (-i · (i · 𝐵))) |
| 66 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) |
| 67 | 17, 66 | anim12i 613 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉)) |
| 68 | 67 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉)) |
| 69 | 21, 23 | clmvs1 25126 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) → (1 · 𝐵) = 𝐵) |
| 70 | 68, 69 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (1 · 𝐵) = 𝐵) |
| 71 | 63, 65, 70 | 3eqtr3a 2801 |
. . . . . . 7
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (-i · (i · 𝐵)) = 𝐵) |
| 72 | 71 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → ((-i · 𝐴) + (-i · (i · 𝐵))) = ((-i · 𝐴) + 𝐵)) |
| 73 | | clmabl 25102 |
. . . . . . . . . 10
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Abel) |
| 74 | 16, 73 | syl 17 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂVec → 𝑊 ∈ Abel) |
| 75 | 1, 74 | simplbiim 504 |
. . . . . . . 8
⊢ (𝑊 ∈ (NrmVec ∩
ℂVec) → 𝑊 ∈
Abel) |
| 76 | 75 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → 𝑊 ∈ Abel) |
| 77 | 21, 22, 23, 24 | clmvscl 25121 |
. . . . . . . 8
⊢ ((𝑊 ∈ ℂMod ∧ -i
∈ 𝐾 ∧ 𝐴 ∈ 𝑉) → (-i · 𝐴) ∈ 𝑉) |
| 78 | 18, 52, 14, 77 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (-i · 𝐴) ∈ 𝑉) |
| 79 | 21, 27 | ablcom 19817 |
. . . . . . 7
⊢ ((𝑊 ∈ Abel ∧ (-i · 𝐴) ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((-i · 𝐴) + 𝐵) = (𝐵 + (-i · 𝐴))) |
| 80 | 76, 78, 20, 79 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → ((-i · 𝐴) + 𝐵) = (𝐵 + (-i · 𝐴))) |
| 81 | 56, 72, 80 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (-i · (𝐴 + (i · 𝐵))) = (𝐵 + (-i · 𝐴))) |
| 82 | 81 | fveq2d 6910 |
. . . 4
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (𝑁‘(-i · (𝐴 + (i · 𝐵)))) = (𝑁‘(𝐵 + (-i · 𝐴)))) |
| 83 | 54, 82 | eqtr3d 2779 |
. . 3
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → ((abs‘-i) · (𝑁‘(𝐴 + (i · 𝐵)))) = (𝑁‘(𝐵 + (-i · 𝐴)))) |
| 84 | 39, 83 | eqtr3id 2791 |
. 2
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (1 · (𝑁‘(𝐴 + (i · 𝐵)))) = (𝑁‘(𝐵 + (-i · 𝐴)))) |
| 85 | 34, 84 | eqtr3d 2779 |
1
⊢ ((𝑊 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) ∧ i ∈ 𝐾) → (𝑁‘(𝐴 + (i · 𝐵))) = (𝑁‘(𝐵 + (-i · 𝐴)))) |