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

Theorem mndpluscn 26494
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 5660 . . . 4  |-  (  .*  : ( C  X.  C ) --> C  ->  .*  Fn  ( C  X.  C ) )
3 fnov 6301 . . . . 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 18662 . . . . . . . . . 10  |-  B  = 
U. J
9 mndpluscn.k . . . . . . . . . . 11  |-  K  e.  (TopOn `  C )
109toponunii 18662 . . . . . . . . . 10  |-  C  = 
U. K
118, 10hmeof1o 19462 . . . . . . . . 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 6091 . . . . . . . 8  |-  ( ( F : B -1-1-onto-> C  /\  a  e.  C )  ->  ( `' F `  a )  e.  B
)
1412, 13mpan 670 . . . . . . 7  |-  ( a  e.  C  ->  ( `' F `  a )  e.  B )
15 f1ocnvdm 6091 . . . . . . . 8  |-  ( ( F : B -1-1-onto-> C  /\  b  e.  C )  ->  ( `' F `  b )  e.  B
)
1612, 15mpan 670 . . . . . . 7  |-  ( b  e.  C  ->  ( `' F `  b )  e.  B )
1714, 16anim12i 566 . . . . . 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 2893 . . . . . 6  |-  A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y
) )  =  ( ( F `  x
)  .*  ( F `
 y ) )
20 oveq1 6200 . . . . . . . . 9  |-  ( x  =  ( `' F `  a )  ->  (
x  .+  y )  =  ( ( `' F `  a ) 
.+  y ) )
2120fveq2d 5796 . . . . . . . 8  |-  ( x  =  ( `' F `  a )  ->  ( F `  ( x  .+  y ) )  =  ( F `  (
( `' F `  a )  .+  y
) ) )
22 fveq2 5792 . . . . . . . . 9  |-  ( x  =  ( `' F `  a )  ->  ( F `  x )  =  ( F `  ( `' F `  a ) ) )
2322oveq1d 6208 . . . . . . . 8  |-  ( x  =  ( `' F `  a )  ->  (
( F `  x
)  .*  ( F `
 y ) )  =  ( ( F `
 ( `' F `  a ) )  .*  ( F `  y
) ) )
2421, 23eqeq12d 2473 . . . . . . 7  |-  ( x  =  ( `' F `  a )  ->  (
( F `  (
x  .+  y )
)  =  ( ( F `  x )  .*  ( F `  y ) )  <->  ( F `  ( ( `' F `  a )  .+  y
) )  =  ( ( F `  ( `' F `  a ) )  .*  ( F `
 y ) ) ) )
25 oveq2 6201 . . . . . . . . 9  |-  ( y  =  ( `' F `  b )  ->  (
( `' F `  a )  .+  y
)  =  ( ( `' F `  a ) 
.+  ( `' F `  b ) ) )
2625fveq2d 5796 . . . . . . . 8  |-  ( y  =  ( `' F `  b )  ->  ( F `  ( ( `' F `  a ) 
.+  y ) )  =  ( F `  ( ( `' F `  a )  .+  ( `' F `  b ) ) ) )
27 fveq2 5792 . . . . . . . . 9  |-  ( y  =  ( `' F `  b )  ->  ( F `  y )  =  ( F `  ( `' F `  b ) ) )
2827oveq2d 6209 . . . . . . . 8  |-  ( y  =  ( `' F `  b )  ->  (
( F `  ( `' F `  a ) )  .*  ( F `
 y ) )  =  ( ( F `
 ( `' F `  a ) )  .*  ( F `  ( `' F `  b ) ) ) )
2926, 28eqeq12d 2473 . . . . . . 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 3180 . . . . . 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 662 . . . . 5  |-  ( ( a  e.  C  /\  b  e.  C )  ->  ( F `  (
( `' F `  a )  .+  ( `' F `  b ) ) )  =  ( ( F `  ( `' F `  a ) )  .*  ( F `
 ( `' F `  b ) ) ) )
32 f1ocnvfv2 6086 . . . . . . 7  |-  ( ( F : B -1-1-onto-> C  /\  a  e.  C )  ->  ( F `  ( `' F `  a ) )  =  a )
3312, 32mpan 670 . . . . . 6  |-  ( a  e.  C  ->  ( F `  ( `' F `  a )
)  =  a )
34 f1ocnvfv2 6086 . . . . . . 7  |-  ( ( F : B -1-1-onto-> C  /\  b  e.  C )  ->  ( F `  ( `' F `  b ) )  =  b )
3512, 34mpan 670 . . . . . 6  |-  ( b  e.  C  ->  ( F `  ( `' F `  b )
)  =  b )
3633, 35oveqan12d 6212 . . . . 5  |-  ( ( a  e.  C  /\  b  e.  C )  ->  ( ( F `  ( `' F `  a ) )  .*  ( F `
 ( `' F `  b ) ) )  =  ( a  .*  b ) )
3731, 36eqtr2d 2493 . . . 4  |-  ( ( a  e.  C  /\  b  e.  C )  ->  ( a  .*  b
)  =  ( F `
 ( ( `' F `  a ) 
.+  ( `' F `  b ) ) ) )
3837mpt2eq3ia 6253 . . 3  |-  ( a  e.  C ,  b  e.  C  |->  ( a  .*  b ) )  =  ( a  e.  C ,  b  e.  C  |->  ( F `  ( ( `' F `  a )  .+  ( `' F `  b ) ) ) )
395, 38eqtri 2480 . 2  |-  .*  =  ( a  e.  C ,  b  e.  C  |->  ( F `  (
( `' F `  a )  .+  ( `' F `  b ) ) ) )
409a1i 11 . . . 4  |-  ( T. 
->  K  e.  (TopOn `  C ) )
4140, 40cnmpt1st 19366 . . . . . 6  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  a )  e.  ( ( K  tX  K
)  Cn  K ) )
42 hmeocnvcn 19459 . . . . . . 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 19370 . . . . 5  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  ( `' F `  a ) )  e.  ( ( K  tX  K )  Cn  J
) )
4540, 40cnmpt2nd 19367 . . . . . 6  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  b )  e.  ( ( K  tX  K
)  Cn  K ) )
4640, 40, 45, 43cnmpt21f 19370 . . . . 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 19373 . . . 4  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  ( ( `' F `  a )  .+  ( `' F `  b ) ) )  e.  ( ( K  tX  K
)  Cn  J ) )
50 hmeocn 19458 . . . . 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 19370 . . 3  |-  ( T. 
->  ( a  e.  C ,  b  e.  C  |->  ( F `  (
( `' F `  a )  .+  ( `' F `  b ) ) ) )  e.  ( ( K  tX  K )  Cn  K
) )
5352trud 1379 . 2  |-  ( a  e.  C ,  b  e.  C  |->  ( F `
 ( ( `' F `  a ) 
.+  ( `' F `  b ) ) ) )  e.  ( ( K  tX  K )  Cn  K )
5439, 53eqeltri 2535 1  |-  .*  e.  ( ( K  tX  K )  Cn  K
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370   T. wtru 1371    e. wcel 1758   A.wral 2795    X. cxp 4939   `'ccnv 4940    Fn wfn 5514   -->wf 5515   -1-1-onto->wf1o 5518   ` cfv 5519  (class class class)co 6193    |-> cmpt2 6195  TopOnctopon 18624    Cn ccn 18953    tX ctx 19258   Homeochmeo 19451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-1st 6680  df-2nd 6681  df-map 7319  df-topgen 14493  df-top 18628  df-bases 18630  df-topon 18631  df-cn 18956  df-tx 19260  df-hmeo 19453
This theorem is referenced by:  mhmhmeotmd  26495  xrge0pluscn  26508
  Copyright terms: Public domain W3C validator