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

Theorem grprinvd 5638
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 ((φ x B y B) → (x + y) B)
grprinvlem.o (φ𝑂 B)
grprinvlem.i ((φ x B) → (𝑂 + x) = x)
grprinvlem.a ((φ (x B y B z B)) → ((x + y) + z) = (x + (y + z)))
grprinvlem.n ((φ x B) → y B (y + x) = 𝑂)
grprinvd.x ((φ ψ) → 𝑋 B)
grprinvd.n ((φ ψ) → 𝑁 B)
grprinvd.e ((φ ψ) → (𝑁 + 𝑋) = 𝑂)
Assertion
Ref Expression
grprinvd ((φ ψ) → (𝑋 + 𝑁) = 𝑂)
Distinct variable groups:   x,y,z,B   x,𝑂,y,z   φ,x,y,z   y,𝑁,z   x, + ,y,z   y,𝑋,z   ψ,y
Allowed substitution hints:   ψ(x,z)   𝑁(x)   𝑋(x)

Proof of Theorem grprinvd
Dummy variables u v w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grprinvlem.c . 2 ((φ x B y B) → (x + y) B)
2 grprinvlem.o . 2 (φ𝑂 B)
3 grprinvlem.i . 2 ((φ x B) → (𝑂 + x) = x)
4 grprinvlem.a . 2 ((φ (x B y B z B)) → ((x + y) + z) = (x + (y + z)))
5 grprinvlem.n . 2 ((φ x B) → y B (y + x) = 𝑂)
613expb 1104 . . . . 5 ((φ (x B y B)) → (x + y) B)
76caovclg 5595 . . . 4 ((φ (u B v B)) → (u + v) B)
87adantlr 446 . . 3 (((φ ψ) (u B v B)) → (u + v) B)
9 grprinvd.x . . 3 ((φ ψ) → 𝑋 B)
10 grprinvd.n . . 3 ((φ ψ) → 𝑁 B)
118, 9, 10caovcld 5596 . 2 ((φ ψ) → (𝑋 + 𝑁) B)
124caovassg 5601 . . . . 5 ((φ (u B v B w B)) → ((u + v) + w) = (u + (v + w)))
1312adantlr 446 . . . 4 (((φ ψ) (u B v B w B)) → ((u + v) + w) = (u + (v + w)))
1413, 9, 10, 11caovassd 5602 . . 3 ((φ ψ) → ((𝑋 + 𝑁) + (𝑋 + 𝑁)) = (𝑋 + (𝑁 + (𝑋 + 𝑁))))
15 grprinvd.e . . . . . 6 ((φ ψ) → (𝑁 + 𝑋) = 𝑂)
1615oveq1d 5470 . . . . 5 ((φ ψ) → ((𝑁 + 𝑋) + 𝑁) = (𝑂 + 𝑁))
1713, 10, 9, 10caovassd 5602 . . . . 5 ((φ ψ) → ((𝑁 + 𝑋) + 𝑁) = (𝑁 + (𝑋 + 𝑁)))
183ralrimiva 2386 . . . . . . . 8 (φx B (𝑂 + x) = x)
19 oveq2 5463 . . . . . . . . . 10 (x = y → (𝑂 + x) = (𝑂 + y))
20 id 19 . . . . . . . . . 10 (x = yx = y)
2119, 20eqeq12d 2051 . . . . . . . . 9 (x = y → ((𝑂 + x) = x ↔ (𝑂 + y) = y))
2221cbvralv 2527 . . . . . . . 8 (x B (𝑂 + x) = xy B (𝑂 + y) = y)
2318, 22sylib 127 . . . . . . 7 (φy B (𝑂 + y) = y)
2423adantr 261 . . . . . 6 ((φ ψ) → y B (𝑂 + y) = y)
25 oveq2 5463 . . . . . . . 8 (y = 𝑁 → (𝑂 + y) = (𝑂 + 𝑁))
26 id 19 . . . . . . . 8 (y = 𝑁y = 𝑁)
2725, 26eqeq12d 2051 . . . . . . 7 (y = 𝑁 → ((𝑂 + y) = y ↔ (𝑂 + 𝑁) = 𝑁))
2827rspcv 2646 . . . . . 6 (𝑁 B → (y B (𝑂 + y) = y → (𝑂 + 𝑁) = 𝑁))
2910, 24, 28sylc 56 . . . . 5 ((φ ψ) → (𝑂 + 𝑁) = 𝑁)
3016, 17, 293eqtr3d 2077 . . . 4 ((φ ψ) → (𝑁 + (𝑋 + 𝑁)) = 𝑁)
3130oveq2d 5471 . . 3 ((φ ψ) → (𝑋 + (𝑁 + (𝑋 + 𝑁))) = (𝑋 + 𝑁))
3214, 31eqtrd 2069 . 2 ((φ ψ) → ((𝑋 + 𝑁) + (𝑋 + 𝑁)) = (𝑋 + 𝑁))
331, 2, 3, 4, 5, 11, 32grprinvlem 5637 1 ((φ ψ) → (𝑋 + 𝑁) = 𝑂)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884   = wceq 1242   wcel 1390  wral 2300  wrex 2301  (class class class)co 5455
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458
This theorem is referenced by:  grpridd  5639
  Copyright terms: Public domain W3C validator