ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  issubmnd GIF version

Theorem issubmnd 12848
Description: Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.)
Hypotheses
Ref Expression
issubmnd.b 𝐵 = (Base‘𝐺)
issubmnd.p + = (+g𝐺)
issubmnd.z 0 = (0g𝐺)
issubmnd.h 𝐻 = (𝐺s 𝑆)
Assertion
Ref Expression
issubmnd ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → (𝐻 ∈ Mnd ↔ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐺,𝑦   𝑥,𝐻,𝑦   𝑥, + ,𝑦   𝑥,𝑆,𝑦   𝑥, 0 ,𝑦

Proof of Theorem issubmnd
Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 528 . . . . 5 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → 𝐻 ∈ Mnd)
2 simprl 529 . . . . . 6 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → 𝑥𝑆)
3 issubmnd.h . . . . . . . . 9 𝐻 = (𝐺s 𝑆)
43a1i 9 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → 𝐻 = (𝐺s 𝑆))
5 issubmnd.b . . . . . . . . 9 𝐵 = (Base‘𝐺)
65a1i 9 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → 𝐵 = (Base‘𝐺))
7 simp1 997 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → 𝐺 ∈ Mnd)
8 simp2 998 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → 𝑆𝐵)
94, 6, 7, 8ressbas2d 12530 . . . . . . 7 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → 𝑆 = (Base‘𝐻))
109ad2antrr 488 . . . . . 6 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → 𝑆 = (Base‘𝐻))
112, 10eleqtrd 2256 . . . . 5 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → 𝑥 ∈ (Base‘𝐻))
12 simprr 531 . . . . . 6 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → 𝑦𝑆)
1312, 10eleqtrd 2256 . . . . 5 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → 𝑦 ∈ (Base‘𝐻))
14 eqid 2177 . . . . . 6 (Base‘𝐻) = (Base‘𝐻)
15 eqid 2177 . . . . . 6 (+g𝐻) = (+g𝐻)
1614, 15mndcl 12829 . . . . 5 ((𝐻 ∈ Mnd ∧ 𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)) → (𝑥(+g𝐻)𝑦) ∈ (Base‘𝐻))
171, 11, 13, 16syl3anc 1238 . . . 4 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥(+g𝐻)𝑦) ∈ (Base‘𝐻))
18 issubmnd.p . . . . . . . 8 + = (+g𝐺)
1918a1i 9 . . . . . . 7 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → + = (+g𝐺))
20 basfn 12522 . . . . . . . . . . 11 Base Fn V
21 elex 2750 . . . . . . . . . . 11 (𝐺 ∈ Mnd → 𝐺 ∈ V)
22 funfvex 5534 . . . . . . . . . . . 12 ((Fun Base ∧ 𝐺 ∈ dom Base) → (Base‘𝐺) ∈ V)
2322funfni 5318 . . . . . . . . . . 11 ((Base Fn V ∧ 𝐺 ∈ V) → (Base‘𝐺) ∈ V)
2420, 21, 23sylancr 414 . . . . . . . . . 10 (𝐺 ∈ Mnd → (Base‘𝐺) ∈ V)
255, 24eqeltrid 2264 . . . . . . . . 9 (𝐺 ∈ Mnd → 𝐵 ∈ V)
267, 25syl 14 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → 𝐵 ∈ V)
2726, 8ssexd 4145 . . . . . . 7 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → 𝑆 ∈ V)
284, 19, 27, 7ressplusgd 12589 . . . . . 6 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → + = (+g𝐻))
2928ad2antrr 488 . . . . 5 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → + = (+g𝐻))
3029oveqd 5894 . . . 4 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) = (𝑥(+g𝐻)𝑦))
3117, 30, 103eltr4d 2261 . . 3 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
3231ralrimivva 2559 . 2 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ 𝐻 ∈ Mnd) → ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)
339adantr 276 . . 3 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 𝑆 = (Base‘𝐻))
3428adantr 276 . . 3 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → + = (+g𝐻))
35 ovrspc2v 5903 . . . . . 6 (((𝑢𝑆𝑣𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆)
3635ancoms 268 . . . . 5 ((∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝑢𝑆𝑣𝑆)) → (𝑢 + 𝑣) ∈ 𝑆)
37363impb 1199 . . . 4 ((∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆𝑢𝑆𝑣𝑆) → (𝑢 + 𝑣) ∈ 𝑆)
38373adant1l 1230 . . 3 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢𝑆𝑣𝑆) → (𝑢 + 𝑣) ∈ 𝑆)
39 simpl1 1000 . . . 4 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 𝐺 ∈ Mnd)
40 simpl2 1001 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 𝑆𝐵)
4140sseld 3156 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → (𝑢𝑆𝑢𝐵))
4240sseld 3156 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → (𝑣𝑆𝑣𝐵))
4340sseld 3156 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → (𝑤𝑆𝑤𝐵))
4441, 42, 433anim123d 1319 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → ((𝑢𝑆𝑣𝑆𝑤𝑆) → (𝑢𝐵𝑣𝐵𝑤𝐵)))
4544imp 124 . . . 4 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ (𝑢𝑆𝑣𝑆𝑤𝑆)) → (𝑢𝐵𝑣𝐵𝑤𝐵))
465, 18mndass 12830 . . . 4 ((𝐺 ∈ Mnd ∧ (𝑢𝐵𝑣𝐵𝑤𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
4739, 45, 46syl2an2r 595 . . 3 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ (𝑢𝑆𝑣𝑆𝑤𝑆)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
48 simpl3 1002 . . 3 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 0𝑆)
4940sselda 3157 . . . 4 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢𝑆) → 𝑢𝐵)
50 issubmnd.z . . . . 5 0 = (0g𝐺)
515, 18, 50mndlid 12841 . . . 4 ((𝐺 ∈ Mnd ∧ 𝑢𝐵) → ( 0 + 𝑢) = 𝑢)
5239, 49, 51syl2an2r 595 . . 3 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢𝑆) → ( 0 + 𝑢) = 𝑢)
535, 18, 50mndrid 12842 . . . 4 ((𝐺 ∈ Mnd ∧ 𝑢𝐵) → (𝑢 + 0 ) = 𝑢)
5439, 49, 53syl2an2r 595 . . 3 ((((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢𝑆) → (𝑢 + 0 ) = 𝑢)
5533, 34, 38, 47, 48, 52, 54ismndd 12843 . 2 (((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 𝐻 ∈ Mnd)
5632, 55impbida 596 1 ((𝐺 ∈ Mnd ∧ 𝑆𝐵0𝑆) → (𝐻 ∈ Mnd ↔ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978   = wceq 1353  wcel 2148  wral 2455  Vcvv 2739  wss 3131   Fn wfn 5213  cfv 5218  (class class class)co 5877  Basecbs 12464  s cress 12465  +gcplusg 12538  0gc0g 12710  Mndcmnd 12822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-addcom 7913  ax-addass 7915  ax-i2m1 7918  ax-0lt1 7919  ax-0id 7921  ax-rnegex 7922  ax-pre-ltirr 7925  ax-pre-ltadd 7929
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-iota 5180  df-fun 5220  df-fn 5221  df-fv 5226  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-pnf 7996  df-mnf 7997  df-ltxr 7999  df-inn 8922  df-2 8980  df-ndx 12467  df-slot 12468  df-base 12470  df-sets 12471  df-iress 12472  df-plusg 12551  df-0g 12712  df-mgm 12780  df-sgrp 12813  df-mnd 12823
This theorem is referenced by:  issubm2  12869
  Copyright terms: Public domain W3C validator