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

Theorem mndpluscn 30506
 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 𝐹 ∈ (𝐽Homeo𝐾)
mndpluscn.p + :(𝐵 × 𝐵)⟶𝐵
mndpluscn.t :(𝐶 × 𝐶)⟶𝐶
mndpluscn.j 𝐽 ∈ (TopOn‘𝐵)
mndpluscn.k 𝐾 ∈ (TopOn‘𝐶)
mndpluscn.h ((𝑥𝐵𝑦𝐵) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
mndpluscn.o + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Assertion
Ref Expression
mndpluscn ∈ ((𝐾 ×t 𝐾) Cn 𝐾)
Distinct variable groups:   𝑦, ,𝑥   𝑦, +   𝑦,𝐹   𝑥, +   𝑥,𝐵,𝑦   𝑥,𝐹
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐽(𝑥,𝑦)   𝐾(𝑥,𝑦)

Proof of Theorem mndpluscn
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mndpluscn.t . . . 4 :(𝐶 × 𝐶)⟶𝐶
2 ffn 6278 . . . 4 ( :(𝐶 × 𝐶)⟶𝐶 Fn (𝐶 × 𝐶))
3 fnov 7028 . . . . 5 ( Fn (𝐶 × 𝐶) ↔ = (𝑎𝐶, 𝑏𝐶 ↦ (𝑎 𝑏)))
43biimpi 208 . . . 4 ( Fn (𝐶 × 𝐶) → = (𝑎𝐶, 𝑏𝐶 ↦ (𝑎 𝑏)))
51, 2, 4mp2b 10 . . 3 = (𝑎𝐶, 𝑏𝐶 ↦ (𝑎 𝑏))
6 mndpluscn.f . . . . . . . . 9 𝐹 ∈ (𝐽Homeo𝐾)
7 mndpluscn.j . . . . . . . . . . 11 𝐽 ∈ (TopOn‘𝐵)
87toponunii 21091 . . . . . . . . . 10 𝐵 = 𝐽
9 mndpluscn.k . . . . . . . . . . 11 𝐾 ∈ (TopOn‘𝐶)
109toponunii 21091 . . . . . . . . . 10 𝐶 = 𝐾
118, 10hmeof1o 21938 . . . . . . . . 9 (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝐵1-1-onto𝐶)
126, 11ax-mp 5 . . . . . . . 8 𝐹:𝐵1-1-onto𝐶
13 f1ocnvdm 6795 . . . . . . . 8 ((𝐹:𝐵1-1-onto𝐶𝑎𝐶) → (𝐹𝑎) ∈ 𝐵)
1412, 13mpan 681 . . . . . . 7 (𝑎𝐶 → (𝐹𝑎) ∈ 𝐵)
15 f1ocnvdm 6795 . . . . . . . 8 ((𝐹:𝐵1-1-onto𝐶𝑏𝐶) → (𝐹𝑏) ∈ 𝐵)
1612, 15mpan 681 . . . . . . 7 (𝑏𝐶 → (𝐹𝑏) ∈ 𝐵)
1714, 16anim12i 606 . . . . . 6 ((𝑎𝐶𝑏𝐶) → ((𝐹𝑎) ∈ 𝐵 ∧ (𝐹𝑏) ∈ 𝐵))
18 mndpluscn.h . . . . . . 7 ((𝑥𝐵𝑦𝐵) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
1918rgen2a 3186 . . . . . 6 𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦))
20 fvoveq1 6928 . . . . . . . 8 (𝑥 = (𝐹𝑎) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘((𝐹𝑎) + 𝑦)))
21 fveq2 6433 . . . . . . . . 9 (𝑥 = (𝐹𝑎) → (𝐹𝑥) = (𝐹‘(𝐹𝑎)))
2221oveq1d 6920 . . . . . . . 8 (𝑥 = (𝐹𝑎) → ((𝐹𝑥) (𝐹𝑦)) = ((𝐹‘(𝐹𝑎)) (𝐹𝑦)))
2320, 22eqeq12d 2840 . . . . . . 7 (𝑥 = (𝐹𝑎) → ((𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ↔ (𝐹‘((𝐹𝑎) + 𝑦)) = ((𝐹‘(𝐹𝑎)) (𝐹𝑦))))
24 oveq2 6913 . . . . . . . . 9 (𝑦 = (𝐹𝑏) → ((𝐹𝑎) + 𝑦) = ((𝐹𝑎) + (𝐹𝑏)))
2524fveq2d 6437 . . . . . . . 8 (𝑦 = (𝐹𝑏) → (𝐹‘((𝐹𝑎) + 𝑦)) = (𝐹‘((𝐹𝑎) + (𝐹𝑏))))
26 fveq2 6433 . . . . . . . . 9 (𝑦 = (𝐹𝑏) → (𝐹𝑦) = (𝐹‘(𝐹𝑏)))
2726oveq2d 6921 . . . . . . . 8 (𝑦 = (𝐹𝑏) → ((𝐹‘(𝐹𝑎)) (𝐹𝑦)) = ((𝐹‘(𝐹𝑎)) (𝐹‘(𝐹𝑏))))
2825, 27eqeq12d 2840 . . . . . . 7 (𝑦 = (𝐹𝑏) → ((𝐹‘((𝐹𝑎) + 𝑦)) = ((𝐹‘(𝐹𝑎)) (𝐹𝑦)) ↔ (𝐹‘((𝐹𝑎) + (𝐹𝑏))) = ((𝐹‘(𝐹𝑎)) (𝐹‘(𝐹𝑏)))))
2923, 28rspc2va 3540 . . . . . 6 ((((𝐹𝑎) ∈ 𝐵 ∧ (𝐹𝑏) ∈ 𝐵) ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦))) → (𝐹‘((𝐹𝑎) + (𝐹𝑏))) = ((𝐹‘(𝐹𝑎)) (𝐹‘(𝐹𝑏))))
3017, 19, 29sylancl 580 . . . . 5 ((𝑎𝐶𝑏𝐶) → (𝐹‘((𝐹𝑎) + (𝐹𝑏))) = ((𝐹‘(𝐹𝑎)) (𝐹‘(𝐹𝑏))))
31 f1ocnvfv2 6788 . . . . . . 7 ((𝐹:𝐵1-1-onto𝐶𝑎𝐶) → (𝐹‘(𝐹𝑎)) = 𝑎)
3212, 31mpan 681 . . . . . 6 (𝑎𝐶 → (𝐹‘(𝐹𝑎)) = 𝑎)
33 f1ocnvfv2 6788 . . . . . . 7 ((𝐹:𝐵1-1-onto𝐶𝑏𝐶) → (𝐹‘(𝐹𝑏)) = 𝑏)
3412, 33mpan 681 . . . . . 6 (𝑏𝐶 → (𝐹‘(𝐹𝑏)) = 𝑏)
3532, 34oveqan12d 6924 . . . . 5 ((𝑎𝐶𝑏𝐶) → ((𝐹‘(𝐹𝑎)) (𝐹‘(𝐹𝑏))) = (𝑎 𝑏))
3630, 35eqtr2d 2862 . . . 4 ((𝑎𝐶𝑏𝐶) → (𝑎 𝑏) = (𝐹‘((𝐹𝑎) + (𝐹𝑏))))
3736mpt2eq3ia 6980 . . 3 (𝑎𝐶, 𝑏𝐶 ↦ (𝑎 𝑏)) = (𝑎𝐶, 𝑏𝐶 ↦ (𝐹‘((𝐹𝑎) + (𝐹𝑏))))
385, 37eqtri 2849 . 2 = (𝑎𝐶, 𝑏𝐶 ↦ (𝐹‘((𝐹𝑎) + (𝐹𝑏))))
399a1i 11 . . . 4 (⊤ → 𝐾 ∈ (TopOn‘𝐶))
4039, 39cnmpt1st 21842 . . . . . 6 (⊤ → (𝑎𝐶, 𝑏𝐶𝑎) ∈ ((𝐾 ×t 𝐾) Cn 𝐾))
41 hmeocnvcn 21935 . . . . . . 7 (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐾 Cn 𝐽))
426, 41mp1i 13 . . . . . 6 (⊤ → 𝐹 ∈ (𝐾 Cn 𝐽))
4339, 39, 40, 42cnmpt21f 21846 . . . . 5 (⊤ → (𝑎𝐶, 𝑏𝐶 ↦ (𝐹𝑎)) ∈ ((𝐾 ×t 𝐾) Cn 𝐽))
4439, 39cnmpt2nd 21843 . . . . . 6 (⊤ → (𝑎𝐶, 𝑏𝐶𝑏) ∈ ((𝐾 ×t 𝐾) Cn 𝐾))
4539, 39, 44, 42cnmpt21f 21846 . . . . 5 (⊤ → (𝑎𝐶, 𝑏𝐶 ↦ (𝐹𝑏)) ∈ ((𝐾 ×t 𝐾) Cn 𝐽))
46 mndpluscn.o . . . . . 6 + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
4746a1i 11 . . . . 5 (⊤ → + ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
4839, 39, 43, 45, 47cnmpt22f 21849 . . . 4 (⊤ → (𝑎𝐶, 𝑏𝐶 ↦ ((𝐹𝑎) + (𝐹𝑏))) ∈ ((𝐾 ×t 𝐾) Cn 𝐽))
49 hmeocn 21934 . . . . 5 (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾))
506, 49mp1i 13 . . . 4 (⊤ → 𝐹 ∈ (𝐽 Cn 𝐾))
5139, 39, 48, 50cnmpt21f 21846 . . 3 (⊤ → (𝑎𝐶, 𝑏𝐶 ↦ (𝐹‘((𝐹𝑎) + (𝐹𝑏)))) ∈ ((𝐾 ×t 𝐾) Cn 𝐾))
5251mptru 1664 . 2 (𝑎𝐶, 𝑏𝐶 ↦ (𝐹‘((𝐹𝑎) + (𝐹𝑏)))) ∈ ((𝐾 ×t 𝐾) Cn 𝐾)
5338, 52eqeltri 2902 1 ∈ ((𝐾 ×t 𝐾) Cn 𝐾)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   = wceq 1656  ⊤wtru 1657   ∈ wcel 2164  ∀wral 3117   × cxp 5340  ◡ccnv 5341   Fn wfn 6118  ⟶wf 6119  –1-1-onto→wf1o 6122  ‘cfv 6123  (class class class)co 6905   ↦ cmpt2 6907  TopOnctopon 21085   Cn ccn 21399   ×t ctx 21734  Homeochmeo 21927 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-1st 7428  df-2nd 7429  df-map 8124  df-topgen 16457  df-top 21069  df-topon 21086  df-bases 21121  df-cn 21402  df-tx 21736  df-hmeo 21929 This theorem is referenced by:  mhmhmeotmd  30507  xrge0pluscn  30520
 Copyright terms: Public domain W3C validator