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

Theorem grprinvd 5696
Description: Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
grprinvlem.c ((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
grprinvlem.o (𝜑𝑂𝐵)
grprinvlem.i ((𝜑𝑥𝐵) → (𝑂 + 𝑥) = 𝑥)
grprinvlem.a ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
grprinvlem.n ((𝜑𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 𝑂)
grprinvd.x ((𝜑𝜓) → 𝑋𝐵)
grprinvd.n ((𝜑𝜓) → 𝑁𝐵)
grprinvd.e ((𝜑𝜓) → (𝑁 + 𝑋) = 𝑂)
Assertion
Ref Expression
grprinvd ((𝜑𝜓) → (𝑋 + 𝑁) = 𝑂)
Distinct variable groups:   𝑥,𝑦,𝑧,𝐵   𝑥,𝑂,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑦,𝑁,𝑧   𝑥, + ,𝑦,𝑧   𝑦,𝑋,𝑧   𝜓,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑧)   𝑁(𝑥)   𝑋(𝑥)

Proof of Theorem grprinvd
Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grprinvlem.c . 2 ((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
2 grprinvlem.o . 2 (𝜑𝑂𝐵)
3 grprinvlem.i . 2 ((𝜑𝑥𝐵) → (𝑂 + 𝑥) = 𝑥)
4 grprinvlem.a . 2 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
5 grprinvlem.n . 2 ((𝜑𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 𝑂)
613expb 1105 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
76caovclg 5653 . . . 4 ((𝜑 ∧ (𝑢𝐵𝑣𝐵)) → (𝑢 + 𝑣) ∈ 𝐵)
87adantlr 446 . . 3 (((𝜑𝜓) ∧ (𝑢𝐵𝑣𝐵)) → (𝑢 + 𝑣) ∈ 𝐵)
9 grprinvd.x . . 3 ((𝜑𝜓) → 𝑋𝐵)
10 grprinvd.n . . 3 ((𝜑𝜓) → 𝑁𝐵)
118, 9, 10caovcld 5654 . 2 ((𝜑𝜓) → (𝑋 + 𝑁) ∈ 𝐵)
124caovassg 5659 . . . . 5 ((𝜑 ∧ (𝑢𝐵𝑣𝐵𝑤𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
1312adantlr 446 . . . 4 (((𝜑𝜓) ∧ (𝑢𝐵𝑣𝐵𝑤𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤)))
1413, 9, 10, 11caovassd 5660 . . 3 ((𝜑𝜓) → ((𝑋 + 𝑁) + (𝑋 + 𝑁)) = (𝑋 + (𝑁 + (𝑋 + 𝑁))))
15 grprinvd.e . . . . . 6 ((𝜑𝜓) → (𝑁 + 𝑋) = 𝑂)
1615oveq1d 5527 . . . . 5 ((𝜑𝜓) → ((𝑁 + 𝑋) + 𝑁) = (𝑂 + 𝑁))
1713, 10, 9, 10caovassd 5660 . . . . 5 ((𝜑𝜓) → ((𝑁 + 𝑋) + 𝑁) = (𝑁 + (𝑋 + 𝑁)))
183ralrimiva 2392 . . . . . . . 8 (𝜑 → ∀𝑥𝐵 (𝑂 + 𝑥) = 𝑥)
19 oveq2 5520 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑂 + 𝑥) = (𝑂 + 𝑦))
20 id 19 . . . . . . . . . 10 (𝑥 = 𝑦𝑥 = 𝑦)
2119, 20eqeq12d 2054 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑂 + 𝑥) = 𝑥 ↔ (𝑂 + 𝑦) = 𝑦))
2221cbvralv 2533 . . . . . . . 8 (∀𝑥𝐵 (𝑂 + 𝑥) = 𝑥 ↔ ∀𝑦𝐵 (𝑂 + 𝑦) = 𝑦)
2318, 22sylib 127 . . . . . . 7 (𝜑 → ∀𝑦𝐵 (𝑂 + 𝑦) = 𝑦)
2423adantr 261 . . . . . 6 ((𝜑𝜓) → ∀𝑦𝐵 (𝑂 + 𝑦) = 𝑦)
25 oveq2 5520 . . . . . . . 8 (𝑦 = 𝑁 → (𝑂 + 𝑦) = (𝑂 + 𝑁))
26 id 19 . . . . . . . 8 (𝑦 = 𝑁𝑦 = 𝑁)
2725, 26eqeq12d 2054 . . . . . . 7 (𝑦 = 𝑁 → ((𝑂 + 𝑦) = 𝑦 ↔ (𝑂 + 𝑁) = 𝑁))
2827rspcv 2652 . . . . . 6 (𝑁𝐵 → (∀𝑦𝐵 (𝑂 + 𝑦) = 𝑦 → (𝑂 + 𝑁) = 𝑁))
2910, 24, 28sylc 56 . . . . 5 ((𝜑𝜓) → (𝑂 + 𝑁) = 𝑁)
3016, 17, 293eqtr3d 2080 . . . 4 ((𝜑𝜓) → (𝑁 + (𝑋 + 𝑁)) = 𝑁)
3130oveq2d 5528 . . 3 ((𝜑𝜓) → (𝑋 + (𝑁 + (𝑋 + 𝑁))) = (𝑋 + 𝑁))
3214, 31eqtrd 2072 . 2 ((𝜑𝜓) → ((𝑋 + 𝑁) + (𝑋 + 𝑁)) = (𝑋 + 𝑁))
331, 2, 3, 4, 5, 11, 32grprinvlem 5695 1 ((𝜑𝜓) → (𝑋 + 𝑁) = 𝑂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885   = wceq 1243  wcel 1393  wral 2306  wrex 2307  (class class class)co 5512
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515
This theorem is referenced by:  grpridd  5697
  Copyright terms: Public domain W3C validator