Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isass Structured version   Visualization version   GIF version

Theorem isass 33927
 Description: The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
Hypothesis
Ref Expression
isass.1 𝑋 = dom dom 𝐺
Assertion
Ref Expression
isass (𝐺𝐴 → (𝐺 ∈ Ass ↔ ∀𝑥𝑋𝑦𝑋𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
Distinct variable groups:   𝑥,𝐺,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧)

Proof of Theorem isass
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 dmeq 5467 . . . . . . . . . 10 (𝑔 = 𝐺 → dom 𝑔 = dom 𝐺)
21dmeqd 5469 . . . . . . . . 9 (𝑔 = 𝐺 → dom dom 𝑔 = dom dom 𝐺)
32eleq2d 2813 . . . . . . . 8 (𝑔 = 𝐺 → (𝑥 ∈ dom dom 𝑔𝑥 ∈ dom dom 𝐺))
42eleq2d 2813 . . . . . . . 8 (𝑔 = 𝐺 → (𝑦 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝐺))
52eleq2d 2813 . . . . . . . 8 (𝑔 = 𝐺 → (𝑧 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝐺))
63, 4, 53anbi123d 1536 . . . . . . 7 (𝑔 = 𝐺 → ((𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔) ↔ (𝑥 ∈ dom dom 𝐺𝑦 ∈ dom dom 𝐺𝑧 ∈ dom dom 𝐺)))
7 oveq 6807 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
87oveq1d 6816 . . . . . . . . 9 (𝑔 = 𝐺 → ((𝑥𝑔𝑦)𝑔𝑧) = ((𝑥𝐺𝑦)𝑔𝑧))
9 oveq 6807 . . . . . . . . 9 (𝑔 = 𝐺 → ((𝑥𝐺𝑦)𝑔𝑧) = ((𝑥𝐺𝑦)𝐺𝑧))
108, 9eqtrd 2782 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑥𝑔𝑦)𝑔𝑧) = ((𝑥𝐺𝑦)𝐺𝑧))
11 oveq 6807 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑦𝑔𝑧) = (𝑦𝐺𝑧))
1211oveq2d 6817 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑥𝑔(𝑦𝑔𝑧)) = (𝑥𝑔(𝑦𝐺𝑧)))
13 oveq 6807 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑥𝑔(𝑦𝐺𝑧)) = (𝑥𝐺(𝑦𝐺𝑧)))
1412, 13eqtrd 2782 . . . . . . . 8 (𝑔 = 𝐺 → (𝑥𝑔(𝑦𝑔𝑧)) = (𝑥𝐺(𝑦𝐺𝑧)))
1510, 14eqeq12d 2763 . . . . . . 7 (𝑔 = 𝐺 → (((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
166, 15imbi12d 333 . . . . . 6 (𝑔 = 𝐺 → (((𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔) → ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))) ↔ ((𝑥 ∈ dom dom 𝐺𝑦 ∈ dom dom 𝐺𝑧 ∈ dom dom 𝐺) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))))
1716albidv 1986 . . . . 5 (𝑔 = 𝐺 → (∀𝑧((𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔) → ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))) ↔ ∀𝑧((𝑥 ∈ dom dom 𝐺𝑦 ∈ dom dom 𝐺𝑧 ∈ dom dom 𝐺) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))))
18172albidv 1988 . . . 4 (𝑔 = 𝐺 → (∀𝑥𝑦𝑧((𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔) → ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))) ↔ ∀𝑥𝑦𝑧((𝑥 ∈ dom dom 𝐺𝑦 ∈ dom dom 𝐺𝑧 ∈ dom dom 𝐺) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))))
19 r3al 3066 . . . 4 (∀𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ∀𝑥𝑦𝑧((𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔) → ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))))
20 r3al 3066 . . . 4 (∀𝑥 ∈ dom dom 𝐺𝑦 ∈ dom dom 𝐺𝑧 ∈ dom dom 𝐺((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑥𝑦𝑧((𝑥 ∈ dom dom 𝐺𝑦 ∈ dom dom 𝐺𝑧 ∈ dom dom 𝐺) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
2118, 19, 203bitr4g 303 . . 3 (𝑔 = 𝐺 → (∀𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ∀𝑥 ∈ dom dom 𝐺𝑦 ∈ dom dom 𝐺𝑧 ∈ dom dom 𝐺((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
22 isass.1 . . . . . 6 𝑋 = dom dom 𝐺
2322eqcomi 2757 . . . . 5 dom dom 𝐺 = 𝑋
2423a1i 11 . . . 4 (𝑔 = 𝐺 → dom dom 𝐺 = 𝑋)
2524raleqdv 3271 . . . 4 (𝑔 = 𝐺 → (∀𝑦 ∈ dom dom 𝐺𝑧 ∈ dom dom 𝐺((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑦𝑋𝑧 ∈ dom dom 𝐺((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
2624, 25raleqbidv 3279 . . 3 (𝑔 = 𝐺 → (∀𝑥 ∈ dom dom 𝐺𝑦 ∈ dom dom 𝐺𝑧 ∈ dom dom 𝐺((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑥𝑋𝑦𝑋𝑧 ∈ dom dom 𝐺((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
2724raleqdv 3271 . . . 4 (𝑔 = 𝐺 → (∀𝑧 ∈ dom dom 𝐺((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
28272ralbidv 3115 . . 3 (𝑔 = 𝐺 → (∀𝑥𝑋𝑦𝑋𝑧 ∈ dom dom 𝐺((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑥𝑋𝑦𝑋𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
2921, 26, 283bitrd 294 . 2 (𝑔 = 𝐺 → (∀𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ∀𝑥𝑋𝑦𝑋𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
30 df-ass 33924 . 2 Ass = {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}
3129, 30elab2g 3481 1 (𝐺𝐴 → (𝐺 ∈ Ass ↔ ∀𝑥𝑋𝑦𝑋𝑧𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1072  ∀wal 1618   = wceq 1620   ∈ wcel 2127  ∀wral 3038  dom cdm 5254  (class class class)co 6801  Asscass 33923 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-dm 5264  df-iota 6000  df-fv 6045  df-ov 6804  df-ass 33924 This theorem is referenced by:  issmgrpOLD  33944
 Copyright terms: Public domain W3C validator