Step | Hyp | Ref
| Expression |
1 | | isncvsngp.v |
. . 3
β’ π = (Baseβπ) |
2 | | isncvsngp.n |
. . 3
β’ π = (normβπ) |
3 | | isncvsngp.s |
. . 3
β’ Β· = (
Β·π βπ) |
4 | | isncvsngp.f |
. . 3
β’ πΉ = (Scalarβπ) |
5 | | isncvsngp.k |
. . 3
β’ πΎ = (BaseβπΉ) |
6 | 1, 2, 3, 4, 5 | isncvsngp 24358 |
. 2
β’ (π β (NrmVec β©
βVec) β (π
β βVec β§ π
β NrmGrp β§ βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
7 | | simp1 1136 |
. . 3
β’ ((π β βVec β§ π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β π β βVec) |
8 | 1, 2 | nmf 23816 |
. . . 4
β’ (π β NrmGrp β π:πβΆβ) |
9 | 8 | 3ad2ant2 1134 |
. . 3
β’ ((π β βVec β§ π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β π:πβΆβ) |
10 | | ncvsi.m |
. . . . . . 7
β’ β =
(-gβπ) |
11 | | ncvsi.0 |
. . . . . . 7
β’ 0 =
(0gβπ) |
12 | 1, 2, 10, 11 | ngpi 23829 |
. . . . . 6
β’ (π β NrmGrp β (π β Grp β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
13 | | r19.26 3111 |
. . . . . . . . 9
β’
(βπ₯ β
π ((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β (βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β§ βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
14 | | simpll 765 |
. . . . . . . . . . 11
β’
(((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β ((πβπ₯) = 0 β π₯ = 0 )) |
15 | | simplr 767 |
. . . . . . . . . . 11
β’
(((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
16 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) |
17 | 14, 15, 16 | 3jca 1128 |
. . . . . . . . . 10
β’
(((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
18 | 17 | ralimi 3083 |
. . . . . . . . 9
β’
(βπ₯ β
π ((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
19 | 13, 18 | sylbir 234 |
. . . . . . . 8
β’
((βπ₯ β
π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β§ βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
20 | 19 | ex 414 |
. . . . . . 7
β’
(βπ₯ β
π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β (βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)) β βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
21 | 20 | 3ad2ant3 1135 |
. . . . . 6
β’ ((π β Grp β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)))) β (βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)) β βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
22 | 12, 21 | syl 17 |
. . . . 5
β’ (π β NrmGrp β
(βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)) β βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
23 | 22 | imp 408 |
. . . 4
β’ ((π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
24 | 23 | 3adant1 1130 |
. . 3
β’ ((π β βVec β§ π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
25 | 7, 9, 24 | 3jca 1128 |
. 2
β’ ((π β βVec β§ π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β (π β βVec β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
26 | 6, 25 | sylbi 216 |
1
β’ (π β (NrmVec β©
βVec) β (π
β βVec β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |