Metamath Proof Explorer

Theorem mndpluscn

Description: A mapping that is both a homeomorphism and a monoid homomorphism preserves the "continuousness" of the operation. (Contributed by Thierry Arnoux, 25-Mar-2017)

Ref Expression
Hypotheses mndpluscn.f ⊢ 𝐹 ∈ ( 𝐽 Homeo 𝐾 )
mndpluscn.p ⊢ + : ( 𝐵 × 𝐵 ) ⟶ 𝐵
mndpluscn.t ⊢ ∗ : ( 𝐶 × 𝐶 ) ⟶ 𝐶
mndpluscn.j ⊢ 𝐽 ∈ ( TopOn ‘ 𝐵 )
mndpluscn.k ⊢ 𝐾 ∈ ( TopOn ‘ 𝐶 )
mndpluscn.h ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) )
mndpluscn.o ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
Assertion mndpluscn ∗ ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )

Proof

Step Hyp Ref Expression
1 mndpluscn.f ⊢ 𝐹 ∈ ( 𝐽 Homeo 𝐾 )
2 mndpluscn.p ⊢ + : ( 𝐵 × 𝐵 ) ⟶ 𝐵
3 mndpluscn.t ⊢ ∗ : ( 𝐶 × 𝐶 ) ⟶ 𝐶
4 mndpluscn.j ⊢ 𝐽 ∈ ( TopOn ‘ 𝐵 )
5 mndpluscn.k ⊢ 𝐾 ∈ ( TopOn ‘ 𝐶 )
6 mndpluscn.h ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) )
7 mndpluscn.o ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
8 ffn ⊢ ( ∗ : ( 𝐶 × 𝐶 ) ⟶ 𝐶 → ∗ Fn ( 𝐶 × 𝐶 ) )
9 fnov ⊢ ( ∗ Fn ( 𝐶 × 𝐶 ) ↔ ∗ = ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( 𝑎 ∗ 𝑏 ) ) )
10 9 biimpi ⊢ ( ∗ Fn ( 𝐶 × 𝐶 ) → ∗ = ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( 𝑎 ∗ 𝑏 ) ) )
11 3 8 10 mp2b ⊢ ∗ = ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( 𝑎 ∗ 𝑏 ) )
12 4 toponunii ⊢ 𝐵 = ∪ 𝐽
13 5 toponunii ⊢ 𝐶 = ∪ 𝐾
14 12 13 hmeof1o ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
15 1 14 ax-mp ⊢ 𝐹 : 𝐵 –1-1-onto→ 𝐶
16 f1ocnvdm ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑎 ∈ 𝐶 ) → ( ◡ 𝐹 ‘ 𝑎 ) ∈ 𝐵 )
17 15 16 mpan ⊢ ( 𝑎 ∈ 𝐶 → ( ◡ 𝐹 ‘ 𝑎 ) ∈ 𝐵 )
18 f1ocnvdm ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝐵 )
19 15 18 mpan ⊢ ( 𝑏 ∈ 𝐶 → ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝐵 )
20 17 19 anim12i ⊢ ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( ( ◡ 𝐹 ‘ 𝑎 ) ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝐵 ) )
21 6 rgen2 ⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) )
22 fvoveq1 ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑎 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + 𝑦 ) ) )
23 fveq2 ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑎 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) )
24 23 oveq1d ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑎 ) → ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ∗ ( 𝐹 ‘ 𝑦 ) ) )
25 22 24 eqeq12d ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑎 ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + 𝑦 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) )
26 oveq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑏 ) → ( ( ◡ 𝐹 ‘ 𝑎 ) + 𝑦 ) = ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) )
27 26 fveq2d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + 𝑦 ) ) = ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
28 fveq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) )
29 28 oveq2d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ∗ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ∗ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
30 27 29 eqeq12d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + 𝑦 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ∗ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ∗ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) ) )
31 25 30 rspc2va ⊢ ( ( ( ( ◡ 𝐹 ‘ 𝑎 ) ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∗ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ∗ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
32 20 21 31 sylancl ⊢ ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ∗ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
33 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑎 ∈ 𝐶 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) = 𝑎 )
34 15 33 mpan ⊢ ( 𝑎 ∈ 𝐶 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) = 𝑎 )
35 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = 𝑏 )
36 15 35 mpan ⊢ ( 𝑏 ∈ 𝐶 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = 𝑏 )
37 34 36 oveqan12d ⊢ ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) ∗ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝑎 ∗ 𝑏 ) )
38 32 37 eqtr2d ⊢ ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( 𝑎 ∗ 𝑏 ) = ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
39 38 mpoeq3ia ⊢ ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( 𝑎 ∗ 𝑏 ) ) = ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
40 11 39 eqtri ⊢ ∗ = ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
41 5 a1i ⊢ ( ⊤ → 𝐾 ∈ ( TopOn ‘ 𝐶 ) )
42 41 41 cnmpt1st ⊢ ( ⊤ → ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ 𝑎 ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
43 hmeocnvcn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
44 1 43 mp1i ⊢ ( ⊤ → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
45 41 41 42 44 cnmpt21f ⊢ ( ⊤ → ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( ◡ 𝐹 ‘ 𝑎 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐽 ) )
46 41 41 cnmpt2nd ⊢ ( ⊤ → ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ 𝑏 ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
47 41 41 46 44 cnmpt21f ⊢ ( ⊤ → ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( ◡ 𝐹 ‘ 𝑏 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐽 ) )
48 7 a1i ⊢ ( ⊤ → + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
49 41 41 45 47 48 cnmpt22f ⊢ ( ⊤ → ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐽 ) )
50 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
51 1 50 mp1i ⊢ ( ⊤ → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
52 41 41 49 51 cnmpt21f ⊢ ( ⊤ → ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
53 52 mptru ⊢ ( 𝑎 ∈ 𝐶 , 𝑏 ∈ 𝐶 ↦ ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑎 ) + ( ◡ 𝐹 ‘ 𝑏 ) ) ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
54 40 53 eqeltri ⊢ ∗ ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )