Step | Hyp | Ref
| Expression |
1 | | mhmhmeotmd.m |
. . 3
β’ πΉ β (π MndHom π) |
2 | | mhmrcl2 18566 |
. . 3
β’ (πΉ β (π MndHom π) β π β Mnd) |
3 | 1, 2 | ax-mp 5 |
. 2
β’ π β Mnd |
4 | | mhmhmeotmd.s |
. 2
β’ π β TopSp |
5 | | mhmhmeotmd.h |
. . 3
β’ πΉ β ((TopOpenβπ)Homeo(TopOpenβπ)) |
6 | | mhmrcl1 18565 |
. . . . 5
β’ (πΉ β (π MndHom π) β π β Mnd) |
7 | 1, 6 | ax-mp 5 |
. . . 4
β’ π β Mnd |
8 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
9 | | eqid 2737 |
. . . . 5
β’
(+πβπ) = (+πβπ) |
10 | 8, 9 | mndplusf 18534 |
. . . 4
β’ (π β Mnd β
(+πβπ):((Baseβπ) Γ (Baseβπ))βΆ(Baseβπ)) |
11 | 7, 10 | ax-mp 5 |
. . 3
β’
(+πβπ):((Baseβπ) Γ (Baseβπ))βΆ(Baseβπ) |
12 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
13 | | eqid 2737 |
. . . . 5
β’
(+πβπ) = (+πβπ) |
14 | 12, 13 | mndplusf 18534 |
. . . 4
β’ (π β Mnd β
(+πβπ):((Baseβπ) Γ (Baseβπ))βΆ(Baseβπ)) |
15 | 3, 14 | ax-mp 5 |
. . 3
β’
(+πβπ):((Baseβπ) Γ (Baseβπ))βΆ(Baseβπ) |
16 | | mhmhmeotmd.t |
. . . 4
β’ π β TopMnd |
17 | | eqid 2737 |
. . . . 5
β’
(TopOpenβπ) =
(TopOpenβπ) |
18 | 17, 8 | tmdtopon 23384 |
. . . 4
β’ (π β TopMnd β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
19 | 16, 18 | ax-mp 5 |
. . 3
β’
(TopOpenβπ)
β (TopOnβ(Baseβπ)) |
20 | | eqid 2737 |
. . . . 5
β’
(TopOpenβπ) =
(TopOpenβπ) |
21 | 12, 20 | istps 22235 |
. . . 4
β’ (π β TopSp β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
22 | 4, 21 | mpbi 229 |
. . 3
β’
(TopOpenβπ)
β (TopOnβ(Baseβπ)) |
23 | | eqid 2737 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
24 | | eqid 2737 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
25 | 8, 23, 24 | mhmlin 18569 |
. . . . 5
β’ ((πΉ β (π MndHom π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
26 | 1, 25 | mp3an1 1448 |
. . . 4
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (πΉβ(π₯(+gβπ)π¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
27 | 8, 23, 9 | plusfval 18464 |
. . . . 5
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(+πβπ)π¦) = (π₯(+gβπ)π¦)) |
28 | 27 | fveq2d 6843 |
. . . 4
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (πΉβ(π₯(+πβπ)π¦)) = (πΉβ(π₯(+gβπ)π¦))) |
29 | 8, 12 | mhmf 18567 |
. . . . . . 7
β’ (πΉ β (π MndHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
30 | 1, 29 | ax-mp 5 |
. . . . . 6
β’ πΉ:(Baseβπ)βΆ(Baseβπ) |
31 | 30 | ffvelcdmi 7030 |
. . . . 5
β’ (π₯ β (Baseβπ) β (πΉβπ₯) β (Baseβπ)) |
32 | 30 | ffvelcdmi 7030 |
. . . . 5
β’ (π¦ β (Baseβπ) β (πΉβπ¦) β (Baseβπ)) |
33 | 12, 24, 13 | plusfval 18464 |
. . . . 5
β’ (((πΉβπ₯) β (Baseβπ) β§ (πΉβπ¦) β (Baseβπ)) β ((πΉβπ₯)(+πβπ)(πΉβπ¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
34 | 31, 32, 33 | syl2an 596 |
. . . 4
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β ((πΉβπ₯)(+πβπ)(πΉβπ¦)) = ((πΉβπ₯)(+gβπ)(πΉβπ¦))) |
35 | 26, 28, 34 | 3eqtr4d 2787 |
. . 3
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (πΉβ(π₯(+πβπ)π¦)) = ((πΉβπ₯)(+πβπ)(πΉβπ¦))) |
36 | 17, 9 | tmdcn 23386 |
. . . 4
β’ (π β TopMnd β
(+πβπ) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβπ))) |
37 | 16, 36 | ax-mp 5 |
. . 3
β’
(+πβπ) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβπ)) |
38 | 5, 11, 15, 19, 22, 35, 37 | mndpluscn 32319 |
. 2
β’
(+πβπ) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβπ)) |
39 | 13, 20 | istmd 23377 |
. 2
β’ (π β TopMnd β (π β Mnd β§ π β TopSp β§
(+πβπ) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβπ)))) |
40 | 3, 4, 38, 39 | mpbir3an 1341 |
1
β’ π β TopMnd |