Proof of Theorem dip0r
Step | Hyp | Ref
| Expression |
1 | | dip0r.1 |
. . . . 5
⊢ 𝑋 = (BaseSet‘𝑈) |
2 | | dip0r.5 |
. . . . 5
⊢ 𝑍 = (0vec‘𝑈) |
3 | 1, 2 | nvzcl 27489 |
. . . 4
⊢ (𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋) |
4 | 3 | adantr 481 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → 𝑍 ∈ 𝑋) |
5 | | eqid 2622 |
. . . 4
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
6 | | eqid 2622 |
. . . 4
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
7 | | eqid 2622 |
. . . 4
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
8 | | dip0r.7 |
. . . 4
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
9 | 1, 5, 6, 7, 8 | ipval2 27562 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) → (𝐴𝑃𝑍) = ((((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) / 4)) |
10 | 4, 9 | mpd3an3 1425 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = ((((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) / 4)) |
11 | | neg1cn 11124 |
. . . . . . . . . . . . 13
⊢ -1 ∈
ℂ |
12 | 6, 2 | nvsz 27493 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ) → (-1( ·𝑠OLD ‘𝑈)𝑍) = 𝑍) |
13 | 11, 12 | mpan2 707 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ NrmCVec → (-1(
·𝑠OLD ‘𝑈)𝑍) = 𝑍) |
14 | 13 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-1(
·𝑠OLD ‘𝑈)𝑍) = 𝑍) |
15 | 14 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)) = (𝐴( +𝑣 ‘𝑈)𝑍)) |
16 | 15 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍))) = ((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))) |
17 | 16 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2) =
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2)) |
18 | 17 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) =
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2))) |
19 | 1, 5, 6, 7, 8 | ipval2lem3 27560 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) ∈ ℝ) |
20 | 4, 19 | mpd3an3 1425 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) ∈ ℝ) |
21 | 20 | recnd 10068 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) ∈ ℂ) |
22 | 21 | subidd 10380 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2)) = 0) |
23 | 18, 22 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) = 0) |
24 | | negicn 10282 |
. . . . . . . . . . . . . . 15
⊢ -i ∈
ℂ |
25 | 6, 2 | nvsz 27493 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ -i ∈
ℂ) → (-i( ·𝑠OLD ‘𝑈)𝑍) = 𝑍) |
26 | 24, 25 | mpan2 707 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ NrmCVec → (-i(
·𝑠OLD ‘𝑈)𝑍) = 𝑍) |
27 | | ax-icn 9995 |
. . . . . . . . . . . . . . 15
⊢ i ∈
ℂ |
28 | 6, 2 | nvsz 27493 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ i ∈
ℂ) → (i( ·𝑠OLD ‘𝑈)𝑍) = 𝑍) |
29 | 27, 28 | mpan2 707 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ NrmCVec → (i(
·𝑠OLD ‘𝑈)𝑍) = 𝑍) |
30 | 26, 29 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ NrmCVec → (-i(
·𝑠OLD ‘𝑈)𝑍) = (i(
·𝑠OLD ‘𝑈)𝑍)) |
31 | 30 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-i(
·𝑠OLD ‘𝑈)𝑍) = (i(
·𝑠OLD ‘𝑈)𝑍)) |
32 | 31 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)) = (𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍))) |
33 | 32 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍))) = ((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))) |
34 | 33 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2) =
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2)) |
35 | 34 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)) =
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2))) |
36 | 1, 5, 6, 7, 8 | ipval2lem4 27561 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) ∧ i ∈ ℂ) →
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) ∈ ℂ) |
37 | 27, 36 | mpan2 707 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) ∈ ℂ) |
38 | 4, 37 | mpd3an3 1425 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) ∈ ℂ) |
39 | 38 | subidd 10380 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2)) = 0) |
40 | 35, 39 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)) = 0) |
41 | 40 | oveq2d 6666 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2))) = (i ·
0)) |
42 | 23, 41 | oveq12d 6668 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) = (0 + (i ·
0))) |
43 | | it0e0 11254 |
. . . . . . 7
⊢ (i
· 0) = 0 |
44 | 43 | oveq2i 6661 |
. . . . . 6
⊢ (0 + (i
· 0)) = (0 + 0) |
45 | | 00id 10211 |
. . . . . 6
⊢ (0 + 0) =
0 |
46 | 44, 45 | eqtri 2644 |
. . . . 5
⊢ (0 + (i
· 0)) = 0 |
47 | 42, 46 | syl6eq 2672 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) = 0) |
48 | 47 | oveq1d 6665 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) / 4) = (0 /
4)) |
49 | | 4cn 11098 |
. . . 4
⊢ 4 ∈
ℂ |
50 | | 4ne0 11117 |
. . . 4
⊢ 4 ≠
0 |
51 | 49, 50 | div0i 10759 |
. . 3
⊢ (0 / 4) =
0 |
52 | 48, 51 | syl6eq 2672 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) / 4) = 0) |
53 | 10, 52 | eqtrd 2656 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = 0) |