Proof of Theorem nvge0
Step | Hyp | Ref
| Expression |
1 | | nvge0.1 |
. . . 4
⊢ 𝑋 = (BaseSet‘𝑈) |
2 | | nvge0.6 |
. . . 4
⊢ 𝑁 =
(normCV‘𝑈) |
3 | 1, 2 | nvcl 27516 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ) |
4 | | 2re 11090 |
. . 3
⊢ 2 ∈
ℝ |
5 | 3, 4 | jctil 560 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (2 ∈ ℝ ∧ (𝑁‘𝐴) ∈ ℝ)) |
6 | | eqid 2622 |
. . . . . . . 8
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
7 | 6, 2 | nvz0 27523 |
. . . . . . 7
⊢ (𝑈 ∈ NrmCVec → (𝑁‘(0vec‘𝑈)) = 0) |
8 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(0vec‘𝑈)) = 0) |
9 | | 1pneg1e0 11129 |
. . . . . . . . . 10
⊢ (1 + -1)
= 0 |
10 | 9 | oveq1i 6660 |
. . . . . . . . 9
⊢ ((1 +
-1)( ·𝑠OLD ‘𝑈)𝐴) = (0(
·𝑠OLD ‘𝑈)𝐴) |
11 | | eqid 2622 |
. . . . . . . . . 10
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
12 | 1, 11, 6 | nv0 27492 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (0(
·𝑠OLD ‘𝑈)𝐴) = (0vec‘𝑈)) |
13 | 10, 12 | syl5req 2669 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (0vec‘𝑈) = ((1 + -1)(
·𝑠OLD ‘𝑈)𝐴)) |
14 | | neg1cn 11124 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
15 | | ax-1cn 9994 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
16 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
17 | 1, 16, 11 | nvdir 27486 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ (1 ∈
ℂ ∧ -1 ∈ ℂ ∧ 𝐴 ∈ 𝑋)) → ((1 + -1)(
·𝑠OLD ‘𝑈)𝐴) = ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴))) |
18 | 15, 17 | mp3anr1 1421 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈
ℂ ∧ 𝐴 ∈
𝑋)) → ((1 + -1)(
·𝑠OLD ‘𝑈)𝐴) = ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴))) |
19 | 14, 18 | mpanr1 719 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((1 + -1)(
·𝑠OLD ‘𝑈)𝐴) = ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴))) |
20 | 1, 11 | nvsid 27482 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1(
·𝑠OLD ‘𝑈)𝐴) = 𝐴) |
21 | 20 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((1(
·𝑠OLD ‘𝑈)𝐴)( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)) = (𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴))) |
22 | 13, 19, 21 | 3eqtrd 2660 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (0vec‘𝑈) = (𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴))) |
23 | 22 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(0vec‘𝑈)) = (𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))) |
24 | 8, 23 | eqtr3d 2658 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → 0 = (𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴)))) |
25 | 1, 11 | nvscl 27481 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝐴 ∈
𝑋) → (-1(
·𝑠OLD ‘𝑈)𝐴) ∈ 𝑋) |
26 | 14, 25 | mp3an2 1412 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-1(
·𝑠OLD ‘𝑈)𝐴) ∈ 𝑋) |
27 | 1, 16, 2 | nvtri 27525 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1(
·𝑠OLD ‘𝑈)𝐴) ∈ 𝑋) → (𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴))) ≤ ((𝑁‘𝐴) + (𝑁‘(-1(
·𝑠OLD ‘𝑈)𝐴)))) |
28 | 26, 27 | mpd3an3 1425 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝐴( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝐴))) ≤ ((𝑁‘𝐴) + (𝑁‘(-1(
·𝑠OLD ‘𝑈)𝐴)))) |
29 | 24, 28 | eqbrtrd 4675 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → 0 ≤ ((𝑁‘𝐴) + (𝑁‘(-1(
·𝑠OLD ‘𝑈)𝐴)))) |
30 | 1, 11, 2 | nvm1 27520 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(-1(
·𝑠OLD ‘𝑈)𝐴)) = (𝑁‘𝐴)) |
31 | 30 | oveq2d 6666 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴) + (𝑁‘(-1(
·𝑠OLD ‘𝑈)𝐴))) = ((𝑁‘𝐴) + (𝑁‘𝐴))) |
32 | 3 | recnd 10068 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℂ) |
33 | 32 | 2timesd 11275 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (2 · (𝑁‘𝐴)) = ((𝑁‘𝐴) + (𝑁‘𝐴))) |
34 | 31, 33 | eqtr4d 2659 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴) + (𝑁‘(-1(
·𝑠OLD ‘𝑈)𝐴))) = (2 · (𝑁‘𝐴))) |
35 | 29, 34 | breqtrd 4679 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → 0 ≤ (2 · (𝑁‘𝐴))) |
36 | | 2pos 11112 |
. . 3
⊢ 0 <
2 |
37 | 35, 36 | jctil 560 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (0 < 2 ∧ 0 ≤ (2 ·
(𝑁‘𝐴)))) |
38 | | prodge0 10870 |
. 2
⊢ (((2
∈ ℝ ∧ (𝑁‘𝐴) ∈ ℝ) ∧ (0 < 2 ∧ 0
≤ (2 · (𝑁‘𝐴)))) → 0 ≤ (𝑁‘𝐴)) |
39 | 5, 37, 38 | syl2anc 693 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → 0 ≤ (𝑁‘𝐴)) |