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.

Step	Hyp	Ref	Expression
1		oveq1 5462	. . . . . . 7 ⊢ ((A𝐹w) = B → ((A𝐹w)𝐹v) = (B𝐹v))
2	1	adantl 262	. . . . . 6 ⊢ ((w ∈ 𝑆 ∧ (A𝐹w) = B) → ((A𝐹w)𝐹v) = (B𝐹v))
3	2	3ad2ant2 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)))
6	5	adantl 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 ∈ 𝑆)
10	6, 7, 8, 9	caovassd 5602	. . . . . . . . . . . 12 ⊢ ((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) → ((A𝐹w)𝐹v) = (A𝐹(w𝐹v)))
11		caovimo.com	. . . . . . . . . . . . . 14 ⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → (x𝐹y) = (y𝐹x))
12	11	adantl 262	. . . . . . . . . . . . 13 ⊢ (((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))
13	7, 8, 9, 12, 6	caov12d 5624	. . . . . . . . . . . 12 ⊢ ((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) → (A𝐹(w𝐹v)) = (w𝐹(A𝐹v)))
14	10, 13	eqtrd 2069	. . . . . . . . . . 11 ⊢ ((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) → ((A𝐹w)𝐹v) = (w𝐹(A𝐹v)))
15	14	adantr 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 = w → x = w)
19	17, 18	eqeq12d 2051	. . . . . . . . . . . . 13 ⊢ (x = w → ((x𝐹B) = x ↔ (w𝐹B) = w))
20		caovimo.id	. . . . . . . . . . . . 13 ⊢ (x ∈ 𝑆 → (x𝐹B) = x)
21	19, 20	vtoclga 2613	. . . . . . . . . . . 12 ⊢ (w ∈ 𝑆 → (w𝐹B) = w)
22	16, 21	sylan9eqr 2091	. . . . . . . . . . 11 ⊢ ((w ∈ 𝑆 ∧ (A𝐹v) = B) → (w𝐹(A𝐹v)) = w)
23	22	3ad2antl2 1066	. . . . . . . . . 10 ⊢ (((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) ∧ (A𝐹v) = B) → (w𝐹(A𝐹v)) = w)
24	15, 23	eqtrd 2069	. . . . . . . . 9 ⊢ (((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) ∧ (A𝐹v) = B) → ((A𝐹w)𝐹v) = w)
25	4, 24	sylanbr 269	. . . . . . . 8 ⊢ ((((A ∈ 𝑆 ∧ w ∈ 𝑆) ∧ v ∈ 𝑆) ∧ (A𝐹v) = B) → ((A𝐹w)𝐹v) = w)
26	25	anasss 379	. . . . . . 7 ⊢ (((A ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ (A𝐹v) = B)) → ((A𝐹w)𝐹v) = w)
27	26	3impa 1098	. . . . . 6 ⊢ ((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ (v ∈ 𝑆 ∧ (A𝐹v) = B)) → ((A𝐹w)𝐹v) = w)
28	27	3adant2r 1129	. . . . 5 ⊢ ((A ∈ 𝑆 ∧ (w ∈ 𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧ (A𝐹v) = B)) → ((A𝐹w)𝐹v) = w)
29	11	adantl 262	. . . . . . . . 9 ⊢ ((v ∈ 𝑆 ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))
30		caovimo.idel	. . . . . . . . . 10 ⊢ B ∈ 𝑆
31	30	a1i 9	. . . . . . . . 9 ⊢ (v ∈ 𝑆 → B ∈ 𝑆)
32		id 19	. . . . . . . . 9 ⊢ (v ∈ 𝑆 → v ∈ 𝑆)
33	29, 31, 32	caovcomd 5599	. . . . . . . 8 ⊢ (v ∈ 𝑆 → (B𝐹v) = (v𝐹B))
34		oveq1 5462	. . . . . . . . . 10 ⊢ (x = v → (x𝐹B) = (v𝐹B))
35		id 19	. . . . . . . . . 10 ⊢ (x = v → x = v)
36	34, 35	eqeq12d 2051	. . . . . . . . 9 ⊢ (x = v → ((x𝐹B) = x ↔ (v𝐹B) = v))
37	36, 20	vtoclga 2613	. . . . . . . 8 ⊢ (v ∈ 𝑆 → (v𝐹B) = v)
38	33, 37	eqtrd 2069	. . . . . . 7 ⊢ (v ∈ 𝑆 → (B𝐹v) = v)
39	38	adantr 261	. . . . . 6 ⊢ ((v ∈ 𝑆 ∧ (A𝐹v) = B) → (B𝐹v) = v)
40	39	3ad2ant3 926	. . . . 5 ⊢ ((A ∈ 𝑆 ∧ (w ∈ 𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧ (A𝐹v) = B)) → (B𝐹v) = v)
41	3, 28, 40	3eqtr3d 2077	. . . 4 ⊢ ((A ∈ 𝑆 ∧ (w ∈ 𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧ (A𝐹v) = B)) → w = v)
42	41	3expib 1106	. . 3 ⊢ (A ∈ 𝑆 → (((w ∈ 𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧ (A𝐹v) = B)) → w = v))
43	42	alrimivv 1752	. 2 ⊢ (A ∈ 𝑆 → ∀w∀v(((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))
46	45	eqeq1d 2045	. . . 4 ⊢ (w = v → ((A𝐹w) = B ↔ (A𝐹v) = B))
47	44, 46	anbi12d 442	. . 3 ⊢ (w = v → ((w ∈ 𝑆 ∧ (A𝐹w) = B) ↔ (v ∈ 𝑆 ∧ (A𝐹v) = B)))
48	47	mo4 1958	. 2 ⊢ (∃*w(w ∈ 𝑆 ∧ (A𝐹w) = B) ↔ ∀w∀v(((w ∈ 𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧ (A𝐹v) = B)) → w = v))
49	43, 48	sylibr 137	1 ⊢ (A ∈ 𝑆 → ∃*w(w ∈ 𝑆 ∧ (A𝐹w) = B))

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-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-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