Step | Hyp | Ref
| Expression |
1 | | sneq 4600 |
. . . . . . . 8
β’ (π¦ = π΄ β {π¦} = {π΄}) |
2 | 1 | xpeq1d 5666 |
. . . . . . 7
β’ (π¦ = π΄ β ({π¦} Γ {π₯}) = ({π΄} Γ {π₯})) |
3 | 2 | mpteq2dv 5211 |
. . . . . 6
β’ (π¦ = π΄ β (π₯ β β β¦ ({π¦} Γ {π₯})) = (π₯ β β β¦ ({π΄} Γ {π₯}))) |
4 | | ismrer1.2 |
. . . . . 6
β’ πΉ = (π₯ β β β¦ ({π΄} Γ {π₯})) |
5 | 3, 4 | eqtr4di 2791 |
. . . . 5
β’ (π¦ = π΄ β (π₯ β β β¦ ({π¦} Γ {π₯})) = πΉ) |
6 | 5 | f1oeq1d 6783 |
. . . 4
β’ (π¦ = π΄ β ((π₯ β β β¦ ({π¦} Γ {π₯})):ββ1-1-ontoβ(β βm {π¦}) β πΉ:ββ1-1-ontoβ(β βm {π¦}))) |
7 | 1 | oveq2d 7377 |
. . . . 5
β’ (π¦ = π΄ β (β βm {π¦}) = (β βm
{π΄})) |
8 | | f1oeq3 6778 |
. . . . 5
β’ ((β
βm {π¦}) =
(β βm {π΄}) β (πΉ:ββ1-1-ontoβ(β βm {π¦}) β πΉ:ββ1-1-ontoβ(β βm {π΄}))) |
9 | 7, 8 | syl 17 |
. . . 4
β’ (π¦ = π΄ β (πΉ:ββ1-1-ontoβ(β βm {π¦}) β πΉ:ββ1-1-ontoβ(β βm {π΄}))) |
10 | 6, 9 | bitrd 279 |
. . 3
β’ (π¦ = π΄ β ((π₯ β β β¦ ({π¦} Γ {π₯})):ββ1-1-ontoβ(β βm {π¦}) β πΉ:ββ1-1-ontoβ(β βm {π΄}))) |
11 | | eqid 2733 |
. . . 4
β’ {π¦} = {π¦} |
12 | | reex 11150 |
. . . 4
β’ β
β V |
13 | | vex 3451 |
. . . 4
β’ π¦ β V |
14 | | eqid 2733 |
. . . 4
β’ (π₯ β β β¦ ({π¦} Γ {π₯})) = (π₯ β β β¦ ({π¦} Γ {π₯})) |
15 | 11, 12, 13, 14 | mapsnf1o3 8839 |
. . 3
β’ (π₯ β β β¦ ({π¦} Γ {π₯})):ββ1-1-ontoβ(β βm {π¦}) |
16 | 10, 15 | vtoclg 3527 |
. 2
β’ (π΄ β π β πΉ:ββ1-1-ontoβ(β βm {π΄})) |
17 | | sneq 4600 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β {π₯} = {π¦}) |
18 | 17 | xpeq2d 5667 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β ({π΄} Γ {π₯}) = ({π΄} Γ {π¦})) |
19 | | snex 5392 |
. . . . . . . . . . . . . . . . 17
β’ {π΄} β V |
20 | | snex 5392 |
. . . . . . . . . . . . . . . . 17
β’ {π₯} β V |
21 | 19, 20 | xpex 7691 |
. . . . . . . . . . . . . . . 16
β’ ({π΄} Γ {π₯}) β V |
22 | 18, 4, 21 | fvmpt3i 6957 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β (πΉβπ¦) = ({π΄} Γ {π¦})) |
23 | 22 | fveq1d 6848 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β ((πΉβπ¦)βπ΄) = (({π΄} Γ {π¦})βπ΄)) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π¦ β β β§ π§ β β) β ((πΉβπ¦)βπ΄) = (({π΄} Γ {π¦})βπ΄)) |
25 | | snidg 4624 |
. . . . . . . . . . . . . 14
β’ (π΄ β π β π΄ β {π΄}) |
26 | | fvconst2g 7155 |
. . . . . . . . . . . . . 14
β’ ((π¦ β V β§ π΄ β {π΄}) β (({π΄} Γ {π¦})βπ΄) = π¦) |
27 | 13, 25, 26 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π΄ β π β (({π΄} Γ {π¦})βπ΄) = π¦) |
28 | 24, 27 | sylan9eqr 2795 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β ((πΉβπ¦)βπ΄) = π¦) |
29 | | sneq 4600 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β {π₯} = {π§}) |
30 | 29 | xpeq2d 5667 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π§ β ({π΄} Γ {π₯}) = ({π΄} Γ {π§})) |
31 | 30, 4, 21 | fvmpt3i 6957 |
. . . . . . . . . . . . . . 15
β’ (π§ β β β (πΉβπ§) = ({π΄} Γ {π§})) |
32 | 31 | fveq1d 6848 |
. . . . . . . . . . . . . 14
β’ (π§ β β β ((πΉβπ§)βπ΄) = (({π΄} Γ {π§})βπ΄)) |
33 | 32 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π¦ β β β§ π§ β β) β ((πΉβπ§)βπ΄) = (({π΄} Γ {π§})βπ΄)) |
34 | | vex 3451 |
. . . . . . . . . . . . . 14
β’ π§ β V |
35 | | fvconst2g 7155 |
. . . . . . . . . . . . . 14
β’ ((π§ β V β§ π΄ β {π΄}) β (({π΄} Γ {π§})βπ΄) = π§) |
36 | 34, 25, 35 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π΄ β π β (({π΄} Γ {π§})βπ΄) = π§) |
37 | 33, 36 | sylan9eqr 2795 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β ((πΉβπ§)βπ΄) = π§) |
38 | 28, 37 | oveq12d 7379 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β (((πΉβπ¦)βπ΄) β ((πΉβπ§)βπ΄)) = (π¦ β π§)) |
39 | 38 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β ((((πΉβπ¦)βπ΄) β ((πΉβπ§)βπ΄))β2) = ((π¦ β π§)β2)) |
40 | | resubcl 11473 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ π§ β β) β (π¦ β π§) β β) |
41 | 40 | adantl 483 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β (π¦ β π§) β β) |
42 | | absresq 15196 |
. . . . . . . . . . 11
β’ ((π¦ β π§) β β β ((absβ(π¦ β π§))β2) = ((π¦ β π§)β2)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β ((absβ(π¦ β π§))β2) = ((π¦ β π§)β2)) |
44 | 39, 43 | eqtr4d 2776 |
. . . . . . . . 9
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β ((((πΉβπ¦)βπ΄) β ((πΉβπ§)βπ΄))β2) = ((absβ(π¦ β π§))β2)) |
45 | 41 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β (π¦ β π§) β β) |
46 | 45 | abscld 15330 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β (absβ(π¦ β π§)) β β) |
47 | 46 | recnd 11191 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β (absβ(π¦ β π§)) β β) |
48 | 47 | sqcld 14058 |
. . . . . . . . 9
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β ((absβ(π¦ β π§))β2) β β) |
49 | 44, 48 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β ((((πΉβπ¦)βπ΄) β ((πΉβπ§)βπ΄))β2) β β) |
50 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π΄ β ((πΉβπ¦)βπ) = ((πΉβπ¦)βπ΄)) |
51 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π΄ β ((πΉβπ§)βπ) = ((πΉβπ§)βπ΄)) |
52 | 50, 51 | oveq12d 7379 |
. . . . . . . . . 10
β’ (π = π΄ β (((πΉβπ¦)βπ) β ((πΉβπ§)βπ)) = (((πΉβπ¦)βπ΄) β ((πΉβπ§)βπ΄))) |
53 | 52 | oveq1d 7376 |
. . . . . . . . 9
β’ (π = π΄ β ((((πΉβπ¦)βπ) β ((πΉβπ§)βπ))β2) = ((((πΉβπ¦)βπ΄) β ((πΉβπ§)βπ΄))β2)) |
54 | 53 | sumsn 15639 |
. . . . . . . 8
β’ ((π΄ β π β§ ((((πΉβπ¦)βπ΄) β ((πΉβπ§)βπ΄))β2) β β) β
Ξ£π β {π΄} ((((πΉβπ¦)βπ) β ((πΉβπ§)βπ))β2) = ((((πΉβπ¦)βπ΄) β ((πΉβπ§)βπ΄))β2)) |
55 | 49, 54 | syldan 592 |
. . . . . . 7
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β Ξ£π β {π΄} ((((πΉβπ¦)βπ) β ((πΉβπ§)βπ))β2) = ((((πΉβπ¦)βπ΄) β ((πΉβπ§)βπ΄))β2)) |
56 | 55, 44 | eqtrd 2773 |
. . . . . 6
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β Ξ£π β {π΄} ((((πΉβπ¦)βπ) β ((πΉβπ§)βπ))β2) = ((absβ(π¦ β π§))β2)) |
57 | 56 | fveq2d 6850 |
. . . . 5
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β
(ββΞ£π
β {π΄} ((((πΉβπ¦)βπ) β ((πΉβπ§)βπ))β2)) =
(ββ((absβ(π¦ β π§))β2))) |
58 | 45 | absge0d 15338 |
. . . . . 6
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β 0 β€
(absβ(π¦ β π§))) |
59 | 46, 58 | sqrtsqd 15313 |
. . . . 5
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β
(ββ((absβ(π¦ β π§))β2)) = (absβ(π¦ β π§))) |
60 | 57, 59 | eqtrd 2773 |
. . . 4
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β
(ββΞ£π
β {π΄} ((((πΉβπ¦)βπ) β ((πΉβπ§)βπ))β2)) = (absβ(π¦ β π§))) |
61 | | f1of 6788 |
. . . . . . . 8
β’ (πΉ:ββ1-1-ontoβ(β βm {π΄}) β πΉ:ββΆ(β βm
{π΄})) |
62 | 16, 61 | syl 17 |
. . . . . . 7
β’ (π΄ β π β πΉ:ββΆ(β βm
{π΄})) |
63 | 62 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π΄ β π β§ π¦ β β) β (πΉβπ¦) β (β βm {π΄})) |
64 | 62 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π΄ β π β§ π§ β β) β (πΉβπ§) β (β βm {π΄})) |
65 | 63, 64 | anim12dan 620 |
. . . . 5
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β ((πΉβπ¦) β (β βm {π΄}) β§ (πΉβπ§) β (β βm {π΄}))) |
66 | | snfi 8994 |
. . . . . 6
β’ {π΄} β Fin |
67 | | eqid 2733 |
. . . . . . 7
β’ (β
βm {π΄}) =
(β βm {π΄}) |
68 | 67 | rrnmval 36337 |
. . . . . 6
β’ (({π΄} β Fin β§ (πΉβπ¦) β (β βm {π΄}) β§ (πΉβπ§) β (β βm {π΄})) β ((πΉβπ¦)(βnβ{π΄})(πΉβπ§)) = (ββΞ£π β {π΄} ((((πΉβπ¦)βπ) β ((πΉβπ§)βπ))β2))) |
69 | 66, 68 | mp3an1 1449 |
. . . . 5
β’ (((πΉβπ¦) β (β βm {π΄}) β§ (πΉβπ§) β (β βm {π΄})) β ((πΉβπ¦)(βnβ{π΄})(πΉβπ§)) = (ββΞ£π β {π΄} ((((πΉβπ¦)βπ) β ((πΉβπ§)βπ))β2))) |
70 | 65, 69 | syl 17 |
. . . 4
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β ((πΉβπ¦)(βnβ{π΄})(πΉβπ§)) = (ββΞ£π β {π΄} ((((πΉβπ¦)βπ) β ((πΉβπ§)βπ))β2))) |
71 | | ismrer1.1 |
. . . . . 6
β’ π
= ((abs β β )
βΎ (β Γ β)) |
72 | 71 | remetdval 24175 |
. . . . 5
β’ ((π¦ β β β§ π§ β β) β (π¦π
π§) = (absβ(π¦ β π§))) |
73 | 72 | adantl 483 |
. . . 4
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β (π¦π
π§) = (absβ(π¦ β π§))) |
74 | 60, 70, 73 | 3eqtr4rd 2784 |
. . 3
β’ ((π΄ β π β§ (π¦ β β β§ π§ β β)) β (π¦π
π§) = ((πΉβπ¦)(βnβ{π΄})(πΉβπ§))) |
75 | 74 | ralrimivva 3194 |
. 2
β’ (π΄ β π β βπ¦ β β βπ§ β β (π¦π
π§) = ((πΉβπ¦)(βnβ{π΄})(πΉβπ§))) |
76 | 71 | rexmet 24177 |
. . 3
β’ π
β
(βMetββ) |
77 | 67 | rrnmet 36338 |
. . . 4
β’ ({π΄} β Fin β
(βnβ{π΄}) β (Metβ(β
βm {π΄}))) |
78 | | metxmet 23710 |
. . . 4
β’
((βnβ{π΄}) β (Metβ(β
βm {π΄}))
β (βnβ{π΄}) β (βMetβ(β
βm {π΄}))) |
79 | 66, 77, 78 | mp2b 10 |
. . 3
β’
(βnβ{π΄}) β (βMetβ(β
βm {π΄})) |
80 | | isismty 36310 |
. . 3
β’ ((π
β
(βMetββ) β§ (βnβ{π΄}) β
(βMetβ(β βm {π΄}))) β (πΉ β (π
Ismty
(βnβ{π΄})) β (πΉ:ββ1-1-ontoβ(β βm {π΄}) β§ βπ¦ β β βπ§ β β (π¦π
π§) = ((πΉβπ¦)(βnβ{π΄})(πΉβπ§))))) |
81 | 76, 79, 80 | mp2an 691 |
. 2
β’ (πΉ β (π
Ismty
(βnβ{π΄})) β (πΉ:ββ1-1-ontoβ(β βm {π΄}) β§ βπ¦ β β βπ§ β β (π¦π
π§) = ((πΉβπ¦)(βnβ{π΄})(πΉβπ§)))) |
82 | 16, 75, 81 | sylanbrc 584 |
1
β’ (π΄ β π β πΉ β (π
Ismty
(βnβ{π΄}))) |