Proof of Theorem nvpi
| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑈 ∈ NrmCVec) |
| 2 | | ax-icn 11214 |
. . . . . . . 8
⊢ i ∈
ℂ |
| 3 | | nvdif.1 |
. . . . . . . . 9
⊢ 𝑋 = (BaseSet‘𝑈) |
| 4 | | nvdif.4 |
. . . . . . . . 9
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
| 5 | 3, 4 | nvscl 30645 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ i ∈
ℂ ∧ 𝐵 ∈
𝑋) → (i𝑆𝐵) ∈ 𝑋) |
| 6 | 2, 5 | mp3an2 1451 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (i𝑆𝐵) ∈ 𝑋) |
| 7 | 6 | 3adant2 1132 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i𝑆𝐵) ∈ 𝑋) |
| 8 | | nvdif.2 |
. . . . . . 7
⊢ 𝐺 = ( +𝑣
‘𝑈) |
| 9 | 3, 8 | nvgcl 30639 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (i𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(i𝑆𝐵)) ∈ 𝑋) |
| 10 | 7, 9 | syld3an3 1411 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺(i𝑆𝐵)) ∈ 𝑋) |
| 11 | | nvdif.6 |
. . . . . 6
⊢ 𝑁 =
(normCV‘𝑈) |
| 12 | 3, 11 | nvcl 30680 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(i𝑆𝐵)) ∈ 𝑋) → (𝑁‘(𝐴𝐺(i𝑆𝐵))) ∈ ℝ) |
| 13 | 1, 10, 12 | syl2anc 584 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺(i𝑆𝐵))) ∈ ℝ) |
| 14 | 13 | recnd 11289 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺(i𝑆𝐵))) ∈ ℂ) |
| 15 | 14 | mullidd 11279 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (1 · (𝑁‘(𝐴𝐺(i𝑆𝐵)))) = (𝑁‘(𝐴𝐺(i𝑆𝐵)))) |
| 16 | 2 | absnegi 15439 |
. . . . 5
⊢
(abs‘-i) = (abs‘i) |
| 17 | | absi 15325 |
. . . . 5
⊢
(abs‘i) = 1 |
| 18 | 16, 17 | eqtri 2765 |
. . . 4
⊢
(abs‘-i) = 1 |
| 19 | 18 | oveq1i 7441 |
. . 3
⊢
((abs‘-i) · (𝑁‘(𝐴𝐺(i𝑆𝐵)))) = (1 · (𝑁‘(𝐴𝐺(i𝑆𝐵)))) |
| 20 | | negicn 11509 |
. . . . . 6
⊢ -i ∈
ℂ |
| 21 | 3, 4, 11 | nvs 30682 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ -i ∈
ℂ ∧ (𝐴𝐺(i𝑆𝐵)) ∈ 𝑋) → (𝑁‘(-i𝑆(𝐴𝐺(i𝑆𝐵)))) = ((abs‘-i) · (𝑁‘(𝐴𝐺(i𝑆𝐵))))) |
| 22 | 20, 21 | mp3an2 1451 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(i𝑆𝐵)) ∈ 𝑋) → (𝑁‘(-i𝑆(𝐴𝐺(i𝑆𝐵)))) = ((abs‘-i) · (𝑁‘(𝐴𝐺(i𝑆𝐵))))) |
| 23 | 1, 10, 22 | syl2anc 584 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(-i𝑆(𝐴𝐺(i𝑆𝐵)))) = ((abs‘-i) · (𝑁‘(𝐴𝐺(i𝑆𝐵))))) |
| 24 | | simp2 1138 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ 𝑋) |
| 25 | 3, 8, 4 | nvdi 30649 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ (-i ∈
ℂ ∧ 𝐴 ∈
𝑋 ∧ (i𝑆𝐵) ∈ 𝑋)) → (-i𝑆(𝐴𝐺(i𝑆𝐵))) = ((-i𝑆𝐴)𝐺(-i𝑆(i𝑆𝐵)))) |
| 26 | 20, 25 | mp3anr1 1460 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ (i𝑆𝐵) ∈ 𝑋)) → (-i𝑆(𝐴𝐺(i𝑆𝐵))) = ((-i𝑆𝐴)𝐺(-i𝑆(i𝑆𝐵)))) |
| 27 | 1, 24, 7, 26 | syl12anc 837 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (-i𝑆(𝐴𝐺(i𝑆𝐵))) = ((-i𝑆𝐴)𝐺(-i𝑆(i𝑆𝐵)))) |
| 28 | 2, 2 | mulneg1i 11709 |
. . . . . . . . . . 11
⊢ (-i
· i) = -(i · i) |
| 29 | | ixi 11892 |
. . . . . . . . . . . . 13
⊢ (i
· i) = -1 |
| 30 | 29 | negeqi 11501 |
. . . . . . . . . . . 12
⊢ -(i
· i) = --1 |
| 31 | | negneg1e1 12384 |
. . . . . . . . . . . 12
⊢ --1 =
1 |
| 32 | 30, 31 | eqtri 2765 |
. . . . . . . . . . 11
⊢ -(i
· i) = 1 |
| 33 | 28, 32 | eqtri 2765 |
. . . . . . . . . 10
⊢ (-i
· i) = 1 |
| 34 | 33 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((-i
· i)𝑆𝐵) = (1𝑆𝐵) |
| 35 | 3, 4 | nvsass 30647 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ (-i ∈
ℂ ∧ i ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → ((-i · i)𝑆𝐵) = (-i𝑆(i𝑆𝐵))) |
| 36 | 20, 35 | mp3anr1 1460 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ (i ∈
ℂ ∧ 𝐵 ∈
𝑋)) → ((-i ·
i)𝑆𝐵) = (-i𝑆(i𝑆𝐵))) |
| 37 | 2, 36 | mpanr1 703 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → ((-i · i)𝑆𝐵) = (-i𝑆(i𝑆𝐵))) |
| 38 | 3, 4 | nvsid 30646 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (1𝑆𝐵) = 𝐵) |
| 39 | 34, 37, 38 | 3eqtr3a 2801 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (-i𝑆(i𝑆𝐵)) = 𝐵) |
| 40 | 39 | 3adant2 1132 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (-i𝑆(i𝑆𝐵)) = 𝐵) |
| 41 | 40 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-i𝑆𝐴)𝐺(-i𝑆(i𝑆𝐵))) = ((-i𝑆𝐴)𝐺𝐵)) |
| 42 | 3, 4 | nvscl 30645 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ -i ∈
ℂ ∧ 𝐴 ∈
𝑋) → (-i𝑆𝐴) ∈ 𝑋) |
| 43 | 20, 42 | mp3an2 1451 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-i𝑆𝐴) ∈ 𝑋) |
| 44 | 43 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (-i𝑆𝐴) ∈ 𝑋) |
| 45 | 3, 8 | nvcom 30640 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ (-i𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-i𝑆𝐴)𝐺𝐵) = (𝐵𝐺(-i𝑆𝐴))) |
| 46 | 44, 45 | syld3an2 1413 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-i𝑆𝐴)𝐺𝐵) = (𝐵𝐺(-i𝑆𝐴))) |
| 47 | 27, 41, 46 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (-i𝑆(𝐴𝐺(i𝑆𝐵))) = (𝐵𝐺(-i𝑆𝐴))) |
| 48 | 47 | fveq2d 6910 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(-i𝑆(𝐴𝐺(i𝑆𝐵)))) = (𝑁‘(𝐵𝐺(-i𝑆𝐴)))) |
| 49 | 23, 48 | eqtr3d 2779 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((abs‘-i) · (𝑁‘(𝐴𝐺(i𝑆𝐵)))) = (𝑁‘(𝐵𝐺(-i𝑆𝐴)))) |
| 50 | 19, 49 | eqtr3id 2791 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (1 · (𝑁‘(𝐴𝐺(i𝑆𝐵)))) = (𝑁‘(𝐵𝐺(-i𝑆𝐴)))) |
| 51 | 15, 50 | eqtr3d 2779 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺(i𝑆𝐵))) = (𝑁‘(𝐵𝐺(-i𝑆𝐴)))) |