Step | Hyp | Ref
| Expression |
1 | | df-nv 29845 |
. . 3
β’ NrmCVec =
{β¨β¨π, π β©, πβ© β£ (β¨π, π β© β CVecOLD β§ π:ran πβΆβ β§ βπ₯ β ran π(((πβπ₯) = 0 β π₯ = (GIdβπ)) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β ran π(πβ(π₯ππ¦)) β€ ((πβπ₯) + (πβπ¦))))} |
2 | 1 | eleq2i 2826 |
. 2
β’
(β¨β¨πΊ,
πβ©, πβ© β NrmCVec β
β¨β¨πΊ, πβ©, πβ© β {β¨β¨π, π β©, πβ© β£ (β¨π, π β© β CVecOLD β§ π:ran πβΆβ β§ βπ₯ β ran π(((πβπ₯) = 0 β π₯ = (GIdβπ)) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β ran π(πβ(π₯ππ¦)) β€ ((πβπ₯) + (πβπ¦))))}) |
3 | | opeq1 4874 |
. . . . 5
β’ (π = πΊ β β¨π, π β© = β¨πΊ, π β©) |
4 | 3 | eleq1d 2819 |
. . . 4
β’ (π = πΊ β (β¨π, π β© β CVecOLD β
β¨πΊ, π β© β
CVecOLD)) |
5 | | rneq 5936 |
. . . . . 6
β’ (π = πΊ β ran π = ran πΊ) |
6 | | isnvlem.1 |
. . . . . 6
β’ π = ran πΊ |
7 | 5, 6 | eqtr4di 2791 |
. . . . 5
β’ (π = πΊ β ran π = π) |
8 | 7 | feq2d 6704 |
. . . 4
β’ (π = πΊ β (π:ran πβΆβ β π:πβΆβ)) |
9 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = πΊ β (GIdβπ) = (GIdβπΊ)) |
10 | | isnvlem.2 |
. . . . . . . . 9
β’ π = (GIdβπΊ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = πΊ β (GIdβπ) = π) |
12 | 11 | eqeq2d 2744 |
. . . . . . 7
β’ (π = πΊ β (π₯ = (GIdβπ) β π₯ = π)) |
13 | 12 | imbi2d 341 |
. . . . . 6
β’ (π = πΊ β (((πβπ₯) = 0 β π₯ = (GIdβπ)) β ((πβπ₯) = 0 β π₯ = π))) |
14 | | oveq 7415 |
. . . . . . . . 9
β’ (π = πΊ β (π₯ππ¦) = (π₯πΊπ¦)) |
15 | 14 | fveq2d 6896 |
. . . . . . . 8
β’ (π = πΊ β (πβ(π₯ππ¦)) = (πβ(π₯πΊπ¦))) |
16 | 15 | breq1d 5159 |
. . . . . . 7
β’ (π = πΊ β ((πβ(π₯ππ¦)) β€ ((πβπ₯) + (πβπ¦)) β (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))) |
17 | 7, 16 | raleqbidv 3343 |
. . . . . 6
β’ (π = πΊ β (βπ¦ β ran π(πβ(π₯ππ¦)) β€ ((πβπ₯) + (πβπ¦)) β βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))) |
18 | 13, 17 | 3anbi13d 1439 |
. . . . 5
β’ (π = πΊ β ((((πβπ₯) = 0 β π₯ = (GIdβπ)) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β ran π(πβ(π₯ππ¦)) β€ ((πβπ₯) + (πβπ¦))) β (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
19 | 7, 18 | raleqbidv 3343 |
. . . 4
β’ (π = πΊ β (βπ₯ β ran π(((πβπ₯) = 0 β π₯ = (GIdβπ)) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β ran π(πβ(π₯ππ¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
20 | 4, 8, 19 | 3anbi123d 1437 |
. . 3
β’ (π = πΊ β ((β¨π, π β© β CVecOLD β§ π:ran πβΆβ β§ βπ₯ β ran π(((πβπ₯) = 0 β π₯ = (GIdβπ)) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β ran π(πβ(π₯ππ¦)) β€ ((πβπ₯) + (πβπ¦)))) β (β¨πΊ, π β© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
21 | | opeq2 4875 |
. . . . 5
β’ (π = π β β¨πΊ, π β© = β¨πΊ, πβ©) |
22 | 21 | eleq1d 2819 |
. . . 4
β’ (π = π β (β¨πΊ, π β© β CVecOLD β
β¨πΊ, πβ© β
CVecOLD)) |
23 | | oveq 7415 |
. . . . . . . 8
β’ (π = π β (π¦π π₯) = (π¦ππ₯)) |
24 | 23 | fveqeq2d 6900 |
. . . . . . 7
β’ (π = π β ((πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)))) |
25 | 24 | ralbidv 3178 |
. . . . . 6
β’ (π = π β (βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)))) |
26 | 25 | 3anbi2d 1442 |
. . . . 5
β’ (π = π β ((((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) β (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
27 | 26 | ralbidv 3178 |
. . . 4
β’ (π = π β (βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
28 | 22, 27 | 3anbi13d 1439 |
. . 3
β’ (π = π β ((β¨πΊ, π β© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))) β (β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
29 | | feq1 6699 |
. . . 4
β’ (π = π β (π:πβΆβ β π:πβΆβ)) |
30 | | fveq1 6891 |
. . . . . . . 8
β’ (π = π β (πβπ₯) = (πβπ₯)) |
31 | 30 | eqeq1d 2735 |
. . . . . . 7
β’ (π = π β ((πβπ₯) = 0 β (πβπ₯) = 0)) |
32 | 31 | imbi1d 342 |
. . . . . 6
β’ (π = π β (((πβπ₯) = 0 β π₯ = π) β ((πβπ₯) = 0 β π₯ = π))) |
33 | | fveq1 6891 |
. . . . . . . 8
β’ (π = π β (πβ(π¦ππ₯)) = (πβ(π¦ππ₯))) |
34 | 30 | oveq2d 7425 |
. . . . . . . 8
β’ (π = π β ((absβπ¦) Β· (πβπ₯)) = ((absβπ¦) Β· (πβπ₯))) |
35 | 33, 34 | eqeq12d 2749 |
. . . . . . 7
β’ (π = π β ((πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)))) |
36 | 35 | ralbidv 3178 |
. . . . . 6
β’ (π = π β (βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)))) |
37 | | fveq1 6891 |
. . . . . . . 8
β’ (π = π β (πβ(π₯πΊπ¦)) = (πβ(π₯πΊπ¦))) |
38 | | fveq1 6891 |
. . . . . . . . 9
β’ (π = π β (πβπ¦) = (πβπ¦)) |
39 | 30, 38 | oveq12d 7427 |
. . . . . . . 8
β’ (π = π β ((πβπ₯) + (πβπ¦)) = ((πβπ₯) + (πβπ¦))) |
40 | 37, 39 | breq12d 5162 |
. . . . . . 7
β’ (π = π β ((πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)) β (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))) |
41 | 40 | ralbidv 3178 |
. . . . . 6
β’ (π = π β (βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)) β βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))) |
42 | 32, 36, 41 | 3anbi123d 1437 |
. . . . 5
β’ (π = π β ((((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) β (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
43 | 42 | ralbidv 3178 |
. . . 4
β’ (π = π β (βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
44 | 29, 43 | 3anbi23d 1440 |
. . 3
β’ (π = π β ((β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))) β (β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
45 | 20, 28, 44 | eloprabg 7518 |
. 2
β’ ((πΊ β V β§ π β V β§ π β V) β
(β¨β¨πΊ, πβ©, πβ© β {β¨β¨π, π β©, πβ© β£ (β¨π, π β© β CVecOLD β§ π:ran πβΆβ β§ βπ₯ β ran π(((πβπ₯) = 0 β π₯ = (GIdβπ)) β§ βπ¦ β β (πβ(π¦π π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β ran π(πβ(π₯ππ¦)) β€ ((πβπ₯) + (πβπ¦))))} β (β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
46 | 2, 45 | bitrid 283 |
1
β’ ((πΊ β V β§ π β V β§ π β V) β
(β¨β¨πΊ, πβ©, πβ© β NrmCVec β (β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))))) |