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 𝐾 )