Step | Hyp | Ref
| Expression |
1 | | mhmhmeotmd.m |
. . 3
⊢ 𝐹 ∈ (𝑆 MndHom 𝑇) |
2 | | mhmrcl2 18222 |
. . 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 18221 |
. . . . 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 18191 |
. . . 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 18191 |
. . . 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 22978 |
. . . 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 21831 |
. . . 4
⊢ (𝑇 ∈ TopSp ↔
(TopOpen‘𝑇) ∈
(TopOn‘(Base‘𝑇))) |
22 | 4, 21 | mpbi 233 |
. . 3
⊢
(TopOpen‘𝑇)
∈ (TopOn‘(Base‘𝑇)) |
23 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑆) = (+g‘𝑆) |
24 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑇) = (+g‘𝑇) |
25 | 8, 23, 24 | mhmlin 18225 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
26 | 1, 25 | mp3an1 1450 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
27 | 8, 23, 9 | plusfval 18121 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(+𝑓‘𝑆)𝑦) = (𝑥(+g‘𝑆)𝑦)) |
28 | 27 | fveq2d 6721 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+𝑓‘𝑆)𝑦)) = (𝐹‘(𝑥(+g‘𝑆)𝑦))) |
29 | 8, 12 | mhmf 18223 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
30 | 1, 29 | ax-mp 5 |
. . . . . 6
⊢ 𝐹:(Base‘𝑆)⟶(Base‘𝑇) |
31 | 30 | ffvelrni 6903 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝑆) → (𝐹‘𝑥) ∈ (Base‘𝑇)) |
32 | 30 | ffvelrni 6903 |
. . . . 5
⊢ (𝑦 ∈ (Base‘𝑆) → (𝐹‘𝑦) ∈ (Base‘𝑇)) |
33 | 12, 24, 13 | plusfval 18121 |
. . . . 5
⊢ (((𝐹‘𝑥) ∈ (Base‘𝑇) ∧ (𝐹‘𝑦) ∈ (Base‘𝑇)) → ((𝐹‘𝑥)(+𝑓‘𝑇)(𝐹‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
34 | 31, 32, 33 | syl2an 599 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑥)(+𝑓‘𝑇)(𝐹‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
35 | 26, 28, 34 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+𝑓‘𝑆)𝑦)) = ((𝐹‘𝑥)(+𝑓‘𝑇)(𝐹‘𝑦))) |
36 | 17, 9 | tmdcn 22980 |
. . . 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 31590 |
. 2
⊢
(+𝑓‘𝑇) ∈ (((TopOpen‘𝑇) ×t (TopOpen‘𝑇)) Cn (TopOpen‘𝑇)) |
39 | 13, 20 | istmd 22971 |
. 2
⊢ (𝑇 ∈ TopMnd ↔ (𝑇 ∈ Mnd ∧ 𝑇 ∈ TopSp ∧
(+𝑓‘𝑇) ∈ (((TopOpen‘𝑇) ×t (TopOpen‘𝑇)) Cn (TopOpen‘𝑇)))) |
40 | 3, 4, 38, 39 | mpbir3an 1343 |
1
⊢ 𝑇 ∈ TopMnd |