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

Theorem caovimo 5636
 Description: Uniqueness of inverse element in commutative, associative operation with identity. The identity element is B. (Contributed by Jim Kingdon, 18-Sep-2019.)
Hypotheses
Ref Expression
caovimo.idel B 𝑆
caovimo.com ((x 𝑆 y 𝑆) → (x𝐹y) = (y𝐹x))
caovimo.ass ((x 𝑆 y 𝑆 z 𝑆) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))
caovimo.id (x 𝑆 → (x𝐹B) = x)
Assertion
Ref Expression
caovimo (A 𝑆∃*w(w 𝑆 (A𝐹w) = B))
Distinct variable groups:   w,A,x,y,z   w,B,x,y   w,𝐹,x,y,z   w,𝑆,x,y,z
Allowed substitution hint:   B(z)

Proof of Theorem caovimo
Dummy variable v is distinct from all other variables.
StepHypRef Expression
1 oveq1 5462 . . . . . . 7 ((A𝐹w) = B → ((A𝐹w)𝐹v) = (B𝐹v))
21adantl 262 . . . . . 6 ((w 𝑆 (A𝐹w) = B) → ((A𝐹w)𝐹v) = (B𝐹v))
323ad2ant2 925 . . . . 5 ((A 𝑆 (w 𝑆 (A𝐹w) = B) (v 𝑆 (A𝐹v) = B)) → ((A𝐹w)𝐹v) = (B𝐹v))
4 df-3an 886 . . . . . . . . 9 ((A 𝑆 w 𝑆 v 𝑆) ↔ ((A 𝑆 w 𝑆) v 𝑆))
5 caovimo.ass . . . . . . . . . . . . . 14 ((x 𝑆 y 𝑆 z 𝑆) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))
65adantl 262 . . . . . . . . . . . . 13 (((A 𝑆 w 𝑆 v 𝑆) (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))
7 simp1 903 . . . . . . . . . . . . 13 ((A 𝑆 w 𝑆 v 𝑆) → A 𝑆)
8 simp2 904 . . . . . . . . . . . . 13 ((A 𝑆 w 𝑆 v 𝑆) → w 𝑆)
9 simp3 905 . . . . . . . . . . . . 13 ((A 𝑆 w 𝑆 v 𝑆) → v 𝑆)
106, 7, 8, 9caovassd 5602 . . . . . . . . . . . 12 ((A 𝑆 w 𝑆 v 𝑆) → ((A𝐹w)𝐹v) = (A𝐹(w𝐹v)))
11 caovimo.com . . . . . . . . . . . . . 14 ((x 𝑆 y 𝑆) → (x𝐹y) = (y𝐹x))
1211adantl 262 . . . . . . . . . . . . 13 (((A 𝑆 w 𝑆 v 𝑆) (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))
137, 8, 9, 12, 6caov12d 5624 . . . . . . . . . . . 12 ((A 𝑆 w 𝑆 v 𝑆) → (A𝐹(w𝐹v)) = (w𝐹(A𝐹v)))
1410, 13eqtrd 2069 . . . . . . . . . . 11 ((A 𝑆 w 𝑆 v 𝑆) → ((A𝐹w)𝐹v) = (w𝐹(A𝐹v)))
1514adantr 261 . . . . . . . . . 10 (((A 𝑆 w 𝑆 v 𝑆) (A𝐹v) = B) → ((A𝐹w)𝐹v) = (w𝐹(A𝐹v)))
16 oveq2 5463 . . . . . . . . . . . 12 ((A𝐹v) = B → (w𝐹(A𝐹v)) = (w𝐹B))
17 oveq1 5462 . . . . . . . . . . . . . 14 (x = w → (x𝐹B) = (w𝐹B))
18 id 19 . . . . . . . . . . . . . 14 (x = wx = w)
1917, 18eqeq12d 2051 . . . . . . . . . . . . 13 (x = w → ((x𝐹B) = x ↔ (w𝐹B) = w))
20 caovimo.id . . . . . . . . . . . . 13 (x 𝑆 → (x𝐹B) = x)
2119, 20vtoclga 2613 . . . . . . . . . . . 12 (w 𝑆 → (w𝐹B) = w)
2216, 21sylan9eqr 2091 . . . . . . . . . . 11 ((w 𝑆 (A𝐹v) = B) → (w𝐹(A𝐹v)) = w)
23223ad2antl2 1066 . . . . . . . . . 10 (((A 𝑆 w 𝑆 v 𝑆) (A𝐹v) = B) → (w𝐹(A𝐹v)) = w)
2415, 23eqtrd 2069 . . . . . . . . 9 (((A 𝑆 w 𝑆 v 𝑆) (A𝐹v) = B) → ((A𝐹w)𝐹v) = w)
254, 24sylanbr 269 . . . . . . . 8 ((((A 𝑆 w 𝑆) v 𝑆) (A𝐹v) = B) → ((A𝐹w)𝐹v) = w)
2625anasss 379 . . . . . . 7 (((A 𝑆 w 𝑆) (v 𝑆 (A𝐹v) = B)) → ((A𝐹w)𝐹v) = w)
27263impa 1098 . . . . . 6 ((A 𝑆 w 𝑆 (v 𝑆 (A𝐹v) = B)) → ((A𝐹w)𝐹v) = w)
28273adant2r 1129 . . . . 5 ((A 𝑆 (w 𝑆 (A𝐹w) = B) (v 𝑆 (A𝐹v) = B)) → ((A𝐹w)𝐹v) = w)
2911adantl 262 . . . . . . . . 9 ((v 𝑆 (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))
30 caovimo.idel . . . . . . . . . 10 B 𝑆
3130a1i 9 . . . . . . . . 9 (v 𝑆B 𝑆)
32 id 19 . . . . . . . . 9 (v 𝑆v 𝑆)
3329, 31, 32caovcomd 5599 . . . . . . . 8 (v 𝑆 → (B𝐹v) = (v𝐹B))
34 oveq1 5462 . . . . . . . . . 10 (x = v → (x𝐹B) = (v𝐹B))
35 id 19 . . . . . . . . . 10 (x = vx = v)
3634, 35eqeq12d 2051 . . . . . . . . 9 (x = v → ((x𝐹B) = x ↔ (v𝐹B) = v))
3736, 20vtoclga 2613 . . . . . . . 8 (v 𝑆 → (v𝐹B) = v)
3833, 37eqtrd 2069 . . . . . . 7 (v 𝑆 → (B𝐹v) = v)
3938adantr 261 . . . . . 6 ((v 𝑆 (A𝐹v) = B) → (B𝐹v) = v)
40393ad2ant3 926 . . . . 5 ((A 𝑆 (w 𝑆 (A𝐹w) = B) (v 𝑆 (A𝐹v) = B)) → (B𝐹v) = v)
413, 28, 403eqtr3d 2077 . . . 4 ((A 𝑆 (w 𝑆 (A𝐹w) = B) (v 𝑆 (A𝐹v) = B)) → w = v)
42413expib 1106 . . 3 (A 𝑆 → (((w 𝑆 (A𝐹w) = B) (v 𝑆 (A𝐹v) = B)) → w = v))
4342alrimivv 1752 . 2 (A 𝑆wv(((w 𝑆 (A𝐹w) = B) (v 𝑆 (A𝐹v) = B)) → w = v))
44 eleq1 2097 . . . 4 (w = v → (w 𝑆v 𝑆))
45 oveq2 5463 . . . . 5 (w = v → (A𝐹w) = (A𝐹v))
4645eqeq1d 2045 . . . 4 (w = v → ((A𝐹w) = B ↔ (A𝐹v) = B))
4744, 46anbi12d 442 . . 3 (w = v → ((w 𝑆 (A𝐹w) = B) ↔ (v 𝑆 (A𝐹v) = B)))
4847mo4 1958 . 2 (∃*w(w 𝑆 (A𝐹w) = B) ↔ wv(((w 𝑆 (A𝐹w) = B) (v 𝑆 (A𝐹v) = B)) → w = v))
4943, 48sylibr 137 1 (A 𝑆∃*w(w 𝑆 (A𝐹w) = B))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884  ∀wal 1240   = wceq 1242   ∈ wcel 1390  ∃*wmo 1898  (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-bndl 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-eu 1900  df-mo 1901  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:  recmulnqg  6375
 Copyright terms: Public domain W3C validator