Step | Hyp | Ref
| Expression |
1 | | nrmmetd.f |
. . 3
β’ (π β πΉ:πβΆβ) |
2 | | nrmmetd.g |
. . . 4
β’ (π β πΊ β Grp) |
3 | | nrmmetd.x |
. . . . 5
β’ π = (BaseβπΊ) |
4 | | nrmmetd.m |
. . . . 5
β’ β =
(-gβπΊ) |
5 | 3, 4 | grpsubf 18834 |
. . . 4
β’ (πΊ β Grp β β :(π Γ π)βΆπ) |
6 | 2, 5 | syl 17 |
. . 3
β’ (π β β :(π Γ π)βΆπ) |
7 | | fco 6696 |
. . 3
β’ ((πΉ:πβΆβ β§ β :(π Γ π)βΆπ) β (πΉ β β ):(π Γ π)βΆβ) |
8 | 1, 6, 7 | syl2anc 585 |
. 2
β’ (π β (πΉ β β ):(π Γ π)βΆβ) |
9 | | opelxpi 5674 |
. . . . . . . 8
β’ ((π β π β§ π β π) β β¨π, πβ© β (π Γ π)) |
10 | | fvco3 6944 |
. . . . . . . 8
β’ (( β :(π Γ π)βΆπ β§ β¨π, πβ© β (π Γ π)) β ((πΉ β β )ββ¨π, πβ©) = (πΉβ( β ββ¨π, πβ©))) |
11 | 6, 9, 10 | syl2an 597 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β ((πΉ β β )ββ¨π, πβ©) = (πΉβ( β ββ¨π, πβ©))) |
12 | | df-ov 7364 |
. . . . . . 7
β’ (π(πΉ β β )π) = ((πΉ β β )ββ¨π, πβ©) |
13 | | df-ov 7364 |
. . . . . . . 8
β’ (π β π) = ( β ββ¨π, πβ©) |
14 | 13 | fveq2i 6849 |
. . . . . . 7
β’ (πΉβ(π β π)) = (πΉβ( β ββ¨π, πβ©)) |
15 | 11, 12, 14 | 3eqtr4g 2798 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (π(πΉ β β )π) = (πΉβ(π β π))) |
16 | 15 | eqeq1d 2735 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β ((π(πΉ β β )π) = 0 β (πΉβ(π β π)) = 0)) |
17 | | nrmmetd.1 |
. . . . . . 7
β’ ((π β§ π₯ β π) β ((πΉβπ₯) = 0 β π₯ = 0 )) |
18 | 17 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ₯ β π ((πΉβπ₯) = 0 β π₯ = 0 )) |
19 | 3, 4 | grpsubcl 18835 |
. . . . . . . 8
β’ ((πΊ β Grp β§ π β π β§ π β π) β (π β π) β π) |
20 | 19 | 3expb 1121 |
. . . . . . 7
β’ ((πΊ β Grp β§ (π β π β§ π β π)) β (π β π) β π) |
21 | 2, 20 | sylan 581 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (π β π) β π) |
22 | | fveq2 6846 |
. . . . . . . . 9
β’ (π₯ = (π β π) β (πΉβπ₯) = (πΉβ(π β π))) |
23 | 22 | eqeq1d 2735 |
. . . . . . . 8
β’ (π₯ = (π β π) β ((πΉβπ₯) = 0 β (πΉβ(π β π)) = 0)) |
24 | | eqeq1 2737 |
. . . . . . . 8
β’ (π₯ = (π β π) β (π₯ = 0 β (π β π) = 0 )) |
25 | 23, 24 | bibi12d 346 |
. . . . . . 7
β’ (π₯ = (π β π) β (((πΉβπ₯) = 0 β π₯ = 0 ) β ((πΉβ(π β π)) = 0 β (π β π) = 0 ))) |
26 | 25 | rspccva 3582 |
. . . . . 6
β’
((βπ₯ β
π ((πΉβπ₯) = 0 β π₯ = 0 ) β§ (π β π) β π) β ((πΉβ(π β π)) = 0 β (π β π) = 0 )) |
27 | 18, 21, 26 | syl2an2r 684 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β ((πΉβ(π β π)) = 0 β (π β π) = 0 )) |
28 | | nrmmetd.z |
. . . . . . . 8
β’ 0 =
(0gβπΊ) |
29 | 3, 28, 4 | grpsubeq0 18841 |
. . . . . . 7
β’ ((πΊ β Grp β§ π β π β§ π β π) β ((π β π) = 0 β π = π)) |
30 | 29 | 3expb 1121 |
. . . . . 6
β’ ((πΊ β Grp β§ (π β π β§ π β π)) β ((π β π) = 0 β π = π)) |
31 | 2, 30 | sylan 581 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β ((π β π) = 0 β π = π)) |
32 | 16, 27, 31 | 3bitrd 305 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β ((π(πΉ β β )π) = 0 β π = π)) |
33 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β πΉ:πβΆβ) |
34 | 21 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (π β π) β π) |
35 | 33, 34 | ffvelcdmd 7040 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ(π β π)) β β) |
36 | 2 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β πΊ β Grp) |
37 | | simprll 778 |
. . . . . . . . . . 11
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β π β π) |
38 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β π β π) |
39 | 3, 4 | grpsubcl 18835 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π β π β§ π β π) β (π β π) β π) |
40 | 36, 37, 38, 39 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (π β π) β π) |
41 | 33, 40 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ(π β π)) β β) |
42 | | simprlr 779 |
. . . . . . . . . . 11
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β π β π) |
43 | 3, 4 | grpsubcl 18835 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π β π β§ π β π) β (π β π) β π) |
44 | 36, 42, 38, 43 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (π β π) β π) |
45 | 33, 44 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ(π β π)) β β) |
46 | 41, 45 | readdcld 11192 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β ((πΉβ(π β π)) + (πΉβ(π β π))) β β) |
47 | 3, 4 | grpsubcl 18835 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π β π β§ π β π) β (π β π) β π) |
48 | 36, 38, 37, 47 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (π β π) β π) |
49 | 33, 48 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ(π β π)) β β) |
50 | 3, 4 | grpsubcl 18835 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π β π β§ π β π) β (π β π) β π) |
51 | 36, 38, 42, 50 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (π β π) β π) |
52 | 33, 51 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ(π β π)) β β) |
53 | 49, 52 | readdcld 11192 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β ((πΉβ(π β π)) + (πΉβ(π β π))) β β) |
54 | 3, 4 | grpnnncan2 18852 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ (π β π β§ π β π β§ π β π)) β ((π β π) β (π β π)) = (π β π)) |
55 | 36, 37, 42, 38, 54 | syl13anc 1373 |
. . . . . . . . . 10
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β ((π β π) β (π β π)) = (π β π)) |
56 | 55 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ((π β π) β (π β π))) = (πΉβ(π β π))) |
57 | | nrmmetd.2 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
58 | 57 | ralrimivva 3194 |
. . . . . . . . . . 11
β’ (π β βπ₯ β π βπ¦ β π (πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
59 | 58 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β βπ₯ β π βπ¦ β π (πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
60 | | fvoveq1 7384 |
. . . . . . . . . . . 12
β’ (π₯ = (π β π) β (πΉβ(π₯ β π¦)) = (πΉβ((π β π) β π¦))) |
61 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π₯ = (π β π) β (πΉβπ₯) = (πΉβ(π β π))) |
62 | 61 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ (π₯ = (π β π) β ((πΉβπ₯) + (πΉβπ¦)) = ((πΉβ(π β π)) + (πΉβπ¦))) |
63 | 60, 62 | breq12d 5122 |
. . . . . . . . . . 11
β’ (π₯ = (π β π) β ((πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)) β (πΉβ((π β π) β π¦)) β€ ((πΉβ(π β π)) + (πΉβπ¦)))) |
64 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π¦ = (π β π) β ((π β π) β π¦) = ((π β π) β (π β π))) |
65 | 64 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π¦ = (π β π) β (πΉβ((π β π) β π¦)) = (πΉβ((π β π) β (π β π)))) |
66 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π¦ = (π β π) β (πΉβπ¦) = (πΉβ(π β π))) |
67 | 66 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ (π¦ = (π β π) β ((πΉβ(π β π)) + (πΉβπ¦)) = ((πΉβ(π β π)) + (πΉβ(π β π)))) |
68 | 65, 67 | breq12d 5122 |
. . . . . . . . . . 11
β’ (π¦ = (π β π) β ((πΉβ((π β π) β π¦)) β€ ((πΉβ(π β π)) + (πΉβπ¦)) β (πΉβ((π β π) β (π β π))) β€ ((πΉβ(π β π)) + (πΉβ(π β π))))) |
69 | 63, 68 | rspc2va 3593 |
. . . . . . . . . 10
β’ ((((π β π) β π β§ (π β π) β π) β§ βπ₯ β π βπ¦ β π (πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) β (πΉβ((π β π) β (π β π))) β€ ((πΉβ(π β π)) + (πΉβ(π β π)))) |
70 | 40, 44, 59, 69 | syl21anc 837 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ((π β π) β (π β π))) β€ ((πΉβ(π β π)) + (πΉβ(π β π)))) |
71 | 56, 70 | eqbrtrrd 5133 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ(π β π)) β€ ((πΉβ(π β π)) + (πΉβ(π β π)))) |
72 | | eleq1w 2817 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π β π β π)) |
73 | 72 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β π β§ π β π) β (π β π β§ π β π))) |
74 | 73 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π = π β ((π β§ (π β π β§ π β π)) β (π β§ (π β π β§ π β π)))) |
75 | | oveq2 7369 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π) = (π β π)) |
76 | 75 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβ(π β π)) = (πΉβ(π β π))) |
77 | | fvoveq1 7384 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβ(π β π)) = (πΉβ(π β π))) |
78 | 76, 77 | breq12d 5122 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβ(π β π)) β€ (πΉβ(π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π)))) |
79 | 74, 78 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β (((π β§ (π β π β§ π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π))) β ((π β§ (π β π β§ π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π))))) |
80 | 2 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π β π)) β πΊ β Grp) |
81 | 3, 28 | grpidcl 18786 |
. . . . . . . . . . . . . 14
β’ (πΊ β Grp β 0 β π) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π β π)) β 0 β π) |
83 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π β π)) β π β π) |
84 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π β π)) β π β π) |
85 | 3, 4 | grpsubcl 18835 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§ π β π β§ π β π) β (π β π) β π) |
86 | 80, 83, 84, 85 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π β π)) β (π β π) β π) |
87 | 58 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π β π)) β βπ₯ β π βπ¦ β π (πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
88 | | fvoveq1 7384 |
. . . . . . . . . . . . . . 15
β’ (π₯ = 0 β (πΉβ(π₯ β π¦)) = (πΉβ( 0 β π¦))) |
89 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = 0 β (πΉβπ₯) = (πΉβ 0 )) |
90 | 89 | oveq1d 7376 |
. . . . . . . . . . . . . . 15
β’ (π₯ = 0 β ((πΉβπ₯) + (πΉβπ¦)) = ((πΉβ 0 ) + (πΉβπ¦))) |
91 | 88, 90 | breq12d 5122 |
. . . . . . . . . . . . . 14
β’ (π₯ = 0 β ((πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)) β (πΉβ( 0 β π¦)) β€ ((πΉβ 0 ) + (πΉβπ¦)))) |
92 | | oveq2 7369 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (π β π) β ( 0 β π¦) = ( 0 β (π β π))) |
93 | 92 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π β π) β (πΉβ( 0 β π¦)) = (πΉβ( 0 β (π β π)))) |
94 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (π β π) β (πΉβπ¦) = (πΉβ(π β π))) |
95 | 94 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π β π) β ((πΉβ 0 ) + (πΉβπ¦)) = ((πΉβ 0 ) + (πΉβ(π β π)))) |
96 | 93, 95 | breq12d 5122 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π β π) β ((πΉβ( 0 β π¦)) β€ ((πΉβ 0 ) + (πΉβπ¦)) β (πΉβ( 0 β (π β π))) β€ ((πΉβ 0 ) + (πΉβ(π β π))))) |
97 | 91, 96 | rspc2va 3593 |
. . . . . . . . . . . . 13
β’ ((( 0 β π β§ (π β π) β π) β§ βπ₯ β π βπ¦ β π (πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) β (πΉβ( 0 β (π β π))) β€ ((πΉβ 0 ) + (πΉβ(π β π)))) |
98 | 82, 86, 87, 97 | syl21anc 837 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π β π)) β (πΉβ( 0 β (π β π))) β€ ((πΉβ 0 ) + (πΉβ(π β π)))) |
99 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(invgβπΊ) = (invgβπΊ) |
100 | 3, 4, 99, 28 | grpinvval2 18838 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β Grp β§ (π β π) β π) β ((invgβπΊ)β(π β π)) = ( 0 β (π β π))) |
101 | 2, 86, 100 | syl2an2r 684 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π β π)) β ((invgβπΊ)β(π β π)) = ( 0 β (π β π))) |
102 | 3, 4, 99 | grpinvsub 18837 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β Grp β§ π β π β§ π β π) β ((invgβπΊ)β(π β π)) = (π β π)) |
103 | 80, 83, 84, 102 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π β π)) β ((invgβπΊ)β(π β π)) = (π β π)) |
104 | 101, 103 | eqtr3d 2775 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π β π)) β ( 0 β (π β π)) = (π β π)) |
105 | 104 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π β π)) β (πΉβ( 0 β (π β π))) = (πΉβ(π β π))) |
106 | 2, 81 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β 0 β π) |
107 | | pm5.501 367 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = 0 β ((πΉβπ₯) = 0 β (π₯ = 0 β (πΉβπ₯) = 0))) |
108 | | bicom 221 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ = 0 β (πΉβπ₯) = 0) β ((πΉβπ₯) = 0 β π₯ = 0 )) |
109 | 107, 108 | bitrdi 287 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = 0 β ((πΉβπ₯) = 0 β ((πΉβπ₯) = 0 β π₯ = 0 ))) |
110 | 89 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = 0 β ((πΉβπ₯) = 0 β (πΉβ 0 ) = 0)) |
111 | 109, 110 | bitr3d 281 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = 0 β (((πΉβπ₯) = 0 β π₯ = 0 ) β (πΉβ 0 ) = 0)) |
112 | 111 | rspccva 3582 |
. . . . . . . . . . . . . . . 16
β’
((βπ₯ β
π ((πΉβπ₯) = 0 β π₯ = 0 ) β§ 0 β π) β (πΉβ 0 ) = 0) |
113 | 18, 106, 112 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉβ 0 ) = 0) |
114 | 113 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π β π)) β (πΉβ 0 ) = 0) |
115 | 114 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π β π)) β ((πΉβ 0 ) + (πΉβ(π β π))) = (0 + (πΉβ(π β π)))) |
116 | 1 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π β π)) β πΉ:πβΆβ) |
117 | 116, 86 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π β π)) β (πΉβ(π β π)) β β) |
118 | 117 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π β π)) β (πΉβ(π β π)) β β) |
119 | 118 | addid2d 11364 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π β π)) β (0 + (πΉβ(π β π))) = (πΉβ(π β π))) |
120 | 115, 119 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π β π)) β ((πΉβ 0 ) + (πΉβ(π β π))) = (πΉβ(π β π))) |
121 | 98, 105, 120 | 3brtr3d 5140 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π))) |
122 | 79, 121 | chvarvv 2003 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π))) |
123 | 122 | adantrlr 722 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π))) |
124 | | eleq1w 2817 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π β π β π)) |
125 | 124 | anbi1d 631 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β π β§ π β π) β (π β π β§ π β π))) |
126 | 125 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π = π β ((π β§ (π β π β§ π β π)) β (π β§ (π β π β§ π β π)))) |
127 | | fvoveq1 7384 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβ(π β π)) = (πΉβ(π β π))) |
128 | | oveq2 7369 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π) = (π β π)) |
129 | 128 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβ(π β π)) = (πΉβ(π β π))) |
130 | 127, 129 | breq12d 5122 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβ(π β π)) β€ (πΉβ(π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π)))) |
131 | 126, 130 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β (((π β§ (π β π β§ π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π))) β ((π β§ (π β π β§ π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π))))) |
132 | 131, 122 | chvarvv 2003 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π))) |
133 | 132 | adantrll 721 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ(π β π)) β€ (πΉβ(π β π))) |
134 | 41, 45, 49, 52, 123, 133 | le2addd 11782 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β ((πΉβ(π β π)) + (πΉβ(π β π))) β€ ((πΉβ(π β π)) + (πΉβ(π β π)))) |
135 | 35, 46, 53, 71, 134 | letrd 11320 |
. . . . . . 7
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (πΉβ(π β π)) β€ ((πΉβ(π β π)) + (πΉβ(π β π)))) |
136 | 15 | adantrr 716 |
. . . . . . 7
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (π(πΉ β β )π) = (πΉβ(π β π))) |
137 | | opelxpi 5674 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β β¨π, πβ© β (π Γ π)) |
138 | 38, 37, 137 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β β¨π, πβ© β (π Γ π)) |
139 | | fvco3 6944 |
. . . . . . . . . 10
β’ (( β :(π Γ π)βΆπ β§ β¨π, πβ© β (π Γ π)) β ((πΉ β β )ββ¨π, πβ©) = (πΉβ( β ββ¨π, πβ©))) |
140 | 6, 138, 139 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β ((πΉ β β )ββ¨π, πβ©) = (πΉβ( β ββ¨π, πβ©))) |
141 | | df-ov 7364 |
. . . . . . . . 9
β’ (π(πΉ β β )π) = ((πΉ β β )ββ¨π, πβ©) |
142 | | df-ov 7364 |
. . . . . . . . . 10
β’ (π β π) = ( β ββ¨π, πβ©) |
143 | 142 | fveq2i 6849 |
. . . . . . . . 9
β’ (πΉβ(π β π)) = (πΉβ( β ββ¨π, πβ©)) |
144 | 140, 141,
143 | 3eqtr4g 2798 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (π(πΉ β β )π) = (πΉβ(π β π))) |
145 | | opelxpi 5674 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β β¨π, πβ© β (π Γ π)) |
146 | 38, 42, 145 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β β¨π, πβ© β (π Γ π)) |
147 | | fvco3 6944 |
. . . . . . . . . 10
β’ (( β :(π Γ π)βΆπ β§ β¨π, πβ© β (π Γ π)) β ((πΉ β β )ββ¨π, πβ©) = (πΉβ( β ββ¨π, πβ©))) |
148 | 6, 146, 147 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β ((πΉ β β )ββ¨π, πβ©) = (πΉβ( β ββ¨π, πβ©))) |
149 | | df-ov 7364 |
. . . . . . . . 9
β’ (π(πΉ β β )π) = ((πΉ β β )ββ¨π, πβ©) |
150 | | df-ov 7364 |
. . . . . . . . . 10
β’ (π β π) = ( β ββ¨π, πβ©) |
151 | 150 | fveq2i 6849 |
. . . . . . . . 9
β’ (πΉβ(π β π)) = (πΉβ( β ββ¨π, πβ©)) |
152 | 148, 149,
151 | 3eqtr4g 2798 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (π(πΉ β β )π) = (πΉβ(π β π))) |
153 | 144, 152 | oveq12d 7379 |
. . . . . . 7
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β ((π(πΉ β β )π) + (π(πΉ β β )π)) = ((πΉβ(π β π)) + (πΉβ(π β π)))) |
154 | 135, 136,
153 | 3brtr4d 5141 |
. . . . . 6
β’ ((π β§ ((π β π β§ π β π) β§ π β π)) β (π(πΉ β β )π) β€ ((π(πΉ β β )π) + (π(πΉ β β )π))) |
155 | 154 | expr 458 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (π β π β (π(πΉ β β )π) β€ ((π(πΉ β β )π) + (π(πΉ β β )π)))) |
156 | 155 | ralrimiv 3139 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β βπ β π (π(πΉ β β )π) β€ ((π(πΉ β β )π) + (π(πΉ β β )π))) |
157 | 32, 156 | jca 513 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β (((π(πΉ β β )π) = 0 β π = π) β§ βπ β π (π(πΉ β β )π) β€ ((π(πΉ β β )π) + (π(πΉ β β )π)))) |
158 | 157 | ralrimivva 3194 |
. 2
β’ (π β βπ β π βπ β π (((π(πΉ β β )π) = 0 β π = π) β§ βπ β π (π(πΉ β β )π) β€ ((π(πΉ β β )π) + (π(πΉ β β )π)))) |
159 | 3 | fvexi 6860 |
. . 3
β’ π β V |
160 | | ismet 23699 |
. . 3
β’ (π β V β ((πΉ β β ) β
(Metβπ) β
((πΉ β β
):(π Γ π)βΆβ β§
βπ β π βπ β π (((π(πΉ β β )π) = 0 β π = π) β§ βπ β π (π(πΉ β β )π) β€ ((π(πΉ β β )π) + (π(πΉ β β )π)))))) |
161 | 159, 160 | ax-mp 5 |
. 2
β’ ((πΉ β β ) β
(Metβπ) β
((πΉ β β
):(π Γ π)βΆβ β§
βπ β π βπ β π (((π(πΉ β β )π) = 0 β π = π) β§ βπ β π (π(πΉ β β )π) β€ ((π(πΉ β β )π) + (π(πΉ β β )π))))) |
162 | 8, 158, 161 | sylanbrc 584 |
1
β’ (π β (πΉ β β ) β
(Metβπ)) |