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

Theorem iscmn 12910
Description: The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
iscmn.b 𝐵 = (Base‘𝐺)
iscmn.p + = (+g𝐺)
Assertion
Ref Expression
iscmn (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐺,𝑦
Allowed substitution hints:   + (𝑥,𝑦)

Proof of Theorem iscmn
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 fveq2 5510 . . . . 5 (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺))
2 iscmn.b . . . . 5 𝐵 = (Base‘𝐺)
31, 2eqtr4di 2228 . . . 4 (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵)
4 raleq 2672 . . . . 5 ((Base‘𝑔) = 𝐵 → (∀𝑦 ∈ (Base‘𝑔)(𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥) ↔ ∀𝑦𝐵 (𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥)))
54raleqbi1dv 2680 . . . 4 ((Base‘𝑔) = 𝐵 → (∀𝑥 ∈ (Base‘𝑔)∀𝑦 ∈ (Base‘𝑔)(𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥) ↔ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥)))
63, 5syl 14 . . 3 (𝑔 = 𝐺 → (∀𝑥 ∈ (Base‘𝑔)∀𝑦 ∈ (Base‘𝑔)(𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥) ↔ ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥)))
7 fveq2 5510 . . . . . . 7 (𝑔 = 𝐺 → (+g𝑔) = (+g𝐺))
8 iscmn.p . . . . . . 7 + = (+g𝐺)
97, 8eqtr4di 2228 . . . . . 6 (𝑔 = 𝐺 → (+g𝑔) = + )
109oveqd 5885 . . . . 5 (𝑔 = 𝐺 → (𝑥(+g𝑔)𝑦) = (𝑥 + 𝑦))
119oveqd 5885 . . . . 5 (𝑔 = 𝐺 → (𝑦(+g𝑔)𝑥) = (𝑦 + 𝑥))
1210, 11eqeq12d 2192 . . . 4 (𝑔 = 𝐺 → ((𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥) ↔ (𝑥 + 𝑦) = (𝑦 + 𝑥)))
13122ralbidv 2501 . . 3 (𝑔 = 𝐺 → (∀𝑥𝐵𝑦𝐵 (𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥) ↔ ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
146, 13bitrd 188 . 2 (𝑔 = 𝐺 → (∀𝑥 ∈ (Base‘𝑔)∀𝑦 ∈ (Base‘𝑔)(𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥) ↔ ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
15 df-cmn 12904 . 2 CMnd = {𝑔 ∈ Mnd ∣ ∀𝑥 ∈ (Base‘𝑔)∀𝑦 ∈ (Base‘𝑔)(𝑥(+g𝑔)𝑦) = (𝑦(+g𝑔)𝑥)}
1614, 15elrab2 2896 1 (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105   = wceq 1353  wcel 2148  wral 2455  cfv 5211  (class class class)co 5868  Basecbs 12432  +gcplusg 12505  Mndcmnd 12696  CMndccmn 12902
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-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-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-iota 5173  df-fv 5219  df-ov 5871  df-cmn 12904
This theorem is referenced by:  isabl2  12911  cmnpropd  12912  iscmnd  12915  cmnmnd  12918  cmncom  12919  iscrng2  13011
  Copyright terms: Public domain W3C validator