Step | Hyp | Ref
| Expression |
1 | | rrxmval.1 |
. . . . . . . . 9
β’ π = {β β (β βm πΌ) β£ β finSupp 0} |
2 | | simprl 770 |
. . . . . . . . 9
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
3 | 1, 2 | rrxfsupp 24769 |
. . . . . . . 8
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (π₯ supp 0) β Fin) |
4 | | simprr 772 |
. . . . . . . . 9
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
5 | 1, 4 | rrxfsupp 24769 |
. . . . . . . 8
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (π¦ supp 0) β Fin) |
6 | | unfi 9117 |
. . . . . . . 8
β’ (((π₯ supp 0) β Fin β§ (π¦ supp 0) β Fin) β
((π₯ supp 0) βͺ (π¦ supp 0)) β
Fin) |
7 | 3, 5, 6 | syl2anc 585 |
. . . . . . 7
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β ((π₯ supp 0) βͺ (π¦ supp 0)) β Fin) |
8 | 1, 2 | rrxsuppss 24770 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (π₯ supp 0) β πΌ) |
9 | 1, 4 | rrxsuppss 24770 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (π¦ supp 0) β πΌ) |
10 | 8, 9 | unssd 4147 |
. . . . . . . . 9
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β ((π₯ supp 0) βͺ (π¦ supp 0)) β πΌ) |
11 | 10 | sselda 3945 |
. . . . . . . 8
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β ((π₯ supp 0) βͺ (π¦ supp 0))) β π β πΌ) |
12 | 1, 2 | rrxf 24768 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β π₯:πΌβΆβ) |
13 | 12 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (π₯βπ) β β) |
14 | 1, 4 | rrxf 24768 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β π¦:πΌβΆβ) |
15 | 14 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (π¦βπ) β β) |
16 | 13, 15 | resubcld 11584 |
. . . . . . . . 9
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β ((π₯βπ) β (π¦βπ)) β β) |
17 | 16 | resqcld 14031 |
. . . . . . . 8
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (((π₯βπ) β (π¦βπ))β2) β β) |
18 | 11, 17 | syldan 592 |
. . . . . . 7
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β ((π₯ supp 0) βͺ (π¦ supp 0))) β (((π₯βπ) β (π¦βπ))β2) β β) |
19 | 7, 18 | fsumrecl 15620 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β Ξ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2) β β) |
20 | 16 | sqge0d 14043 |
. . . . . . . 8
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β 0 β€ (((π₯βπ) β (π¦βπ))β2)) |
21 | 11, 20 | syldan 592 |
. . . . . . 7
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β ((π₯ supp 0) βͺ (π¦ supp 0))) β 0 β€ (((π₯βπ) β (π¦βπ))β2)) |
22 | 7, 18, 21 | fsumge0 15681 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β 0 β€ Ξ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) |
23 | 19, 22 | resqrtcld 15303 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) β β) |
24 | 23 | ralrimivva 3198 |
. . . 4
β’ (πΌ β π β βπ₯ β π βπ¦ β π (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) β β) |
25 | | eqid 2737 |
. . . . 5
β’ (π₯ β π, π¦ β π β¦ (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2))) = (π₯ β π, π¦ β π β¦ (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2))) |
26 | 25 | fmpo 8001 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) β β β (π₯ β π, π¦ β π β¦ (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2))):(π Γ π)βΆβ) |
27 | 24, 26 | sylib 217 |
. . 3
β’ (πΌ β π β (π₯ β π, π¦ β π β¦ (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2))):(π Γ π)βΆβ) |
28 | | rrxmval.d |
. . . . 5
β’ π· =
(distβ(β^βπΌ)) |
29 | 1, 28 | rrxmfval 24773 |
. . . 4
β’ (πΌ β π β π· = (π₯ β π, π¦ β π β¦ (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)))) |
30 | 29 | feq1d 6654 |
. . 3
β’ (πΌ β π β (π·:(π Γ π)βΆβ β (π₯ β π, π¦ β π β¦ (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2))):(π Γ π)βΆβ)) |
31 | 27, 30 | mpbird 257 |
. 2
β’ (πΌ β π β π·:(π Γ π)βΆβ) |
32 | | sqrt00 15149 |
. . . . . . 7
β’
((Ξ£π β
((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2) β β β§ 0 β€
Ξ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) β
((ββΞ£π
β ((π₯ supp 0) βͺ
(π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) = 0 β Ξ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2) = 0)) |
33 | 19, 22, 32 | syl2anc 585 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β ((ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) = 0 β Ξ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2) = 0)) |
34 | 7, 18, 21 | fsum00 15684 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (Ξ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2) = 0 β βπ β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2) = 0)) |
35 | 16 | recnd 11184 |
. . . . . . . . . 10
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β ((π₯βπ) β (π¦βπ)) β β) |
36 | | sqeq0 14026 |
. . . . . . . . . 10
β’ (((π₯βπ) β (π¦βπ)) β β β ((((π₯βπ) β (π¦βπ))β2) = 0 β ((π₯βπ) β (π¦βπ)) = 0)) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β ((((π₯βπ) β (π¦βπ))β2) = 0 β ((π₯βπ) β (π¦βπ)) = 0)) |
38 | 13 | recnd 11184 |
. . . . . . . . . 10
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (π₯βπ) β β) |
39 | 15 | recnd 11184 |
. . . . . . . . . 10
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (π¦βπ) β β) |
40 | 38, 39 | subeq0ad 11523 |
. . . . . . . . 9
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β (((π₯βπ) β (π¦βπ)) = 0 β (π₯βπ) = (π¦βπ))) |
41 | 37, 40 | bitrd 279 |
. . . . . . . 8
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β πΌ) β ((((π₯βπ) β (π¦βπ))β2) = 0 β (π₯βπ) = (π¦βπ))) |
42 | 11, 41 | syldan 592 |
. . . . . . 7
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β ((π₯ supp 0) βͺ (π¦ supp 0))) β ((((π₯βπ) β (π¦βπ))β2) = 0 β (π₯βπ) = (π¦βπ))) |
43 | 42 | ralbidva 3173 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (βπ β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2) = 0 β βπ β ((π₯ supp 0) βͺ (π¦ supp 0))(π₯βπ) = (π¦βπ))) |
44 | 33, 34, 43 | 3bitrd 305 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β ((ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) = 0 β βπ β ((π₯ supp 0) βͺ (π¦ supp 0))(π₯βπ) = (π¦βπ))) |
45 | 1, 28 | rrxmval 24772 |
. . . . . . 7
β’ ((πΌ β π β§ π₯ β π β§ π¦ β π) β (π₯π·π¦) = (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2))) |
46 | 45 | 3expb 1121 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) = (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2))) |
47 | 46 | eqeq1d 2739 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) = 0)) |
48 | 12 | ffnd 6670 |
. . . . . . 7
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β π₯ Fn πΌ) |
49 | 14 | ffnd 6670 |
. . . . . . 7
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β π¦ Fn πΌ) |
50 | | eqfnfv 6983 |
. . . . . . 7
β’ ((π₯ Fn πΌ β§ π¦ Fn πΌ) β (π₯ = π¦ β βπ β πΌ (π₯βπ) = (π¦βπ))) |
51 | 48, 49, 50 | syl2anc 585 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (π₯ = π¦ β βπ β πΌ (π₯βπ) = (π¦βπ))) |
52 | | ssun1 4133 |
. . . . . . . . . . 11
β’ (π₯ supp 0) β ((π₯ supp 0) βͺ (π¦ supp 0)) |
53 | 52 | a1i 11 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (π₯ supp 0) β ((π₯ supp 0) βͺ (π¦ supp 0))) |
54 | | simpl 484 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β πΌ β π) |
55 | | 0red 11159 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β 0 β β) |
56 | 12, 53, 54, 55 | suppssr 8128 |
. . . . . . . . 9
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β (πΌ β ((π₯ supp 0) βͺ (π¦ supp 0)))) β (π₯βπ) = 0) |
57 | | ssun2 4134 |
. . . . . . . . . . 11
β’ (π¦ supp 0) β ((π₯ supp 0) βͺ (π¦ supp 0)) |
58 | 57 | a1i 11 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (π¦ supp 0) β ((π₯ supp 0) βͺ (π¦ supp 0))) |
59 | 14, 58, 54, 55 | suppssr 8128 |
. . . . . . . . 9
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β (πΌ β ((π₯ supp 0) βͺ (π¦ supp 0)))) β (π¦βπ) = 0) |
60 | 56, 59 | eqtr4d 2780 |
. . . . . . . 8
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π β (πΌ β ((π₯ supp 0) βͺ (π¦ supp 0)))) β (π₯βπ) = (π¦βπ)) |
61 | 60 | ralrimiva 3144 |
. . . . . . 7
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β βπ β (πΌ β ((π₯ supp 0) βͺ (π¦ supp 0)))(π₯βπ) = (π¦βπ)) |
62 | 10, 61 | raldifeq 4452 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (βπ β ((π₯ supp 0) βͺ (π¦ supp 0))(π₯βπ) = (π¦βπ) β βπ β πΌ (π₯βπ) = (π¦βπ))) |
63 | 51, 62 | bitr4d 282 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (π₯ = π¦ β βπ β ((π₯ supp 0) βͺ (π¦ supp 0))(π₯βπ) = (π¦βπ))) |
64 | 44, 47, 63 | 3bitr4d 311 |
. . . 4
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β π₯ = π¦)) |
65 | 7 | 3adant2 1132 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β ((π₯ supp 0) βͺ (π¦ supp 0)) β Fin) |
66 | | simp2 1138 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β π§ β π) |
67 | 1, 66 | rrxfsupp 24769 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π§ supp 0) β Fin) |
68 | | unfi 9117 |
. . . . . . . . . . 11
β’ ((((π₯ supp 0) βͺ (π¦ supp 0)) β Fin β§
(π§ supp 0) β Fin)
β (((π₯ supp 0) βͺ
(π¦ supp 0)) βͺ (π§ supp 0)) β
Fin) |
69 | 65, 67, 68 | syl2anc 585 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0)) β Fin) |
70 | 69 | 3expa 1119 |
. . . . . . . . 9
β’ (((πΌ β π β§ π§ β π) β§ (π₯ β π β§ π¦ β π)) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0)) β Fin) |
71 | 70 | an32s 651 |
. . . . . . . 8
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0)) β Fin) |
72 | 10 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β ((π₯ supp 0) βͺ (π¦ supp 0)) β πΌ) |
73 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β π§ β π) |
74 | 1, 73 | rrxsuppss 24770 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (π§ supp 0) β πΌ) |
75 | 72, 74 | unssd 4147 |
. . . . . . . . . 10
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0)) β πΌ) |
76 | 75 | sselda 3945 |
. . . . . . . . 9
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) β π β πΌ) |
77 | 13 | adantlr 714 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π₯βπ) β β) |
78 | 1, 73 | rrxf 24768 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β π§:πΌβΆβ) |
79 | 78 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π§βπ) β β) |
80 | 77, 79 | resubcld 11584 |
. . . . . . . . 9
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β ((π₯βπ) β (π§βπ)) β β) |
81 | 76, 80 | syldan 592 |
. . . . . . . 8
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) β ((π₯βπ) β (π§βπ)) β β) |
82 | 15 | adantlr 714 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π¦βπ) β β) |
83 | 79, 82 | resubcld 11584 |
. . . . . . . . 9
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β ((π§βπ) β (π¦βπ)) β β) |
84 | 76, 83 | syldan 592 |
. . . . . . . 8
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) β ((π§βπ) β (π¦βπ)) β β) |
85 | 71, 81, 84 | trirn 24767 |
. . . . . . 7
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))((((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ)))β2)) β€
((ββΞ£π
β (((π₯ supp 0) βͺ
(π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π§βπ))β2)) + (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2)))) |
86 | 38 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π₯βπ) β β) |
87 | 79 | recnd 11184 |
. . . . . . . . . . . 12
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π§βπ) β β) |
88 | 39 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (π¦βπ) β β) |
89 | 86, 87, 88 | npncand 11537 |
. . . . . . . . . . 11
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ))) = ((π₯βπ) β (π¦βπ))) |
90 | 89 | oveq1d 7373 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β ((((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ)))β2) = (((π₯βπ) β (π¦βπ))β2)) |
91 | 76, 90 | syldan 592 |
. . . . . . . . 9
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) β ((((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ)))β2) = (((π₯βπ) β (π¦βπ))β2)) |
92 | 91 | sumeq2dv 15589 |
. . . . . . . 8
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β Ξ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))((((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ)))β2) = Ξ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π¦βπ))β2)) |
93 | 92 | fveq2d 6847 |
. . . . . . 7
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))((((π₯βπ) β (π§βπ)) + ((π§βπ) β (π¦βπ)))β2)) = (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π¦βπ))β2))) |
94 | | sqsubswap 14023 |
. . . . . . . . . . . 12
β’ (((π₯βπ) β β β§ (π§βπ) β β) β (((π₯βπ) β (π§βπ))β2) = (((π§βπ) β (π₯βπ))β2)) |
95 | 86, 87, 94 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β πΌ) β (((π₯βπ) β (π§βπ))β2) = (((π§βπ) β (π₯βπ))β2)) |
96 | 76, 95 | syldan 592 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β§ π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) β (((π₯βπ) β (π§βπ))β2) = (((π§βπ) β (π₯βπ))β2)) |
97 | 96 | sumeq2dv 15589 |
. . . . . . . . 9
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β Ξ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π§βπ))β2) = Ξ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2)) |
98 | 97 | fveq2d 6847 |
. . . . . . . 8
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π§βπ))β2)) = (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2))) |
99 | 98 | oveq1d 7373 |
. . . . . . 7
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β ((ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π§βπ))β2)) + (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2))) = ((ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2)))) |
100 | 85, 93, 99 | 3brtr3d 5137 |
. . . . . 6
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π¦βπ))β2)) β€ ((ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2)))) |
101 | 46 | adantr 482 |
. . . . . . 7
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (π₯π·π¦) = (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2))) |
102 | | simp1 1137 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β πΌ β π) |
103 | 2 | 3adant2 1132 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
104 | 4 | 3adant2 1132 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
105 | 1, 103 | rrxsuppss 24770 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π₯ supp 0) β πΌ) |
106 | 1, 104 | rrxsuppss 24770 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π¦ supp 0) β πΌ) |
107 | 105, 106 | unssd 4147 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β ((π₯ supp 0) βͺ (π¦ supp 0)) β πΌ) |
108 | 1, 66 | rrxsuppss 24770 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π§ supp 0) β πΌ) |
109 | 107, 108 | unssd 4147 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0)) β πΌ) |
110 | | ssun1 4133 |
. . . . . . . . . . . 12
β’ ((π₯ supp 0) βͺ (π¦ supp 0)) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0)) |
111 | 110 | a1i 11 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β ((π₯ supp 0) βͺ (π¦ supp 0)) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) |
112 | 1, 28, 102, 103, 104, 109, 69, 111 | rrxmetlem 24774 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β Ξ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2) = Ξ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π¦βπ))β2)) |
113 | 112 | fveq2d 6847 |
. . . . . . . . 9
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) = (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π¦βπ))β2))) |
114 | 113 | 3expa 1119 |
. . . . . . . 8
β’ (((πΌ β π β§ π§ β π) β§ (π₯ β π β§ π¦ β π)) β (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) = (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π¦βπ))β2))) |
115 | 114 | an32s 651 |
. . . . . . 7
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (ββΞ£π β ((π₯ supp 0) βͺ (π¦ supp 0))(((π₯βπ) β (π¦βπ))β2)) = (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π¦βπ))β2))) |
116 | 101, 115 | eqtrd 2777 |
. . . . . 6
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (π₯π·π¦) = (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π₯βπ) β (π¦βπ))β2))) |
117 | 1, 28 | rrxmval 24772 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ π₯ β π) β (π§π·π₯) = (ββΞ£π β ((π§ supp 0) βͺ (π₯ supp 0))(((π§βπ) β (π₯βπ))β2))) |
118 | 117 | 3adant3r 1182 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π§π·π₯) = (ββΞ£π β ((π§ supp 0) βͺ (π₯ supp 0))(((π§βπ) β (π₯βπ))β2))) |
119 | 1, 28 | rrxmval 24772 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ π¦ β π) β (π§π·π¦) = (ββΞ£π β ((π§ supp 0) βͺ (π¦ supp 0))(((π§βπ) β (π¦βπ))β2))) |
120 | 119 | 3adant3l 1181 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π§π·π¦) = (ββΞ£π β ((π§ supp 0) βͺ (π¦ supp 0))(((π§βπ) β (π¦βπ))β2))) |
121 | 118, 120 | oveq12d 7376 |
. . . . . . . . 9
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β ((π§π·π₯) + (π§π·π¦)) = ((ββΞ£π β ((π§ supp 0) βͺ (π₯ supp 0))(((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β ((π§ supp 0) βͺ (π¦ supp 0))(((π§βπ) β (π¦βπ))β2)))) |
122 | | ssun2 4134 |
. . . . . . . . . . . . . 14
β’ (π§ supp 0) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0)) |
123 | 122 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π§ supp 0) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) |
124 | 52, 110 | sstri 3954 |
. . . . . . . . . . . . . 14
β’ (π₯ supp 0) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0)) |
125 | 124 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π₯ supp 0) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) |
126 | 123, 125 | unssd 4147 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β ((π§ supp 0) βͺ (π₯ supp 0)) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) |
127 | 1, 28, 102, 66, 103, 109, 69, 126 | rrxmetlem 24774 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β Ξ£π β ((π§ supp 0) βͺ (π₯ supp 0))(((π§βπ) β (π₯βπ))β2) = Ξ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2)) |
128 | 127 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (ββΞ£π β ((π§ supp 0) βͺ (π₯ supp 0))(((π§βπ) β (π₯βπ))β2)) = (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2))) |
129 | 57, 110 | sstri 3954 |
. . . . . . . . . . . . . 14
β’ (π¦ supp 0) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0)) |
130 | 129 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (π¦ supp 0) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) |
131 | 123, 130 | unssd 4147 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β ((π§ supp 0) βͺ (π¦ supp 0)) β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))) |
132 | 1, 28, 102, 66, 104, 109, 69, 131 | rrxmetlem 24774 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β Ξ£π β ((π§ supp 0) βͺ (π¦ supp 0))(((π§βπ) β (π¦βπ))β2) = Ξ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2)) |
133 | 132 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β (ββΞ£π β ((π§ supp 0) βͺ (π¦ supp 0))(((π§βπ) β (π¦βπ))β2)) = (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2))) |
134 | 128, 133 | oveq12d 7376 |
. . . . . . . . 9
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β ((ββΞ£π β ((π§ supp 0) βͺ (π₯ supp 0))(((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β ((π§ supp 0) βͺ (π¦ supp 0))(((π§βπ) β (π¦βπ))β2))) = ((ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2)))) |
135 | 121, 134 | eqtrd 2777 |
. . . . . . . 8
β’ ((πΌ β π β§ π§ β π β§ (π₯ β π β§ π¦ β π)) β ((π§π·π₯) + (π§π·π¦)) = ((ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2)))) |
136 | 135 | 3expa 1119 |
. . . . . . 7
β’ (((πΌ β π β§ π§ β π) β§ (π₯ β π β§ π¦ β π)) β ((π§π·π₯) + (π§π·π¦)) = ((ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2)))) |
137 | 136 | an32s 651 |
. . . . . 6
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β ((π§π·π₯) + (π§π·π¦)) = ((ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π₯βπ))β2)) + (ββΞ£π β (((π₯ supp 0) βͺ (π¦ supp 0)) βͺ (π§ supp 0))(((π§βπ) β (π¦βπ))β2)))) |
138 | 100, 116,
137 | 3brtr4d 5138 |
. . . . 5
β’ (((πΌ β π β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) |
139 | 138 | ralrimiva 3144 |
. . . 4
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) |
140 | 64, 139 | jca 513 |
. . 3
β’ ((πΌ β π β§ (π₯ β π β§ π¦ β π)) β (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦)))) |
141 | 140 | ralrimivva 3198 |
. 2
β’ (πΌ β π β βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦)))) |
142 | | ovex 7391 |
. . . 4
β’ (β
βm πΌ)
β V |
143 | 1, 142 | rabex2 5292 |
. . 3
β’ π β V |
144 | | ismet 23679 |
. . 3
β’ (π β V β (π· β (Metβπ) β (π·:(π Γ π)βΆβ β§ βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦)))))) |
145 | 143, 144 | ax-mp 5 |
. 2
β’ (π· β (Metβπ) β (π·:(π Γ π)βΆβ β§ βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))))) |
146 | 31, 141, 145 | sylanbrc 584 |
1
β’ (πΌ β π β π· β (Metβπ)) |