Step | Hyp | Ref
| Expression |
1 | | nvtri.1 |
. . . . . . 7
β’ π = (BaseSetβπ) |
2 | | nvtri.2 |
. . . . . . 7
β’ πΊ = ( +π£
βπ) |
3 | | eqid 2733 |
. . . . . . . . 9
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
4 | 3 | smfval 29846 |
. . . . . . . 8
β’ (
Β·π OLD βπ) = (2nd β(1st
βπ)) |
5 | 4 | eqcomi 2742 |
. . . . . . 7
β’
(2nd β(1st βπ)) = (
Β·π OLD βπ) |
6 | | eqid 2733 |
. . . . . . 7
β’
(0vecβπ) = (0vecβπ) |
7 | | nvtri.6 |
. . . . . . 7
β’ π =
(normCVβπ) |
8 | 1, 2, 5, 6, 7 | nvi 29855 |
. . . . . 6
β’ (π β NrmCVec β
(β¨πΊ, (2nd
β(1st βπ))β© β CVecOLD β§
π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = (0vecβπ)) β§ βπ¦ β β (πβ(π¦(2nd β(1st
βπ))π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))))) |
9 | 8 | simp3d 1145 |
. . . . 5
β’ (π β NrmCVec β
βπ₯ β π (((πβπ₯) = 0 β π₯ = (0vecβπ)) β§ βπ¦ β β (πβ(π¦(2nd β(1st
βπ))π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))) |
10 | | simp3 1139 |
. . . . . 6
β’ ((((πβπ₯) = 0 β π₯ = (0vecβπ)) β§ βπ¦ β β (πβ(π¦(2nd β(1st
βπ))π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) |
11 | 10 | ralimi 3084 |
. . . . 5
β’
(βπ₯ β
π (((πβπ₯) = 0 β π₯ = (0vecβπ)) β§ βπ¦ β β (πβ(π¦(2nd β(1st
βπ))π₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ₯ β π βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) |
12 | 9, 11 | syl 17 |
. . . 4
β’ (π β NrmCVec β
βπ₯ β π βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦))) |
13 | | fvoveq1 7429 |
. . . . . 6
β’ (π₯ = π΄ β (πβ(π₯πΊπ¦)) = (πβ(π΄πΊπ¦))) |
14 | | fveq2 6889 |
. . . . . . 7
β’ (π₯ = π΄ β (πβπ₯) = (πβπ΄)) |
15 | 14 | oveq1d 7421 |
. . . . . 6
β’ (π₯ = π΄ β ((πβπ₯) + (πβπ¦)) = ((πβπ΄) + (πβπ¦))) |
16 | 13, 15 | breq12d 5161 |
. . . . 5
β’ (π₯ = π΄ β ((πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)) β (πβ(π΄πΊπ¦)) β€ ((πβπ΄) + (πβπ¦)))) |
17 | | oveq2 7414 |
. . . . . . 7
β’ (π¦ = π΅ β (π΄πΊπ¦) = (π΄πΊπ΅)) |
18 | 17 | fveq2d 6893 |
. . . . . 6
β’ (π¦ = π΅ β (πβ(π΄πΊπ¦)) = (πβ(π΄πΊπ΅))) |
19 | | fveq2 6889 |
. . . . . . 7
β’ (π¦ = π΅ β (πβπ¦) = (πβπ΅)) |
20 | 19 | oveq2d 7422 |
. . . . . 6
β’ (π¦ = π΅ β ((πβπ΄) + (πβπ¦)) = ((πβπ΄) + (πβπ΅))) |
21 | 18, 20 | breq12d 5161 |
. . . . 5
β’ (π¦ = π΅ β ((πβ(π΄πΊπ¦)) β€ ((πβπ΄) + (πβπ¦)) β (πβ(π΄πΊπ΅)) β€ ((πβπ΄) + (πβπ΅)))) |
22 | 16, 21 | rspc2v 3622 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)) β (πβ(π΄πΊπ΅)) β€ ((πβπ΄) + (πβπ΅)))) |
23 | 12, 22 | syl5 34 |
. . 3
β’ ((π΄ β π β§ π΅ β π) β (π β NrmCVec β (πβ(π΄πΊπ΅)) β€ ((πβπ΄) + (πβπ΅)))) |
24 | 23 | 3impia 1118 |
. 2
β’ ((π΄ β π β§ π΅ β π β§ π β NrmCVec) β (πβ(π΄πΊπ΅)) β€ ((πβπ΄) + (πβπ΅))) |
25 | 24 | 3comr 1126 |
1
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄πΊπ΅)) β€ ((πβπ΄) + (πβπ΅))) |