Proof of Theorem ipidsq
| Step | Hyp | Ref
| Expression |
| 1 | | ipid.1 |
. . . 4
⊢ 𝑋 = (BaseSet‘𝑈) |
| 2 | | eqid 2737 |
. . . 4
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
| 3 | | eqid 2737 |
. . . 4
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
| 4 | | ipid.6 |
. . . 4
⊢ 𝑁 =
(normCV‘𝑈) |
| 5 | | ipid.7 |
. . . 4
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
| 6 | 1, 2, 3, 4, 5 | ipval2 30726 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝐴) = (((((𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))↑2)) + (i · (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2)))) / 4)) |
| 7 | 6 | 3anidm23 1423 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝐴) = (((((𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))↑2)) + (i · (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2)))) / 4)) |
| 8 | 1, 2, 3 | nv2 30651 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +𝑣 ‘𝑈)𝐴) = (2(
·𝑠OLD ‘𝑈)𝐴)) |
| 9 | 8 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴)) = (𝑁‘(2(
·𝑠OLD ‘𝑈)𝐴))) |
| 10 | | 2re 12340 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
| 11 | | 0le2 12368 |
. . . . . . . . . . . 12
⊢ 0 ≤
2 |
| 12 | 10, 11 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ ∧ 0 ≤ 2) |
| 13 | 1, 3, 4 | nvsge0 30683 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ (2 ∈
ℝ ∧ 0 ≤ 2) ∧ 𝐴 ∈ 𝑋) → (𝑁‘(2(
·𝑠OLD ‘𝑈)𝐴)) = (2 · (𝑁‘𝐴))) |
| 14 | 12, 13 | mp3an2 1451 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(2(
·𝑠OLD ‘𝑈)𝐴)) = (2 · (𝑁‘𝐴))) |
| 15 | 9, 14 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴)) = (2 · (𝑁‘𝐴))) |
| 16 | 15 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴))↑2) = ((2 · (𝑁‘𝐴))↑2)) |
| 17 | 1, 4 | nvcl 30680 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ) |
| 18 | 17 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℂ) |
| 19 | | 2cn 12341 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
| 20 | | 2nn0 12543 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
| 21 | | mulexp 14142 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ (𝑁‘𝐴) ∈ ℂ ∧ 2 ∈
ℕ0) → ((2 · (𝑁‘𝐴))↑2) = ((2↑2) · ((𝑁‘𝐴)↑2))) |
| 22 | 19, 20, 21 | mp3an13 1454 |
. . . . . . . . . 10
⊢ ((𝑁‘𝐴) ∈ ℂ → ((2 · (𝑁‘𝐴))↑2) = ((2↑2) · ((𝑁‘𝐴)↑2))) |
| 23 | 18, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((2 · (𝑁‘𝐴))↑2) = ((2↑2) · ((𝑁‘𝐴)↑2))) |
| 24 | | sq2 14236 |
. . . . . . . . . 10
⊢
(2↑2) = 4 |
| 25 | 24 | oveq1i 7441 |
. . . . . . . . 9
⊢
((2↑2) · ((𝑁‘𝐴)↑2)) = (4 · ((𝑁‘𝐴)↑2)) |
| 26 | 23, 25 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((2 · (𝑁‘𝐴))↑2) = (4 · ((𝑁‘𝐴)↑2))) |
| 27 | 16, 26 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴))↑2) = (4 · ((𝑁‘𝐴)↑2))) |
| 28 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
| 29 | 1, 2, 3, 28 | nvrinv 30670 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)) = (0vec‘𝑈)) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴))) = (𝑁‘(0vec‘𝑈))) |
| 31 | 28, 4 | nvz0 30687 |
. . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec → (𝑁‘(0vec‘𝑈)) = 0) |
| 32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(0vec‘𝑈)) = 0) |
| 33 | 30, 32 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴))) = 0) |
| 34 | 33 | sq0id 14233 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))↑2) = 0) |
| 35 | 27, 34 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))↑2)) = ((4 · ((𝑁‘𝐴)↑2)) − 0)) |
| 36 | | 4cn 12351 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
| 37 | 18 | sqcld 14184 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)↑2) ∈ ℂ) |
| 38 | | mulcl 11239 |
. . . . . . . 8
⊢ ((4
∈ ℂ ∧ ((𝑁‘𝐴)↑2) ∈ ℂ) → (4 ·
((𝑁‘𝐴)↑2)) ∈ ℂ) |
| 39 | 36, 37, 38 | sylancr 587 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (4 · ((𝑁‘𝐴)↑2)) ∈ ℂ) |
| 40 | 39 | subid1d 11609 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((4 · ((𝑁‘𝐴)↑2)) − 0) = (4 · ((𝑁‘𝐴)↑2))) |
| 41 | 35, 40 | eqtrd 2777 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))↑2)) = (4 · ((𝑁‘𝐴)↑2))) |
| 42 | | 1re 11261 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
| 43 | | neg1rr 12381 |
. . . . . . . . . . . . . . . 16
⊢ -1 ∈
ℝ |
| 44 | | absreim 15332 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ -1 ∈ ℝ) → (abs‘(1 + (i ·
-1))) = (√‘((1↑2) + (-1↑2)))) |
| 45 | 42, 43, 44 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢
(abs‘(1 + (i · -1))) = (√‘((1↑2) +
(-1↑2))) |
| 46 | | ax-icn 11214 |
. . . . . . . . . . . . . . . . . . 19
⊢ i ∈
ℂ |
| 47 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
| 48 | 46, 47 | mulneg2i 11710 |
. . . . . . . . . . . . . . . . . 18
⊢ (i
· -1) = -(i · 1) |
| 49 | 46 | mulridi 11265 |
. . . . . . . . . . . . . . . . . . 19
⊢ (i
· 1) = i |
| 50 | 49 | negeqi 11501 |
. . . . . . . . . . . . . . . . . 18
⊢ -(i
· 1) = -i |
| 51 | 48, 50 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ (i
· -1) = -i |
| 52 | 51 | oveq2i 7442 |
. . . . . . . . . . . . . . . 16
⊢ (1 + (i
· -1)) = (1 + -i) |
| 53 | 52 | fveq2i 6909 |
. . . . . . . . . . . . . . 15
⊢
(abs‘(1 + (i · -1))) = (abs‘(1 +
-i)) |
| 54 | | sqneg 14156 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℂ → (-1↑2) = (1↑2)) |
| 55 | 47, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(-1↑2) = (1↑2) |
| 56 | 55 | oveq2i 7442 |
. . . . . . . . . . . . . . . 16
⊢
((1↑2) + (-1↑2)) = ((1↑2) + (1↑2)) |
| 57 | 56 | fveq2i 6909 |
. . . . . . . . . . . . . . 15
⊢
(√‘((1↑2) + (-1↑2))) = (√‘((1↑2)
+ (1↑2))) |
| 58 | 45, 53, 57 | 3eqtr3i 2773 |
. . . . . . . . . . . . . 14
⊢
(abs‘(1 + -i)) = (√‘((1↑2) +
(1↑2))) |
| 59 | | absreim 15332 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ 1 ∈ ℝ) → (abs‘(1 + (i · 1)))
= (√‘((1↑2) + (1↑2)))) |
| 60 | 42, 42, 59 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
(abs‘(1 + (i · 1))) = (√‘((1↑2) +
(1↑2))) |
| 61 | 49 | oveq2i 7442 |
. . . . . . . . . . . . . . 15
⊢ (1 + (i
· 1)) = (1 + i) |
| 62 | 61 | fveq2i 6909 |
. . . . . . . . . . . . . 14
⊢
(abs‘(1 + (i · 1))) = (abs‘(1 + i)) |
| 63 | 58, 60, 62 | 3eqtr2i 2771 |
. . . . . . . . . . . . 13
⊢
(abs‘(1 + -i)) = (abs‘(1 + i)) |
| 64 | 63 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢
((abs‘(1 + -i)) · (𝑁‘𝐴)) = ((abs‘(1 + i)) · (𝑁‘𝐴)) |
| 65 | | negicn 11509 |
. . . . . . . . . . . . . 14
⊢ -i ∈
ℂ |
| 66 | 47, 65 | addcli 11267 |
. . . . . . . . . . . . 13
⊢ (1 + -i)
∈ ℂ |
| 67 | 1, 3, 4 | nvs 30682 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ (1 + -i)
∈ ℂ ∧ 𝐴
∈ 𝑋) → (𝑁‘((1 + -i)(
·𝑠OLD ‘𝑈)𝐴)) = ((abs‘(1 + -i)) · (𝑁‘𝐴))) |
| 68 | 66, 67 | mp3an2 1451 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘((1 + -i)(
·𝑠OLD ‘𝑈)𝐴)) = ((abs‘(1 + -i)) · (𝑁‘𝐴))) |
| 69 | 47, 46 | addcli 11267 |
. . . . . . . . . . . . 13
⊢ (1 + i)
∈ ℂ |
| 70 | 1, 3, 4 | nvs 30682 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ (1 + i)
∈ ℂ ∧ 𝐴
∈ 𝑋) → (𝑁‘((1 + i)(
·𝑠OLD ‘𝑈)𝐴)) = ((abs‘(1 + i)) · (𝑁‘𝐴))) |
| 71 | 69, 70 | mp3an2 1451 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘((1 + i)(
·𝑠OLD ‘𝑈)𝐴)) = ((abs‘(1 + i)) · (𝑁‘𝐴))) |
| 72 | 64, 68, 71 | 3eqtr4a 2803 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘((1 + -i)(
·𝑠OLD ‘𝑈)𝐴)) = (𝑁‘((1 + i)(
·𝑠OLD ‘𝑈)𝐴))) |
| 73 | 1, 2, 3 | nvdir 30650 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ (1 ∈
ℂ ∧ -i ∈ ℂ ∧ 𝐴 ∈ 𝑋)) → ((1 + -i)(
·𝑠OLD ‘𝑈)𝐴) = ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴))) |
| 74 | 47, 73 | mp3anr1 1460 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ (-i ∈
ℂ ∧ 𝐴 ∈
𝑋)) → ((1 + -i)(
·𝑠OLD ‘𝑈)𝐴) = ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴))) |
| 75 | 65, 74 | mpanr1 703 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((1 + -i)(
·𝑠OLD ‘𝑈)𝐴) = ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴))) |
| 76 | 1, 3 | nvsid 30646 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1(
·𝑠OLD ‘𝑈)𝐴) = 𝐴) |
| 77 | 76 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)) = (𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴))) |
| 78 | 75, 77 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((1 + -i)(
·𝑠OLD ‘𝑈)𝐴) = (𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴))) |
| 79 | 78 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘((1 + -i)(
·𝑠OLD ‘𝑈)𝐴)) = (𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))) |
| 80 | 1, 2, 3 | nvdir 30650 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ (1 ∈
ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋)) → ((1 + i)(
·𝑠OLD ‘𝑈)𝐴) = ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴))) |
| 81 | 47, 80 | mp3anr1 1460 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ (i ∈
ℂ ∧ 𝐴 ∈
𝑋)) → ((1 + i)(
·𝑠OLD ‘𝑈)𝐴) = ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴))) |
| 82 | 46, 81 | mpanr1 703 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((1 + i)(
·𝑠OLD ‘𝑈)𝐴) = ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴))) |
| 83 | 76 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)) = (𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴))) |
| 84 | 82, 83 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((1 + i)(
·𝑠OLD ‘𝑈)𝐴) = (𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴))) |
| 85 | 84 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘((1 + i)(
·𝑠OLD ‘𝑈)𝐴)) = (𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))) |
| 86 | 72, 79, 85 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴))) = (𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))) |
| 87 | 86 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2) = ((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2)) |
| 88 | 87 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2)) = (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2))) |
| 89 | 1, 2, 3, 4, 5 | ipval2lem4 30725 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ i ∈ ℂ) → ((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) ∈ ℂ) |
| 90 | 46, 89 | mpan2 691 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) ∈ ℂ) |
| 91 | 90 | 3anidm23 1423 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) ∈ ℂ) |
| 92 | 91 | subidd 11608 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2)) = 0) |
| 93 | 88, 92 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2)) = 0) |
| 94 | 93 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (i · (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2))) = (i ·
0)) |
| 95 | | it0e0 12488 |
. . . . . 6
⊢ (i
· 0) = 0 |
| 96 | 94, 95 | eqtrdi 2793 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (i · (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2))) = 0) |
| 97 | 41, 96 | oveq12d 7449 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))↑2)) + (i · (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2)))) = ((4 · ((𝑁‘𝐴)↑2)) + 0)) |
| 98 | 39 | addridd 11461 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((4 · ((𝑁‘𝐴)↑2)) + 0) = (4 · ((𝑁‘𝐴)↑2))) |
| 99 | 97, 98 | eqtr2d 2778 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (4 · ((𝑁‘𝐴)↑2)) = ((((𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))↑2)) + (i · (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2))))) |
| 100 | 99 | oveq1d 7446 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((4 · ((𝑁‘𝐴)↑2)) / 4) = (((((𝑁‘(𝐴( +𝑣 ‘𝑈)𝐴))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))↑2)) + (i · (((𝑁‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝐴)))↑2) − ((𝑁‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝐴)))↑2)))) / 4)) |
| 101 | | 4ne0 12374 |
. . . 4
⊢ 4 ≠
0 |
| 102 | | divcan3 11948 |
. . . 4
⊢ ((((𝑁‘𝐴)↑2) ∈ ℂ ∧ 4 ∈
ℂ ∧ 4 ≠ 0) → ((4 · ((𝑁‘𝐴)↑2)) / 4) = ((𝑁‘𝐴)↑2)) |
| 103 | 36, 101, 102 | mp3an23 1455 |
. . 3
⊢ (((𝑁‘𝐴)↑2) ∈ ℂ → ((4 ·
((𝑁‘𝐴)↑2)) / 4) = ((𝑁‘𝐴)↑2)) |
| 104 | 37, 103 | syl 17 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((4 · ((𝑁‘𝐴)↑2)) / 4) = ((𝑁‘𝐴)↑2)) |
| 105 | 7, 100, 104 | 3eqtr2d 2783 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝐴) = ((𝑁‘𝐴)↑2)) |