Step | Hyp | Ref
| Expression |
1 | | mndpluscn.t |
. . . 4
β’ β
:(πΆ Γ πΆ)βΆπΆ |
2 | | ffn 6672 |
. . . 4
β’ ( β
:(πΆ Γ πΆ)βΆπΆ β β Fn (πΆ Γ πΆ)) |
3 | | fnov 7491 |
. . . . 5
β’ ( β Fn
(πΆ Γ πΆ) β β = (π β πΆ, π β πΆ β¦ (π β π))) |
4 | 3 | biimpi 215 |
. . . 4
β’ ( β Fn
(πΆ Γ πΆ) β β = (π β πΆ, π β πΆ β¦ (π β π))) |
5 | 1, 2, 4 | mp2b 10 |
. . 3
β’ β =
(π β πΆ, π β πΆ β¦ (π β π)) |
6 | | mndpluscn.f |
. . . . . . . . 9
β’ πΉ β (π½HomeoπΎ) |
7 | | mndpluscn.j |
. . . . . . . . . . 11
β’ π½ β (TopOnβπ΅) |
8 | 7 | toponunii 22288 |
. . . . . . . . . 10
β’ π΅ = βͺ
π½ |
9 | | mndpluscn.k |
. . . . . . . . . . 11
β’ πΎ β (TopOnβπΆ) |
10 | 9 | toponunii 22288 |
. . . . . . . . . 10
β’ πΆ = βͺ
πΎ |
11 | 8, 10 | hmeof1o 23138 |
. . . . . . . . 9
β’ (πΉ β (π½HomeoπΎ) β πΉ:π΅β1-1-ontoβπΆ) |
12 | 6, 11 | ax-mp 5 |
. . . . . . . 8
β’ πΉ:π΅β1-1-ontoβπΆ |
13 | | f1ocnvdm 7235 |
. . . . . . . 8
β’ ((πΉ:π΅β1-1-ontoβπΆ β§ π β πΆ) β (β‘πΉβπ) β π΅) |
14 | 12, 13 | mpan 689 |
. . . . . . 7
β’ (π β πΆ β (β‘πΉβπ) β π΅) |
15 | | f1ocnvdm 7235 |
. . . . . . . 8
β’ ((πΉ:π΅β1-1-ontoβπΆ β§ π β πΆ) β (β‘πΉβπ) β π΅) |
16 | 12, 15 | mpan 689 |
. . . . . . 7
β’ (π β πΆ β (β‘πΉβπ) β π΅) |
17 | 14, 16 | anim12i 614 |
. . . . . 6
β’ ((π β πΆ β§ π β πΆ) β ((β‘πΉβπ) β π΅ β§ (β‘πΉβπ) β π΅)) |
18 | | mndpluscn.h |
. . . . . . 7
β’ ((π₯ β π΅ β§ π¦ β π΅) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) β (πΉβπ¦))) |
19 | 18 | rgen2 3191 |
. . . . . 6
β’
βπ₯ β
π΅ βπ¦ β π΅ (πΉβ(π₯ + π¦)) = ((πΉβπ₯) β (πΉβπ¦)) |
20 | | fvoveq1 7384 |
. . . . . . . 8
β’ (π₯ = (β‘πΉβπ) β (πΉβ(π₯ + π¦)) = (πΉβ((β‘πΉβπ) + π¦))) |
21 | | fveq2 6846 |
. . . . . . . . 9
β’ (π₯ = (β‘πΉβπ) β (πΉβπ₯) = (πΉβ(β‘πΉβπ))) |
22 | 21 | oveq1d 7376 |
. . . . . . . 8
β’ (π₯ = (β‘πΉβπ) β ((πΉβπ₯) β (πΉβπ¦)) = ((πΉβ(β‘πΉβπ)) β (πΉβπ¦))) |
23 | 20, 22 | eqeq12d 2749 |
. . . . . . 7
β’ (π₯ = (β‘πΉβπ) β ((πΉβ(π₯ + π¦)) = ((πΉβπ₯) β (πΉβπ¦)) β (πΉβ((β‘πΉβπ) + π¦)) = ((πΉβ(β‘πΉβπ)) β (πΉβπ¦)))) |
24 | | oveq2 7369 |
. . . . . . . . 9
β’ (π¦ = (β‘πΉβπ) β ((β‘πΉβπ) + π¦) = ((β‘πΉβπ) + (β‘πΉβπ))) |
25 | 24 | fveq2d 6850 |
. . . . . . . 8
β’ (π¦ = (β‘πΉβπ) β (πΉβ((β‘πΉβπ) + π¦)) = (πΉβ((β‘πΉβπ) + (β‘πΉβπ)))) |
26 | | fveq2 6846 |
. . . . . . . . 9
β’ (π¦ = (β‘πΉβπ) β (πΉβπ¦) = (πΉβ(β‘πΉβπ))) |
27 | 26 | oveq2d 7377 |
. . . . . . . 8
β’ (π¦ = (β‘πΉβπ) β ((πΉβ(β‘πΉβπ)) β (πΉβπ¦)) = ((πΉβ(β‘πΉβπ)) β (πΉβ(β‘πΉβπ)))) |
28 | 25, 27 | eqeq12d 2749 |
. . . . . . 7
β’ (π¦ = (β‘πΉβπ) β ((πΉβ((β‘πΉβπ) + π¦)) = ((πΉβ(β‘πΉβπ)) β (πΉβπ¦)) β (πΉβ((β‘πΉβπ) + (β‘πΉβπ))) = ((πΉβ(β‘πΉβπ)) β (πΉβ(β‘πΉβπ))))) |
29 | 23, 28 | rspc2va 3593 |
. . . . . 6
β’ ((((β‘πΉβπ) β π΅ β§ (β‘πΉβπ) β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (πΉβ(π₯ + π¦)) = ((πΉβπ₯) β (πΉβπ¦))) β (πΉβ((β‘πΉβπ) + (β‘πΉβπ))) = ((πΉβ(β‘πΉβπ)) β (πΉβ(β‘πΉβπ)))) |
30 | 17, 19, 29 | sylancl 587 |
. . . . 5
β’ ((π β πΆ β§ π β πΆ) β (πΉβ((β‘πΉβπ) + (β‘πΉβπ))) = ((πΉβ(β‘πΉβπ)) β (πΉβ(β‘πΉβπ)))) |
31 | | f1ocnvfv2 7227 |
. . . . . . 7
β’ ((πΉ:π΅β1-1-ontoβπΆ β§ π β πΆ) β (πΉβ(β‘πΉβπ)) = π) |
32 | 12, 31 | mpan 689 |
. . . . . 6
β’ (π β πΆ β (πΉβ(β‘πΉβπ)) = π) |
33 | | f1ocnvfv2 7227 |
. . . . . . 7
β’ ((πΉ:π΅β1-1-ontoβπΆ β§ π β πΆ) β (πΉβ(β‘πΉβπ)) = π) |
34 | 12, 33 | mpan 689 |
. . . . . 6
β’ (π β πΆ β (πΉβ(β‘πΉβπ)) = π) |
35 | 32, 34 | oveqan12d 7380 |
. . . . 5
β’ ((π β πΆ β§ π β πΆ) β ((πΉβ(β‘πΉβπ)) β (πΉβ(β‘πΉβπ))) = (π β π)) |
36 | 30, 35 | eqtr2d 2774 |
. . . 4
β’ ((π β πΆ β§ π β πΆ) β (π β π) = (πΉβ((β‘πΉβπ) + (β‘πΉβπ)))) |
37 | 36 | mpoeq3ia 7439 |
. . 3
β’ (π β πΆ, π β πΆ β¦ (π β π)) = (π β πΆ, π β πΆ β¦ (πΉβ((β‘πΉβπ) + (β‘πΉβπ)))) |
38 | 5, 37 | eqtri 2761 |
. 2
β’ β =
(π β πΆ, π β πΆ β¦ (πΉβ((β‘πΉβπ) + (β‘πΉβπ)))) |
39 | 9 | a1i 11 |
. . . 4
β’ (β€
β πΎ β
(TopOnβπΆ)) |
40 | 39, 39 | cnmpt1st 23042 |
. . . . . 6
β’ (β€
β (π β πΆ, π β πΆ β¦ π) β ((πΎ Γt πΎ) Cn πΎ)) |
41 | | hmeocnvcn 23135 |
. . . . . . 7
β’ (πΉ β (π½HomeoπΎ) β β‘πΉ β (πΎ Cn π½)) |
42 | 6, 41 | mp1i 13 |
. . . . . 6
β’ (β€
β β‘πΉ β (πΎ Cn π½)) |
43 | 39, 39, 40, 42 | cnmpt21f 23046 |
. . . . 5
β’ (β€
β (π β πΆ, π β πΆ β¦ (β‘πΉβπ)) β ((πΎ Γt πΎ) Cn π½)) |
44 | 39, 39 | cnmpt2nd 23043 |
. . . . . 6
β’ (β€
β (π β πΆ, π β πΆ β¦ π) β ((πΎ Γt πΎ) Cn πΎ)) |
45 | 39, 39, 44, 42 | cnmpt21f 23046 |
. . . . 5
β’ (β€
β (π β πΆ, π β πΆ β¦ (β‘πΉβπ)) β ((πΎ Γt πΎ) Cn π½)) |
46 | | mndpluscn.o |
. . . . . 6
β’ + β
((π½ Γt
π½) Cn π½) |
47 | 46 | a1i 11 |
. . . . 5
β’ (β€
β +
β ((π½
Γt π½) Cn
π½)) |
48 | 39, 39, 43, 45, 47 | cnmpt22f 23049 |
. . . 4
β’ (β€
β (π β πΆ, π β πΆ β¦ ((β‘πΉβπ) + (β‘πΉβπ))) β ((πΎ Γt πΎ) Cn π½)) |
49 | | hmeocn 23134 |
. . . . 5
β’ (πΉ β (π½HomeoπΎ) β πΉ β (π½ Cn πΎ)) |
50 | 6, 49 | mp1i 13 |
. . . 4
β’ (β€
β πΉ β (π½ Cn πΎ)) |
51 | 39, 39, 48, 50 | cnmpt21f 23046 |
. . 3
β’ (β€
β (π β πΆ, π β πΆ β¦ (πΉβ((β‘πΉβπ) + (β‘πΉβπ)))) β ((πΎ Γt πΎ) Cn πΎ)) |
52 | 51 | mptru 1549 |
. 2
β’ (π β πΆ, π β πΆ β¦ (πΉβ((β‘πΉβπ) + (β‘πΉβπ)))) β ((πΎ Γt πΎ) Cn πΎ) |
53 | 38, 52 | eqeltri 2830 |
1
β’ β β
((πΎ Γt
πΎ) Cn πΎ) |