Step |
Hyp |
Ref |
Expression |
1 |
|
cncfcn.2 |
β’ π½ = ( TopOpen β βfld ) |
2 |
|
cncfcn.3 |
β’ πΎ = ( π½ βΎt π΄ ) |
3 |
|
cncfcn.4 |
β’ πΏ = ( π½ βΎt π΅ ) |
4 |
|
eqid |
β’ ( ( abs β β ) βΎ ( π΄ Γ π΄ ) ) = ( ( abs β β ) βΎ ( π΄ Γ π΄ ) ) |
5 |
|
eqid |
β’ ( ( abs β β ) βΎ ( π΅ Γ π΅ ) ) = ( ( abs β β ) βΎ ( π΅ Γ π΅ ) ) |
6 |
|
eqid |
β’ ( MetOpen β ( ( abs β β ) βΎ ( π΄ Γ π΄ ) ) ) = ( MetOpen β ( ( abs β β ) βΎ ( π΄ Γ π΄ ) ) ) |
7 |
|
eqid |
β’ ( MetOpen β ( ( abs β β ) βΎ ( π΅ Γ π΅ ) ) ) = ( MetOpen β ( ( abs β β ) βΎ ( π΅ Γ π΅ ) ) ) |
8 |
4 5 6 7
|
cncfmet |
β’ ( ( π΄ β β β§ π΅ β β ) β ( π΄ βcnβ π΅ ) = ( ( MetOpen β ( ( abs β β ) βΎ ( π΄ Γ π΄ ) ) ) Cn ( MetOpen β ( ( abs β β ) βΎ ( π΅ Γ π΅ ) ) ) ) ) |
9 |
|
cnxmet |
β’ ( abs β β ) β ( βMet β β ) |
10 |
|
simpl |
β’ ( ( π΄ β β β§ π΅ β β ) β π΄ β β ) |
11 |
1
|
cnfldtopn |
β’ π½ = ( MetOpen β ( abs β β ) ) |
12 |
4 11 6
|
metrest |
β’ ( ( ( abs β β ) β ( βMet β β ) β§ π΄ β β ) β ( π½ βΎt π΄ ) = ( MetOpen β ( ( abs β β ) βΎ ( π΄ Γ π΄ ) ) ) ) |
13 |
9 10 12
|
sylancr |
β’ ( ( π΄ β β β§ π΅ β β ) β ( π½ βΎt π΄ ) = ( MetOpen β ( ( abs β β ) βΎ ( π΄ Γ π΄ ) ) ) ) |
14 |
2 13
|
eqtrid |
β’ ( ( π΄ β β β§ π΅ β β ) β πΎ = ( MetOpen β ( ( abs β β ) βΎ ( π΄ Γ π΄ ) ) ) ) |
15 |
|
simpr |
β’ ( ( π΄ β β β§ π΅ β β ) β π΅ β β ) |
16 |
5 11 7
|
metrest |
β’ ( ( ( abs β β ) β ( βMet β β ) β§ π΅ β β ) β ( π½ βΎt π΅ ) = ( MetOpen β ( ( abs β β ) βΎ ( π΅ Γ π΅ ) ) ) ) |
17 |
9 15 16
|
sylancr |
β’ ( ( π΄ β β β§ π΅ β β ) β ( π½ βΎt π΅ ) = ( MetOpen β ( ( abs β β ) βΎ ( π΅ Γ π΅ ) ) ) ) |
18 |
3 17
|
eqtrid |
β’ ( ( π΄ β β β§ π΅ β β ) β πΏ = ( MetOpen β ( ( abs β β ) βΎ ( π΅ Γ π΅ ) ) ) ) |
19 |
14 18
|
oveq12d |
β’ ( ( π΄ β β β§ π΅ β β ) β ( πΎ Cn πΏ ) = ( ( MetOpen β ( ( abs β β ) βΎ ( π΄ Γ π΄ ) ) ) Cn ( MetOpen β ( ( abs β β ) βΎ ( π΅ Γ π΅ ) ) ) ) ) |
20 |
8 19
|
eqtr4d |
β’ ( ( π΄ β β β§ π΅ β β ) β ( π΄ βcnβ π΅ ) = ( πΎ Cn πΏ ) ) |