Proof of Theorem dip0r
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dip0r.1 | . . . . 5
⊢ 𝑋 = (BaseSet‘𝑈) | 
| 2 |  | dip0r.5 | . . . . 5
⊢ 𝑍 = (0vec‘𝑈) | 
| 3 | 1, 2 | nvzcl 30654 | . . . 4
⊢ (𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋) | 
| 4 | 3 | adantr 480 | . . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → 𝑍 ∈ 𝑋) | 
| 5 |  | eqid 2736 | . . . 4
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) | 
| 6 |  | eqid 2736 | . . . 4
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) | 
| 7 |  | eqid 2736 | . . . 4
⊢
(normCV‘𝑈) = (normCV‘𝑈) | 
| 8 |  | dip0r.7 | . . . 4
⊢ 𝑃 =
(·𝑖OLD‘𝑈) | 
| 9 | 1, 5, 6, 7, 8 | ipval2 30727 | . . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) → (𝐴𝑃𝑍) = ((((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) / 4)) | 
| 10 | 4, 9 | mpd3an3 1463 | . 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = ((((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) / 4)) | 
| 11 |  | neg1cn 12381 | . . . . . . . . . . . . 13
⊢ -1 ∈
ℂ | 
| 12 | 6, 2 | nvsz 30658 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ) → (-1( ·𝑠OLD ‘𝑈)𝑍) = 𝑍) | 
| 13 | 11, 12 | mpan2 691 | . . . . . . . . . . . 12
⊢ (𝑈 ∈ NrmCVec → (-1(
·𝑠OLD ‘𝑈)𝑍) = 𝑍) | 
| 14 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-1(
·𝑠OLD ‘𝑈)𝑍) = 𝑍) | 
| 15 | 14 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)) = (𝐴( +𝑣 ‘𝑈)𝑍)) | 
| 16 | 15 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍))) = ((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))) | 
| 17 | 16 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2) =
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2)) | 
| 18 | 17 | oveq2d 7448 | . . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) =
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2))) | 
| 19 | 1, 5, 6, 7, 8 | ipval2lem3 30725 | . . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) ∈ ℝ) | 
| 20 | 4, 19 | mpd3an3 1463 | . . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) ∈ ℝ) | 
| 21 | 20 | recnd 11290 | . . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) ∈ ℂ) | 
| 22 | 21 | subidd 11609 | . . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2)) = 0) | 
| 23 | 18, 22 | eqtrd 2776 | . . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) = 0) | 
| 24 |  | negicn 11510 | . . . . . . . . . . . . . . 15
⊢ -i ∈
ℂ | 
| 25 | 6, 2 | nvsz 30658 | . . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ -i ∈
ℂ) → (-i( ·𝑠OLD ‘𝑈)𝑍) = 𝑍) | 
| 26 | 24, 25 | mpan2 691 | . . . . . . . . . . . . . 14
⊢ (𝑈 ∈ NrmCVec → (-i(
·𝑠OLD ‘𝑈)𝑍) = 𝑍) | 
| 27 |  | ax-icn 11215 | . . . . . . . . . . . . . . 15
⊢ i ∈
ℂ | 
| 28 | 6, 2 | nvsz 30658 | . . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ i ∈
ℂ) → (i( ·𝑠OLD ‘𝑈)𝑍) = 𝑍) | 
| 29 | 27, 28 | mpan2 691 | . . . . . . . . . . . . . 14
⊢ (𝑈 ∈ NrmCVec → (i(
·𝑠OLD ‘𝑈)𝑍) = 𝑍) | 
| 30 | 26, 29 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (𝑈 ∈ NrmCVec → (-i(
·𝑠OLD ‘𝑈)𝑍) = (i(
·𝑠OLD ‘𝑈)𝑍)) | 
| 31 | 30 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-i(
·𝑠OLD ‘𝑈)𝑍) = (i(
·𝑠OLD ‘𝑈)𝑍)) | 
| 32 | 31 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)) = (𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍))) | 
| 33 | 32 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍))) = ((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))) | 
| 34 | 33 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2) =
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2)) | 
| 35 | 34 | oveq2d 7448 | . . . . . . . 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 30726 | . . . . . . . . . . 11
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) ∧ i ∈ ℂ) →
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) ∈ ℂ) | 
| 37 | 27, 36 | mpan2 691 | . . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) ∈ ℂ) | 
| 38 | 4, 37 | mpd3an3 1463 | . . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) ∈ ℂ) | 
| 39 | 38 | subidd 11609 | . . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2)) = 0) | 
| 40 | 35, 39 | eqtrd 2776 | . . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)) = 0) | 
| 41 | 40 | oveq2d 7448 | . . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2))) = (i ·
0)) | 
| 42 | 23, 41 | oveq12d 7450 | . . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) = (0 + (i ·
0))) | 
| 43 |  | it0e0 12491 | . . . . . . 7
⊢ (i
· 0) = 0 | 
| 44 | 43 | oveq2i 7443 | . . . . . 6
⊢ (0 + (i
· 0)) = (0 + 0) | 
| 45 |  | 00id 11437 | . . . . . 6
⊢ (0 + 0) =
0 | 
| 46 | 44, 45 | eqtri 2764 | . . . . 5
⊢ (0 + (i
· 0)) = 0 | 
| 47 | 42, 46 | eqtrdi 2792 | . . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) = 0) | 
| 48 | 47 | oveq1d 7447 | . . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) / 4) = (0 /
4)) | 
| 49 |  | 4cn 12352 | . . . 4
⊢ 4 ∈
ℂ | 
| 50 |  | 4ne0 12375 | . . . 4
⊢ 4 ≠
0 | 
| 51 | 49, 50 | div0i 12002 | . . 3
⊢ (0 / 4) =
0 | 
| 52 | 48, 51 | eqtrdi 2792 | . 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)𝑍))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑍)))↑2)) + (i ·
((((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(i(
·𝑠OLD ‘𝑈)𝑍)))↑2) −
(((normCV‘𝑈)‘(𝐴( +𝑣 ‘𝑈)(-i(
·𝑠OLD ‘𝑈)𝑍)))↑2)))) / 4) = 0) | 
| 53 | 10, 52 | eqtrd 2776 | 1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = 0) |