Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . 7
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β πΌ β Fin) |
2 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
3 | | rrnval.1 |
. . . . . . . . . . . 12
β’ π = (β βm
πΌ) |
4 | 2, 3 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π₯ β (β βm πΌ)) |
5 | | elmapi 8840 |
. . . . . . . . . . 11
β’ (π₯ β (β
βm πΌ)
β π₯:πΌβΆβ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π₯:πΌβΆβ) |
7 | 6 | ffvelcdmda 7084 |
. . . . . . . . 9
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (π₯βπ) β β) |
8 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
9 | 8, 3 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π¦ β (β βm πΌ)) |
10 | | elmapi 8840 |
. . . . . . . . . . 11
β’ (π¦ β (β
βm πΌ)
β π¦:πΌβΆβ) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π¦:πΌβΆβ) |
12 | 11 | ffvelcdmda 7084 |
. . . . . . . . 9
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (π¦βπ) β β) |
13 | 7, 12 | resubcld 11639 |
. . . . . . . 8
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β ((π₯βπ) β (π¦βπ)) β β) |
14 | 13 | resqcld 14087 |
. . . . . . 7
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (((π₯βπ) β (π¦βπ))β2) β β) |
15 | 1, 14 | fsumrecl 15677 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β Ξ£π β πΌ (((π₯βπ) β (π¦βπ))β2) β β) |
16 | 13 | sqge0d 14099 |
. . . . . . 7
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β 0 β€ (((π₯βπ) β (π¦βπ))β2)) |
17 | 1, 14, 16 | fsumge0 15738 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β 0 β€ Ξ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) |
18 | 15, 17 | resqrtcld 15361 |
. . . . 5
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) β β) |
19 | 18 | ralrimivva 3201 |
. . . 4
β’ (πΌ β Fin β βπ₯ β π βπ¦ β π (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) β β) |
20 | | eqid 2733 |
. . . . 5
β’ (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) = (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) |
21 | 20 | fmpo 8051 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) β β β (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))):(π Γ π)βΆβ) |
22 | 19, 21 | sylib 217 |
. . 3
β’ (πΌ β Fin β (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))):(π Γ π)βΆβ) |
23 | 3 | rrnval 36684 |
. . . 4
β’ (πΌ β Fin β
(βnβπΌ) = (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)))) |
24 | 23 | feq1d 6700 |
. . 3
β’ (πΌ β Fin β
((βnβπΌ):(π Γ π)βΆβ β (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))):(π Γ π)βΆβ)) |
25 | 22, 24 | mpbird 257 |
. 2
β’ (πΌ β Fin β
(βnβπΌ):(π Γ π)βΆβ) |
26 | | sqrt00 15207 |
. . . . . . . 8
β’
((Ξ£π β
πΌ (((π₯βπ) β (π¦βπ))β2) β β β§ 0 β€
Ξ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) β
((ββΞ£π
β πΌ (((π₯βπ) β (π¦βπ))β2)) = 0 β Ξ£π β πΌ (((π₯βπ) β (π¦βπ))β2) = 0)) |
27 | 15, 17, 26 | syl2anc 585 |
. . . . . . 7
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β ((ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) = 0 β Ξ£π β πΌ (((π₯βπ) β (π¦βπ))β2) = 0)) |
28 | 1, 14, 16 | fsum00 15741 |
. . . . . . 7
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (Ξ£π β πΌ (((π₯βπ) β (π¦βπ))β2) = 0 β βπ β πΌ (((π₯βπ) β (π¦βπ))β2) = 0)) |
29 | 27, 28 | bitrd 279 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β ((ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) = 0 β βπ β πΌ (((π₯βπ) β (π¦βπ))β2) = 0)) |
30 | 13 | recnd 11239 |
. . . . . . . . 9
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β ((π₯βπ) β (π¦βπ)) β β) |
31 | | sqeq0 14082 |
. . . . . . . . 9
β’ (((π₯βπ) β (π¦βπ)) β β β ((((π₯βπ) β (π¦βπ))β2) = 0 β ((π₯βπ) β (π¦βπ)) = 0)) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β ((((π₯βπ) β (π¦βπ))β2) = 0 β ((π₯βπ) β (π¦βπ)) = 0)) |
33 | 7 | recnd 11239 |
. . . . . . . . 9
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (π₯βπ) β β) |
34 | 12 | recnd 11239 |
. . . . . . . . 9
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (π¦βπ) β β) |
35 | 33, 34 | subeq0ad 11578 |
. . . . . . . 8
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (((π₯βπ) β (π¦βπ)) = 0 β (π₯βπ) = (π¦βπ))) |
36 | 32, 35 | bitrd 279 |
. . . . . . 7
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β ((((π₯βπ) β (π¦βπ))β2) = 0 β (π₯βπ) = (π¦βπ))) |
37 | 36 | ralbidva 3176 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (βπ β πΌ (((π₯βπ) β (π¦βπ))β2) = 0 β βπ β πΌ (π₯βπ) = (π¦βπ))) |
38 | 29, 37 | bitrd 279 |
. . . . 5
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β ((ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) = 0 β βπ β πΌ (π₯βπ) = (π¦βπ))) |
39 | 3 | rrnmval 36685 |
. . . . . . 7
β’ ((πΌ β Fin β§ π₯ β π β§ π¦ β π) β (π₯(βnβπΌ)π¦) = (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) |
40 | 39 | 3expb 1121 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (π₯(βnβπΌ)π¦) = (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) |
41 | 40 | eqeq1d 2735 |
. . . . 5
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β ((π₯(βnβπΌ)π¦) = 0 β (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) = 0)) |
42 | 6 | ffnd 6716 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π₯ Fn πΌ) |
43 | 11 | ffnd 6716 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π¦ Fn πΌ) |
44 | | eqfnfv 7030 |
. . . . . 6
β’ ((π₯ Fn πΌ β§ π¦ Fn πΌ) β (π₯ = π¦ β βπ β πΌ (π₯βπ) = (π¦βπ))) |
45 | 42, 43, 44 | syl2anc 585 |
. . . . 5
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (π₯ = π¦ β βπ β πΌ (π₯βπ) = (π¦βπ))) |
46 | 38, 41, 45 | 3bitr4d 311 |
. . . 4
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β ((π₯(βnβπΌ)π¦) = 0 β π₯ = π¦)) |
47 | | simpll 766 |
. . . . . . . 8
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β πΌ β Fin) |
48 | 7 | adantlr 714 |
. . . . . . . . 9
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π₯βπ) β β) |
49 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β π§ β π) |
50 | 49, 3 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β π§ β (β βm πΌ)) |
51 | | elmapi 8840 |
. . . . . . . . . . 11
β’ (π§ β (β
βm πΌ)
β π§:πΌβΆβ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β π§:πΌβΆβ) |
53 | 52 | ffvelcdmda 7084 |
. . . . . . . . 9
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π§βπ) β β) |
54 | 48, 53 | resubcld 11639 |
. . . . . . . 8
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β ((π₯βπ) β (π§βπ)) β β) |
55 | 12 | adantlr 714 |
. . . . . . . . 9
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π¦βπ) β β) |
56 | 53, 55 | resubcld 11639 |
. . . . . . . 8
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β ((π§βπ) β (π¦βπ)) β β) |
57 | 47, 54, 56 | trirn 24909 |
. . . . . . 7
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (ββΞ£π β πΌ ((((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ)))β2)) β€
((ββΞ£π
β πΌ (((π₯βπ) β (π§βπ))β2)) + (ββΞ£π β πΌ (((π§βπ) β (π¦βπ))β2)))) |
58 | 33 | adantlr 714 |
. . . . . . . . . . 11
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π₯βπ) β β) |
59 | 53 | recnd 11239 |
. . . . . . . . . . 11
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π§βπ) β β) |
60 | 34 | adantlr 714 |
. . . . . . . . . . 11
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π¦βπ) β β) |
61 | 58, 59, 60 | npncand 11592 |
. . . . . . . . . 10
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ))) = ((π₯βπ) β (π¦βπ))) |
62 | 61 | oveq1d 7421 |
. . . . . . . . 9
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β ((((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ)))β2) = (((π₯βπ) β (π¦βπ))β2)) |
63 | 62 | sumeq2dv 15646 |
. . . . . . . 8
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β Ξ£π β πΌ ((((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ)))β2) = Ξ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) |
64 | 63 | fveq2d 6893 |
. . . . . . 7
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (ββΞ£π β πΌ ((((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ)))β2)) = (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) |
65 | | sqsubswap 14079 |
. . . . . . . . . . 11
β’ (((π₯βπ) β β β§ (π§βπ) β β) β (((π₯βπ) β (π§βπ))β2) = (((π§βπ) β (π₯βπ))β2)) |
66 | 58, 59, 65 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (((π₯βπ) β (π§βπ))β2) = (((π§βπ) β (π₯βπ))β2)) |
67 | 66 | sumeq2dv 15646 |
. . . . . . . . 9
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β Ξ£π β πΌ (((π₯βπ) β (π§βπ))β2) = Ξ£π β πΌ (((π§βπ) β (π₯βπ))β2)) |
68 | 67 | fveq2d 6893 |
. . . . . . . 8
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (ββΞ£π β πΌ (((π₯βπ) β (π§βπ))β2)) = (ββΞ£π β πΌ (((π§βπ) β (π₯βπ))β2))) |
69 | 68 | oveq1d 7421 |
. . . . . . 7
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β ((ββΞ£π β πΌ (((π₯βπ) β (π§βπ))β2)) + (ββΞ£π β πΌ (((π§βπ) β (π¦βπ))β2))) = ((ββΞ£π β πΌ (((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β πΌ (((π§βπ) β (π¦βπ))β2)))) |
70 | 57, 64, 69 | 3brtr3d 5179 |
. . . . . 6
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) β€ ((ββΞ£π β πΌ (((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β πΌ (((π§βπ) β (π¦βπ))β2)))) |
71 | 40 | adantr 482 |
. . . . . 6
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (π₯(βnβπΌ)π¦) = (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) |
72 | 3 | rrnmval 36685 |
. . . . . . . . . 10
β’ ((πΌ β Fin β§ π§ β π β§ π₯ β π) β (π§(βnβπΌ)π₯) = (ββΞ£π β πΌ (((π§βπ) β (π₯βπ))β2))) |
73 | 72 | 3adant3r 1182 |
. . . . . . . . 9
β’ ((πΌ β Fin β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π§(βnβπΌ)π₯) = (ββΞ£π β πΌ (((π§βπ) β (π₯βπ))β2))) |
74 | 3 | rrnmval 36685 |
. . . . . . . . . 10
β’ ((πΌ β Fin β§ π§ β π β§ π¦ β π) β (π§(βnβπΌ)π¦) = (ββΞ£π β πΌ (((π§βπ) β (π¦βπ))β2))) |
75 | 74 | 3adant3l 1181 |
. . . . . . . . 9
β’ ((πΌ β Fin β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π§(βnβπΌ)π¦) = (ββΞ£π β πΌ (((π§βπ) β (π¦βπ))β2))) |
76 | 73, 75 | oveq12d 7424 |
. . . . . . . 8
β’ ((πΌ β Fin β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β ((π§(βnβπΌ)π₯) + (π§(βnβπΌ)π¦)) = ((ββΞ£π β πΌ (((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β πΌ (((π§βπ) β (π¦βπ))β2)))) |
77 | 76 | 3expa 1119 |
. . . . . . 7
β’ (((πΌ β Fin β§ π§ β π) β§ (π₯ β π β§ π¦ β π)) β ((π§(βnβπΌ)π₯) + (π§(βnβπΌ)π¦)) = ((ββΞ£π β πΌ (((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β πΌ (((π§βπ) β (π¦βπ))β2)))) |
78 | 77 | an32s 651 |
. . . . . 6
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β ((π§(βnβπΌ)π₯) + (π§(βnβπΌ)π¦)) = ((ββΞ£π β πΌ (((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β πΌ (((π§βπ) β (π¦βπ))β2)))) |
79 | 70, 71, 78 | 3brtr4d 5180 |
. . . . 5
β’ (((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (π₯(βnβπΌ)π¦) β€ ((π§(βnβπΌ)π₯) + (π§(βnβπΌ)π¦))) |
80 | 79 | ralrimiva 3147 |
. . . 4
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β βπ§ β π (π₯(βnβπΌ)π¦) β€ ((π§(βnβπΌ)π₯) + (π§(βnβπΌ)π¦))) |
81 | 46, 80 | jca 513 |
. . 3
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (((π₯(βnβπΌ)π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯(βnβπΌ)π¦) β€ ((π§(βnβπΌ)π₯) + (π§(βnβπΌ)π¦)))) |
82 | 81 | ralrimivva 3201 |
. 2
β’ (πΌ β Fin β βπ₯ β π βπ¦ β π (((π₯(βnβπΌ)π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯(βnβπΌ)π¦) β€ ((π§(βnβπΌ)π₯) + (π§(βnβπΌ)π¦)))) |
83 | | ovex 7439 |
. . . 4
β’ (β
βm πΌ)
β V |
84 | 3, 83 | eqeltri 2830 |
. . 3
β’ π β V |
85 | | ismet 23821 |
. . 3
β’ (π β V β
((βnβπΌ) β (Metβπ) β
((βnβπΌ):(π Γ π)βΆβ β§ βπ₯ β π βπ¦ β π (((π₯(βnβπΌ)π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯(βnβπΌ)π¦) β€ ((π§(βnβπΌ)π₯) + (π§(βnβπΌ)π¦)))))) |
86 | 84, 85 | ax-mp 5 |
. 2
β’
((βnβπΌ) β (Metβπ) β
((βnβπΌ):(π Γ π)βΆβ β§ βπ₯ β π βπ¦ β π (((π₯(βnβπΌ)π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯(βnβπΌ)π¦) β€ ((π§(βnβπΌ)π₯) + (π§(βnβπΌ)π¦))))) |
87 | 25, 82, 86 | sylanbrc 584 |
1
β’ (πΌ β Fin β
(βnβπΌ) β (Metβπ)) |