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 
|- F e. ( J Homeo K )
mndpluscn.p 
|- .+ : ( B X. B ) --> B
mndpluscn.t 
|- .* : ( C X. C ) --> C
mndpluscn.j 
|- J e. ( TopOn ` B )
mndpluscn.k 
|- K e. ( TopOn ` C )
mndpluscn.h 
|- ( ( x e. B /\ y e. B ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .* ( F ` y ) ) )
mndpluscn.o 
|- .+ e. ( ( J tX J ) Cn J )
Assertion mndpluscn 
|- .* e. ( ( K tX K ) Cn K )

Proof

Step Hyp Ref Expression
1 mndpluscn.f 
 |-  F e. ( J Homeo K )
2 mndpluscn.p 
 |-  .+ : ( B X. B ) --> B
3 mndpluscn.t 
 |-  .* : ( C X. C ) --> C
4 mndpluscn.j 
 |-  J e. ( TopOn ` B )
5 mndpluscn.k 
 |-  K e. ( TopOn ` C )
6 mndpluscn.h 
 |-  ( ( x e. B /\ y e. B ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .* ( F ` y ) ) )
7 mndpluscn.o 
 |-  .+ e. ( ( J tX J ) Cn J )
8 ffn 
 |-  ( .* : ( C X. C ) --> C -> .* Fn ( C X. C ) )
9 fnov 
 |-  ( .* Fn ( C X. C ) <-> .* = ( a e. C , b e. C |-> ( a .* b ) ) )
10 9 biimpi 
 |-  ( .* Fn ( C X. C ) -> .* = ( a e. C , b e. C |-> ( a .* b ) ) )
11 3 8 10 mp2b 
 |-  .* = ( a e. C , b e. C |-> ( a .* b ) )
12 4 toponunii 
 |-  B = U. J
13 5 toponunii 
 |-  C = U. K
14 12 13 hmeof1o 
 |-  ( F e. ( J Homeo K ) -> F : B -1-1-onto-> C )
15 1 14 ax-mp 
 |-  F : B -1-1-onto-> C
16 f1ocnvdm 
 |-  ( ( F : B -1-1-onto-> C /\ a e. C ) -> ( `' F ` a ) e. B )
17 15 16 mpan 
 |-  ( a e. C -> ( `' F ` a ) e. B )
18 f1ocnvdm 
 |-  ( ( F : B -1-1-onto-> C /\ b e. C ) -> ( `' F ` b ) e. B )
19 15 18 mpan 
 |-  ( b e. C -> ( `' F ` b ) e. B )
20 17 19 anim12i 
 |-  ( ( a e. C /\ b e. C ) -> ( ( `' F ` a ) e. B /\ ( `' F ` b ) e. B ) )
21 6 rgen2 
 |-  A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .* ( F ` y ) )
22 fvoveq1 
 |-  ( x = ( `' F ` a ) -> ( F ` ( x .+ y ) ) = ( F ` ( ( `' F ` a ) .+ y ) ) )
23 fveq2 
 |-  ( x = ( `' F ` a ) -> ( F ` x ) = ( F ` ( `' F ` a ) ) )
24 23 oveq1d 
 |-  ( x = ( `' F ` a ) -> ( ( F ` x ) .* ( F ` y ) ) = ( ( F ` ( `' F ` a ) ) .* ( F ` y ) ) )
25 22 24 eqeq12d 
 |-  ( x = ( `' F ` a ) -> ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .* ( F ` y ) ) <-> ( F ` ( ( `' F ` a ) .+ y ) ) = ( ( F ` ( `' F ` a ) ) .* ( F ` y ) ) ) )
26 oveq2 
 |-  ( y = ( `' F ` b ) -> ( ( `' F ` a ) .+ y ) = ( ( `' F ` a ) .+ ( `' F ` b ) ) )
27 26 fveq2d 
 |-  ( y = ( `' F ` b ) -> ( F ` ( ( `' F ` a ) .+ y ) ) = ( F ` ( ( `' F ` a ) .+ ( `' F ` b ) ) ) )
28 fveq2 
 |-  ( y = ( `' F ` b ) -> ( F ` y ) = ( F ` ( `' F ` b ) ) )
29 28 oveq2d 
 |-  ( y = ( `' F ` b ) -> ( ( F ` ( `' F ` a ) ) .* ( F ` y ) ) = ( ( F ` ( `' F ` a ) ) .* ( F ` ( `' F ` b ) ) ) )
30 27 29 eqeq12d 
 |-  ( y = ( `' F ` b ) -> ( ( F ` ( ( `' F ` a ) .+ y ) ) = ( ( F ` ( `' F ` a ) ) .* ( F ` y ) ) <-> ( F ` ( ( `' F ` a ) .+ ( `' F ` b ) ) ) = ( ( F ` ( `' F ` a ) ) .* ( F ` ( `' F ` b ) ) ) ) )
31 25 30 rspc2va 
 |-  ( ( ( ( `' F ` a ) e. B /\ ( `' F ` b ) e. B ) /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) -> ( F ` ( ( `' F ` a ) .+ ( `' F ` b ) ) ) = ( ( F ` ( `' F ` a ) ) .* ( F ` ( `' F ` b ) ) ) )
32 20 21 31 sylancl 
 |-  ( ( a e. C /\ b e. C ) -> ( F ` ( ( `' F ` a ) .+ ( `' F ` b ) ) ) = ( ( F ` ( `' F ` a ) ) .* ( F ` ( `' F ` b ) ) ) )
33 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> C /\ a e. C ) -> ( F ` ( `' F ` a ) ) = a )
34 15 33 mpan 
 |-  ( a e. C -> ( F ` ( `' F ` a ) ) = a )
35 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> C /\ b e. C ) -> ( F ` ( `' F ` b ) ) = b )
36 15 35 mpan 
 |-  ( b e. C -> ( F ` ( `' F ` b ) ) = b )
37 34 36 oveqan12d 
 |-  ( ( a e. C /\ b e. C ) -> ( ( F ` ( `' F ` a ) ) .* ( F ` ( `' F ` b ) ) ) = ( a .* b ) )
38 32 37 eqtr2d 
 |-  ( ( a e. C /\ b e. C ) -> ( a .* b ) = ( F ` ( ( `' F ` a ) .+ ( `' F ` b ) ) ) )
39 38 mpoeq3ia 
 |-  ( a e. C , b e. C |-> ( a .* b ) ) = ( a e. C , b e. C |-> ( F ` ( ( `' F ` a ) .+ ( `' F ` b ) ) ) )
40 11 39 eqtri 
 |-  .* = ( a e. C , b e. C |-> ( F ` ( ( `' F ` a ) .+ ( `' F ` b ) ) ) )
41 5 a1i 
 |-  ( T. -> K e. ( TopOn ` C ) )
42 41 41 cnmpt1st 
 |-  ( T. -> ( a e. C , b e. C |-> a ) e. ( ( K tX K ) Cn K ) )
43 hmeocnvcn 
 |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )
44 1 43 mp1i 
 |-  ( T. -> `' F e. ( K Cn J ) )
45 41 41 42 44 cnmpt21f 
 |-  ( T. -> ( a e. C , b e. C |-> ( `' F ` a ) ) e. ( ( K tX K ) Cn J ) )
46 41 41 cnmpt2nd 
 |-  ( T. -> ( a e. C , b e. C |-> b ) e. ( ( K tX K ) Cn K ) )
47 41 41 46 44 cnmpt21f 
 |-  ( T. -> ( a e. C , b e. C |-> ( `' F ` b ) ) e. ( ( K tX K ) Cn J ) )
48 7 a1i 
 |-  ( T. -> .+ e. ( ( J tX J ) Cn J ) )
49 41 41 45 47 48 cnmpt22f 
 |-  ( T. -> ( a e. C , b e. C |-> ( ( `' F ` a ) .+ ( `' F ` b ) ) ) e. ( ( K tX K ) Cn J ) )
50 hmeocn 
 |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
51 1 50 mp1i 
 |-  ( T. -> F e. ( J Cn K ) )
52 41 41 49 51 cnmpt21f 
 |-  ( T. -> ( a e. C , b e. C |-> ( F ` ( ( `' F ` a ) .+ ( `' F ` b ) ) ) ) e. ( ( K tX K ) Cn K ) )
53 52 mptru 
 |-  ( a e. C , b e. C |-> ( F ` ( ( `' F ` a ) .+ ( `' F ` b ) ) ) ) e. ( ( K tX K ) Cn K )
54 40 53 eqeltri 
 |-  .* e. ( ( K tX K ) Cn K )