Step |
Hyp |
Ref |
Expression |
1 |
|
xmetresbl.1 |
β’ π΅ = ( π ( ball β π· ) π
) |
2 |
|
simp1 |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β π· β ( βMet β π ) ) |
3 |
|
blssm |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π ( ball β π· ) π
) β π ) |
4 |
1 3
|
eqsstrid |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β π΅ β π ) |
5 |
|
xmetres2 |
β’ ( ( π· β ( βMet β π ) β§ π΅ β π ) β ( π· βΎ ( π΅ Γ π΅ ) ) β ( βMet β π΅ ) ) |
6 |
2 4 5
|
syl2anc |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π· βΎ ( π΅ Γ π΅ ) ) β ( βMet β π΅ ) ) |
7 |
|
xmetf |
β’ ( π· β ( βMet β π ) β π· : ( π Γ π ) βΆ β* ) |
8 |
2 7
|
syl |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β π· : ( π Γ π ) βΆ β* ) |
9 |
|
xpss12 |
β’ ( ( π΅ β π β§ π΅ β π ) β ( π΅ Γ π΅ ) β ( π Γ π ) ) |
10 |
4 4 9
|
syl2anc |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π΅ Γ π΅ ) β ( π Γ π ) ) |
11 |
8 10
|
fssresd |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π· βΎ ( π΅ Γ π΅ ) ) : ( π΅ Γ π΅ ) βΆ β* ) |
12 |
11
|
ffnd |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π· βΎ ( π΅ Γ π΅ ) ) Fn ( π΅ Γ π΅ ) ) |
13 |
|
ovres |
β’ ( ( π₯ β π΅ β§ π¦ β π΅ ) β ( π₯ ( π· βΎ ( π΅ Γ π΅ ) ) π¦ ) = ( π₯ π· π¦ ) ) |
14 |
13
|
adantl |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β ( π₯ ( π· βΎ ( π΅ Γ π΅ ) ) π¦ ) = ( π₯ π· π¦ ) ) |
15 |
|
simpl1 |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β π· β ( βMet β π ) ) |
16 |
|
eqid |
β’ ( β‘ π· β β ) = ( β‘ π· β β ) |
17 |
16
|
xmeter |
β’ ( π· β ( βMet β π ) β ( β‘ π· β β ) Er π ) |
18 |
15 17
|
syl |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β ( β‘ π· β β ) Er π ) |
19 |
16
|
blssec |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π ( ball β π· ) π
) β [ π ] ( β‘ π· β β ) ) |
20 |
1 19
|
eqsstrid |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β π΅ β [ π ] ( β‘ π· β β ) ) |
21 |
20
|
sselda |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π₯ β π΅ ) β π₯ β [ π ] ( β‘ π· β β ) ) |
22 |
21
|
adantrr |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β π₯ β [ π ] ( β‘ π· β β ) ) |
23 |
|
simpl2 |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β π β π ) |
24 |
|
elecg |
β’ ( ( π₯ β [ π ] ( β‘ π· β β ) β§ π β π ) β ( π₯ β [ π ] ( β‘ π· β β ) β π ( β‘ π· β β ) π₯ ) ) |
25 |
22 23 24
|
syl2anc |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β ( π₯ β [ π ] ( β‘ π· β β ) β π ( β‘ π· β β ) π₯ ) ) |
26 |
22 25
|
mpbid |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β π ( β‘ π· β β ) π₯ ) |
27 |
20
|
sselda |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β π΅ ) β π¦ β [ π ] ( β‘ π· β β ) ) |
28 |
27
|
adantrl |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β π¦ β [ π ] ( β‘ π· β β ) ) |
29 |
|
elecg |
β’ ( ( π¦ β [ π ] ( β‘ π· β β ) β§ π β π ) β ( π¦ β [ π ] ( β‘ π· β β ) β π ( β‘ π· β β ) π¦ ) ) |
30 |
28 23 29
|
syl2anc |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β ( π¦ β [ π ] ( β‘ π· β β ) β π ( β‘ π· β β ) π¦ ) ) |
31 |
28 30
|
mpbid |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β π ( β‘ π· β β ) π¦ ) |
32 |
18 26 31
|
ertr3d |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β π₯ ( β‘ π· β β ) π¦ ) |
33 |
16
|
xmeterval |
β’ ( π· β ( βMet β π ) β ( π₯ ( β‘ π· β β ) π¦ β ( π₯ β π β§ π¦ β π β§ ( π₯ π· π¦ ) β β ) ) ) |
34 |
15 33
|
syl |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β ( π₯ ( β‘ π· β β ) π¦ β ( π₯ β π β§ π¦ β π β§ ( π₯ π· π¦ ) β β ) ) ) |
35 |
32 34
|
mpbid |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β ( π₯ β π β§ π¦ β π β§ ( π₯ π· π¦ ) β β ) ) |
36 |
35
|
simp3d |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β ( π₯ π· π¦ ) β β ) |
37 |
14 36
|
eqeltrd |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ ( π₯ β π΅ β§ π¦ β π΅ ) ) β ( π₯ ( π· βΎ ( π΅ Γ π΅ ) ) π¦ ) β β ) |
38 |
37
|
ralrimivva |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β β π₯ β π΅ β π¦ β π΅ ( π₯ ( π· βΎ ( π΅ Γ π΅ ) ) π¦ ) β β ) |
39 |
|
ffnov |
β’ ( ( π· βΎ ( π΅ Γ π΅ ) ) : ( π΅ Γ π΅ ) βΆ β β ( ( π· βΎ ( π΅ Γ π΅ ) ) Fn ( π΅ Γ π΅ ) β§ β π₯ β π΅ β π¦ β π΅ ( π₯ ( π· βΎ ( π΅ Γ π΅ ) ) π¦ ) β β ) ) |
40 |
12 38 39
|
sylanbrc |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π· βΎ ( π΅ Γ π΅ ) ) : ( π΅ Γ π΅ ) βΆ β ) |
41 |
|
ismet2 |
β’ ( ( π· βΎ ( π΅ Γ π΅ ) ) β ( Met β π΅ ) β ( ( π· βΎ ( π΅ Γ π΅ ) ) β ( βMet β π΅ ) β§ ( π· βΎ ( π΅ Γ π΅ ) ) : ( π΅ Γ π΅ ) βΆ β ) ) |
42 |
6 40 41
|
sylanbrc |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π· βΎ ( π΅ Γ π΅ ) ) β ( Met β π΅ ) ) |