Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . . . 6
β’
(1st βπ) = (1st βπ) |
2 | | nvi.6 |
. . . . . 6
β’ π =
(normCVβπ) |
3 | 1, 2 | nvop2 29856 |
. . . . 5
β’ (π β NrmCVec β π = β¨(1st
βπ), πβ©) |
4 | | nvi.2 |
. . . . . . 7
β’ πΊ = ( +π£
βπ) |
5 | | nvi.4 |
. . . . . . 7
β’ π = (
Β·π OLD βπ) |
6 | 1, 4, 5 | nvvop 29857 |
. . . . . 6
β’ (π β NrmCVec β
(1st βπ) =
β¨πΊ, πβ©) |
7 | 6 | opeq1d 4879 |
. . . . 5
β’ (π β NrmCVec β
β¨(1st βπ), πβ© = β¨β¨πΊ, πβ©, πβ©) |
8 | 3, 7 | eqtrd 2772 |
. . . 4
β’ (π β NrmCVec β π = β¨β¨πΊ, πβ©, πβ©) |
9 | | id 22 |
. . . 4
β’ (π β NrmCVec β π β
NrmCVec) |
10 | 8, 9 | eqeltrrd 2834 |
. . 3
β’ (π β NrmCVec β
β¨β¨πΊ, πβ©, πβ© β NrmCVec) |
11 | | nvi.1 |
. . . . 5
β’ π = (BaseSetβπ) |
12 | 11, 4 | bafval 29852 |
. . . 4
β’ π = ran πΊ |
13 | | eqid 2732 |
. . . 4
β’
(GIdβπΊ) =
(GIdβπΊ) |
14 | 12, 13 | isnv 29860 |
. . 3
β’
(β¨β¨πΊ,
πβ©, πβ© β NrmCVec β (β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = (GIdβπΊ)) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
15 | 10, 14 | sylib 217 |
. 2
β’ (π β NrmCVec β
(β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = (GIdβπΊ)) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
16 | | nvi.5 |
. . . . . . . 8
β’ π = (0vecβπ) |
17 | 4, 16 | 0vfval 29854 |
. . . . . . 7
β’ (π β NrmCVec β π = (GIdβπΊ)) |
18 | 17 | eqeq2d 2743 |
. . . . . 6
β’ (π β NrmCVec β (π₯ = π β π₯ = (GIdβπΊ))) |
19 | 18 | imbi2d 340 |
. . . . 5
β’ (π β NrmCVec β (((πβπ₯) = 0 β π₯ = π) β ((πβπ₯) = 0 β π₯ = (GIdβπΊ)))) |
20 | 19 | 3anbi1d 1440 |
. . . 4
β’ (π β NrmCVec β ((((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) β (((πβπ₯) = 0 β π₯ = (GIdβπΊ)) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
21 | 20 | ralbidv 3177 |
. . 3
β’ (π β NrmCVec β
(βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ₯ β π (((πβπ₯) = 0 β π₯ = (GIdβπΊ)) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
22 | 21 | 3anbi3d 1442 |
. 2
β’ (π β NrmCVec β
((β¨πΊ, πβ© β CVecOLD
β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))) β (β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = (GIdβπΊ)) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
23 | 15, 22 | mpbird 256 |
1
β’ (π β NrmCVec β
(β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |