Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mndpluscn Structured version   Unicode version

Theorem mndpluscn 28143
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.)
Hypotheses
Ref Expression
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
Ref Expression
mndpluscn  |-  .*  e.  ( ( K  tX  K )  Cn  K
)
Distinct variable groups:    y,  .* , x    y,  .+    y, F    x,  .+    x, B, y    x, F
Allowed substitution hints:    C( x, y)    J( x, y)    K( x, y)

Proof of Theorem mndpluscn
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mndpluscn.t . . . 4  |-  .*  :
( C  X.  C
) --> C
2 ffn 5713 . . . 4  |-  (  .*  : ( C  X.  C ) --> C  ->  .*  Fn  ( C  X.  C ) )
3 fnov 6383 . . . . 5  |-  (  .*  Fn  ( C  X.  C )  <->  .*  =  ( a  e.  C ,  b  e.  C  |->  ( a  .*  b
) ) )
43biimpi 194 . . . 4  |-  (  .*  Fn  ( C  X.  C )  ->  .*  =  ( a  e.  C ,  b  e.  C  |->  ( a  .*  b
) ) )
51, 2, 4mp2b 10 . . 3  |-  .*  =  ( a  e.  C ,  b  e.  C  |->  ( a  .*  b
) )
6 mndpluscn.f . . . . . . . . 9  |-  F  e.  ( J Homeo K )
7 mndpluscn.j . . . . . . . . . . 11  |-  J  e.  (TopOn `  B )
87toponunii 19600 . . . . . . . . . 10  |-  B  = 
U. J
9 mndpluscn.k . . . . . . . . . . 11  |-  K  e.  (TopOn `  C )
109toponunii 19600 . . . . . . . . . 10  |-  C  = 
U. K
118, 10hmeof1o 20431 . . . . . . . . 9  |-  ( F  e.  ( J Homeo K )  ->  F : B
-1-1-onto-> C )
126, 11ax-mp 5 . . . . . . . 8  |-  F : B
-1-1-onto-> C
13 f1ocnvdm 6163 . . . . . . . 8  |-  ( ( F : B -1-1-onto-> C  /\  a  e.  C )  ->  ( `' F `  a )  e.  B
)
1412, 13mpan 668 . . . . . . 7  |-  ( a  e.  C  ->  ( `' F `  a )  e.  B )
15 f1ocnvdm 6163 . . . . . . . 8  |-  ( ( F : B -1-1-onto-> C  /\  b  e.  C )  ->  ( `' F `  b )  e.  B
)
1612, 15mpan 668 . . . . . . 7  |-  ( b  e.  C  ->  ( `' F `  b )  e.  B )
1714, 16anim12i 564 . . . . . 6  |-  ( ( a  e.  C  /\  b  e.  C )  ->  ( ( `' F `  a )  e.  B  /\  ( `' F `  b )  e.  B
) )
18 mndpluscn.h . . . . . . 7  |-  ( ( x  e.  B  /\  y  e.  B )  ->  ( F `  (
x  .+  y )
)  =  ( ( F `  x )  .*  ( F `  y ) ) )
1918rgen2a 2881 . . . . . 6  |-  A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y
) )  =  ( ( F `  x
)  .*  ( F `
 y ) )
20 oveq1 6277 . . . . . . . . 9  |-  ( x  =  ( `' F `  a )  ->  (
x  .+  y )  =  ( ( `' F `  a ) 
.+  y ) )
2120fveq2d 5852 . . . . . . . 8  |-  ( x  =  ( `' F `  a )  ->  ( F `  ( x  .+  y ) )  =  ( F `  (
( `' F `  a )  .+  y
) ) )
22 fveq2 5848 . . . . . . . . 9  |-  ( x  =  ( `' F `  a )  ->  ( F `  x )  =  ( F `  ( `' F `  a ) ) )
2322oveq1d 6285 . . . . . . . 8  |-  ( x  =  ( `' F `  a )  ->  (
( F `  x
)  .*  ( F `
 y ) )  =  ( ( F `
 ( `' F `  a ) )  .*  ( F `  y
) ) )
2421, 23eqeq12d 2476 . . . . . . 7  |-  ( x  =  ( `' F `  a )  ->  (
( F `  (
x  .+  y )
)  =  ( ( F `  x )  .*  ( F `  y ) )  <->  ( F `  ( ( `' F `  a )  .+  y
) )  =  ( ( F `  ( `' F `  a ) )  .*  ( F `
 y ) ) ) )
25 oveq2 6278 . . . . . . . . 9  |-  ( y  =  ( `' F `  b )  ->  (
( `' F `  a )  .+  y
)  =  ( ( `' F `  a ) 
.+  ( `' F `  b ) ) )
2625fveq2d 5852 . . . . . . . 8  |-  ( y  =  ( `' F `  b )  ->  ( F `  ( ( `' F `  a ) 
.+  y ) )  =  ( F `  ( ( `' F `  a )  .+  ( `' F `  b ) ) ) )
27 fveq2 5848 . . . . . . . . 9  |-  ( y  =  ( `' F `  b )  ->  ( F `  y )  =  ( F `  ( `' F `  b ) ) )
2827oveq2d 6286 . . . . . . . 8  |-  ( y  =  ( `' F `  b )  ->  (
( F `  ( `' F `  a ) )  .*  ( F `
 y ) )  =  ( ( F `
 ( `' F `  a ) )  .*  ( F `  ( `' F `  b ) ) ) )
2926, 28eqeq12d 2476 . . . . . . 7  |-  ( y  =  ( `' F `  b )  ->  (
( F `  (
( `' F `  a )  .+  y
) )  =  ( ( F `  ( `' F `  a ) )  .*  ( F `
 y ) )  <-> 
( F `  (
( `' F `  a )  .+  ( `' F `  b ) ) )  =  ( ( F `  ( `' F `  a ) )  .*  ( F `
 ( `' F `  b ) ) ) ) )
3024, 29rspc2va 3217 . . . . . 6  |-  ( ( ( ( `' 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 ) ) ) )
3117, 19, 30sylancl 660 . . . . 5  |-  ( ( a  e.  C  /\  b  e.  C )  ->  ( F `  (
( `' F `  a )  .+  ( `' F `  b ) ) )  =  ( ( F `  ( `' F `  a ) )  .*  ( F `
 ( `' F `  b ) ) ) )
32 f1ocnvfv2 6158 . . . . . . 7  |-  ( ( F : B -1-1-onto-> C  /\  a  e.  C )  ->  ( F `  ( `' F `  a ) )  =  a )
3312, 32mpan 668 . . . . . 6  |-  ( a  e.  C  ->  ( F `  ( `' F `  a )
)  =  a )
34 f1ocnvfv2 6158 . . . . . . 7  |-  ( ( F : B -1-1-onto-> C  /\  b  e.  C )  ->  ( F `  ( `' F `  b ) )  =  b )
3512, 34mpan 668 . . . . . 6  |-  ( b  e.  C  ->  ( F `  ( `' F `  b )
)  =  b )
3633, 35oveqan12d 6289 . . . . 5  |-  ( ( a  e.  C  /\  b  e.  C )  ->  ( ( F `  ( `' F `  a ) )  .*  ( F `
 ( `' F `  b ) ) )  =  ( a  .*  b ) )
3731, 36eqtr2d 2496 . . . 4  |-  ( ( a  e.  C  /\  b  e.  C )  ->  ( a  .*  b
)  =  ( F `
 ( ( `' F `  a ) 
.+  ( `' F `  b ) ) ) )
3837mpt2eq3ia 6335 . . 3  |-  ( a  e.  C ,  b  e.  C  |->  ( a  .*  b ) )  =  ( a  e.  C ,  b  e.  C  |->  ( F `  ( ( `' F `  a )  .+  ( `' F `  b ) ) ) )
395, 38eqtri 2483 . 2  |-  .*  =  ( a  e.  C ,  b  e.  C  |->  ( F `  (
( `' F `  a )  .+  ( `' F `  b ) ) ) )
409a1i 11 . . . 4  |-  ( T. 
->  K  e.  (TopOn `  C ) )
4140, 40cnmpt1st 20335 . . . . . 6  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  a )  e.  ( ( K  tX  K
)  Cn  K ) )
42 hmeocnvcn 20428 . . . . . . 7  |-  ( F  e.  ( J Homeo K )  ->  `' F  e.  ( K  Cn  J
) )
436, 42mp1i 12 . . . . . 6  |-  ( T. 
->  `' F  e.  ( K  Cn  J ) )
4440, 40, 41, 43cnmpt21f 20339 . . . . 5  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  ( `' F `  a ) )  e.  ( ( K  tX  K )  Cn  J
) )
4540, 40cnmpt2nd 20336 . . . . . 6  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  b )  e.  ( ( K  tX  K
)  Cn  K ) )
4640, 40, 45, 43cnmpt21f 20339 . . . . 5  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  ( `' F `  b ) )  e.  ( ( K  tX  K )  Cn  J
) )
47 mndpluscn.o . . . . . 6  |-  .+  e.  ( ( J  tX  J )  Cn  J
)
4847a1i 11 . . . . 5  |-  ( T. 
->  .+  e.  ( ( J  tX  J )  Cn  J ) )
4940, 40, 44, 46, 48cnmpt22f 20342 . . . 4  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  ( ( `' F `  a )  .+  ( `' F `  b ) ) )  e.  ( ( K  tX  K
)  Cn  J ) )
50 hmeocn 20427 . . . . 5  |-  ( F  e.  ( J Homeo K )  ->  F  e.  ( J  Cn  K
) )
516, 50mp1i 12 . . . 4  |-  ( T. 
->  F  e.  ( J  Cn  K ) )
5240, 40, 49, 51cnmpt21f 20339 . . 3  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  ( F `  (
( `' F `  a )  .+  ( `' F `  b ) ) ) )  e.  ( ( K  tX  K )  Cn  K
) )
5352trud 1407 . 2  |-  ( a  e.  C ,  b  e.  C  |->  ( F `
 ( ( `' F `  a ) 
.+  ( `' F `  b ) ) ) )  e.  ( ( K  tX  K )  Cn  K )
5439, 53eqeltri 2538 1  |-  .*  e.  ( ( K  tX  K )  Cn  K
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398   T. wtru 1399    e. wcel 1823   A.wral 2804    X. cxp 4986   `'ccnv 4987    Fn wfn 5565   -->wf 5566   -1-1-onto->wf1o 5569   ` cfv 5570  (class class class)co 6270    |-> cmpt2 6272  TopOnctopon 19562    Cn ccn 19892    tX ctx 20227   Homeochmeo 20420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-1st 6773  df-2nd 6774  df-map 7414  df-topgen 14933  df-top 19566  df-bases 19568  df-topon 19569  df-cn 19895  df-tx 20229  df-hmeo 20422
This theorem is referenced by:  mhmhmeotmd  28144  xrge0pluscn  28157
  Copyright terms: Public domain W3C validator