MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mgmlrid Structured version   Visualization version   GIF version

Theorem mgmlrid 18163
Description: The identity element of a magma, if it exists, is a left and right identity. (Contributed by Mario Carneiro, 27-Dec-2014.)
Hypotheses
Ref Expression
ismgmid.b 𝐵 = (Base‘𝐺)
ismgmid.o 0 = (0g𝐺)
ismgmid.p + = (+g𝐺)
mgmidcl.e (𝜑 → ∃𝑒𝐵𝑥𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))
Assertion
Ref Expression
mgmlrid ((𝜑𝑋𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
Distinct variable groups:   𝑥,𝑒, +   0 ,𝑒,𝑥   𝐵,𝑒,𝑥   𝑒,𝐺,𝑥   𝑥,𝑋
Allowed substitution hints:   𝜑(𝑥,𝑒)   𝑋(𝑒)

Proof of Theorem mgmlrid
StepHypRef Expression
1 eqid 2738 . . . 4 0 = 0
2 ismgmid.b . . . . 5 𝐵 = (Base‘𝐺)
3 ismgmid.o . . . . 5 0 = (0g𝐺)
4 ismgmid.p . . . . 5 + = (+g𝐺)
5 mgmidcl.e . . . . 5 (𝜑 → ∃𝑒𝐵𝑥𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))
62, 3, 4, 5ismgmid 18161 . . . 4 (𝜑 → (( 0𝐵 ∧ ∀𝑥𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) ↔ 0 = 0 ))
71, 6mpbiri 261 . . 3 (𝜑 → ( 0𝐵 ∧ ∀𝑥𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)))
87simprd 499 . 2 (𝜑 → ∀𝑥𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))
9 oveq2 7239 . . . . 5 (𝑥 = 𝑋 → ( 0 + 𝑥) = ( 0 + 𝑋))
10 id 22 . . . . 5 (𝑥 = 𝑋𝑥 = 𝑋)
119, 10eqeq12d 2754 . . . 4 (𝑥 = 𝑋 → (( 0 + 𝑥) = 𝑥 ↔ ( 0 + 𝑋) = 𝑋))
12 oveq1 7238 . . . . 5 (𝑥 = 𝑋 → (𝑥 + 0 ) = (𝑋 + 0 ))
1312, 10eqeq12d 2754 . . . 4 (𝑥 = 𝑋 → ((𝑥 + 0 ) = 𝑥 ↔ (𝑋 + 0 ) = 𝑋))
1411, 13anbi12d 634 . . 3 (𝑥 = 𝑋 → ((( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥) ↔ (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋)))
1514rspccva 3548 . 2 ((∀𝑥𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥) ∧ 𝑋𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
168, 15sylan 583 1 ((𝜑𝑋𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2111  wral 3062  wrex 3063  cfv 6397  (class class class)co 7231  Basecbs 16784  +gcplusg 16826  0gc0g 16968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pr 5336
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-iota 6355  df-fun 6399  df-fv 6405  df-riota 7188  df-ov 7234  df-0g 16970
This theorem is referenced by:  mndlrid  18216
  Copyright terms: Public domain W3C validator