Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isomnd Structured version   Visualization version   GIF version

Theorem isomnd 29510
 Description: A (left) ordered monoid is a monoid with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 30-Jan-2018.)
Hypotheses
Ref Expression
isomnd.0 𝐵 = (Base‘𝑀)
isomnd.1 + = (+g𝑀)
isomnd.2 = (le‘𝑀)
Assertion
Ref Expression
isomnd (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐))))
Distinct variable groups:   𝑎,𝑏,𝑐,𝐵   𝑀,𝑎,𝑏,𝑐
Allowed substitution hints:   + (𝑎,𝑏,𝑐)   (𝑎,𝑏,𝑐)

Proof of Theorem isomnd
Dummy variables 𝑙 𝑚 𝑝 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6163 . . . . . 6 (Base‘𝑚) ∈ V
21a1i 11 . . . . 5 (𝑚 = 𝑀 → (Base‘𝑚) ∈ V)
3 simpr 477 . . . . . . . . . . 11 ((𝑚 = 𝑀𝑣 = (Base‘𝑚)) → 𝑣 = (Base‘𝑚))
4 fveq2 6153 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀))
54adantr 481 . . . . . . . . . . 11 ((𝑚 = 𝑀𝑣 = (Base‘𝑚)) → (Base‘𝑚) = (Base‘𝑀))
63, 5eqtrd 2655 . . . . . . . . . 10 ((𝑚 = 𝑀𝑣 = (Base‘𝑚)) → 𝑣 = (Base‘𝑀))
7 isomnd.0 . . . . . . . . . 10 𝐵 = (Base‘𝑀)
86, 7syl6eqr 2673 . . . . . . . . 9 ((𝑚 = 𝑀𝑣 = (Base‘𝑚)) → 𝑣 = 𝐵)
9 raleq 3130 . . . . . . . . . . 11 (𝑣 = 𝐵 → (∀𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)) ↔ ∀𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))))
109raleqbi1dv 3138 . . . . . . . . . 10 (𝑣 = 𝐵 → (∀𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)) ↔ ∀𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))))
1110raleqbi1dv 3138 . . . . . . . . 9 (𝑣 = 𝐵 → (∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)) ↔ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))))
128, 11syl 17 . . . . . . . 8 ((𝑚 = 𝑀𝑣 = (Base‘𝑚)) → (∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)) ↔ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))))
1312anbi2d 739 . . . . . . 7 ((𝑚 = 𝑀𝑣 = (Base‘𝑚)) → ((𝑚 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))) ↔ (𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))))
1413sbcbidv 3476 . . . . . 6 ((𝑚 = 𝑀𝑣 = (Base‘𝑚)) → ([(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))) ↔ [(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))))
1514sbcbidv 3476 . . . . 5 ((𝑚 = 𝑀𝑣 = (Base‘𝑚)) → ([(+g𝑚) / 𝑝][(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))) ↔ [(+g𝑚) / 𝑝][(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))))
162, 15sbcied 3458 . . . 4 (𝑚 = 𝑀 → ([(Base‘𝑚) / 𝑣][(+g𝑚) / 𝑝][(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))) ↔ [(+g𝑚) / 𝑝][(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))))
17 fvex 6163 . . . . . 6 (+g𝑚) ∈ V
1817a1i 11 . . . . 5 (𝑚 = 𝑀 → (+g𝑚) ∈ V)
19 simpr 477 . . . . . . . . . . . . . 14 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → 𝑝 = (+g𝑚))
20 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑚 = 𝑀 → (+g𝑚) = (+g𝑀))
2120adantr 481 . . . . . . . . . . . . . 14 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → (+g𝑚) = (+g𝑀))
2219, 21eqtrd 2655 . . . . . . . . . . . . 13 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → 𝑝 = (+g𝑀))
23 isomnd.1 . . . . . . . . . . . . 13 + = (+g𝑀)
2422, 23syl6eqr 2673 . . . . . . . . . . . 12 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → 𝑝 = + )
2524oveqd 6627 . . . . . . . . . . 11 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → (𝑎𝑝𝑐) = (𝑎 + 𝑐))
2624oveqd 6627 . . . . . . . . . . 11 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → (𝑏𝑝𝑐) = (𝑏 + 𝑐))
2725, 26breq12d 4631 . . . . . . . . . 10 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → ((𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐) ↔ (𝑎 + 𝑐)𝑙(𝑏 + 𝑐)))
2827imbi2d 330 . . . . . . . . 9 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → ((𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)) ↔ (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐))))
2928ralbidv 2981 . . . . . . . 8 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → (∀𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)) ↔ ∀𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐))))
30292ralbidv 2984 . . . . . . 7 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → (∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)) ↔ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐))))
3130anbi2d 739 . . . . . 6 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → ((𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))) ↔ (𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐)))))
3231sbcbidv 3476 . . . . 5 ((𝑚 = 𝑀𝑝 = (+g𝑚)) → ([(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))) ↔ [(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐)))))
3318, 32sbcied 3458 . . . 4 (𝑚 = 𝑀 → ([(+g𝑚) / 𝑝][(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))) ↔ [(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐)))))
34 fvex 6163 . . . . . . 7 (le‘𝑚) ∈ V
3534a1i 11 . . . . . 6 (𝑚 = 𝑀 → (le‘𝑚) ∈ V)
36 simpr 477 . . . . . . . . . . . . 13 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → 𝑙 = (le‘𝑚))
37 simpl 473 . . . . . . . . . . . . . 14 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → 𝑚 = 𝑀)
3837fveq2d 6157 . . . . . . . . . . . . 13 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → (le‘𝑚) = (le‘𝑀))
3936, 38eqtrd 2655 . . . . . . . . . . . 12 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → 𝑙 = (le‘𝑀))
40 isomnd.2 . . . . . . . . . . . 12 = (le‘𝑀)
4139, 40syl6eqr 2673 . . . . . . . . . . 11 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → 𝑙 = )
4241breqd 4629 . . . . . . . . . 10 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → (𝑎𝑙𝑏𝑎 𝑏))
4341breqd 4629 . . . . . . . . . 10 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → ((𝑎 + 𝑐)𝑙(𝑏 + 𝑐) ↔ (𝑎 + 𝑐) (𝑏 + 𝑐)))
4442, 43imbi12d 334 . . . . . . . . 9 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → ((𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐)) ↔ (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐))))
4544ralbidv 2981 . . . . . . . 8 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → (∀𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐)) ↔ ∀𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐))))
46452ralbidv 2984 . . . . . . 7 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → (∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐)) ↔ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐))))
4746anbi2d 739 . . . . . 6 ((𝑚 = 𝑀𝑙 = (le‘𝑚)) → ((𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐))) ↔ (𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐)))))
4835, 47sbcied 3458 . . . . 5 (𝑚 = 𝑀 → ([(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐))) ↔ (𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐)))))
49 eleq1 2686 . . . . . 6 (𝑚 = 𝑀 → (𝑚 ∈ Toset ↔ 𝑀 ∈ Toset))
5049anbi1d 740 . . . . 5 (𝑚 = 𝑀 → ((𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐))) ↔ (𝑀 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐)))))
5148, 50bitrd 268 . . . 4 (𝑚 = 𝑀 → ([(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎𝑙𝑏 → (𝑎 + 𝑐)𝑙(𝑏 + 𝑐))) ↔ (𝑀 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐)))))
5216, 33, 513bitrd 294 . . 3 (𝑚 = 𝑀 → ([(Base‘𝑚) / 𝑣][(+g𝑚) / 𝑝][(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))) ↔ (𝑀 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐)))))
53 df-omnd 29508 . . 3 oMnd = {𝑚 ∈ Mnd ∣ [(Base‘𝑚) / 𝑣][(+g𝑚) / 𝑝][(le‘𝑚) / 𝑙](𝑚 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))}
5452, 53elrab2 3352 . 2 (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ (𝑀 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐)))))
55 3anass 1040 . 2 ((𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐))) ↔ (𝑀 ∈ Mnd ∧ (𝑀 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐)))))
5654, 55bitr4i 267 1 (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀𝑎𝐵𝑏𝐵𝑐𝐵 (𝑎 𝑏 → (𝑎 + 𝑐) (𝑏 + 𝑐))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ∀wral 2907  Vcvv 3189  [wsbc 3421   class class class wbr 4618  ‘cfv 5852  (class class class)co 6610  Basecbs 15792  +gcplusg 15873  lecple 15880  Tosetctos 16965  Mndcmnd 17226  oMndcomnd 29506 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4754 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860  df-ov 6613  df-omnd 29508 This theorem is referenced by:  omndmnd  29513  omndtos  29514  omndadd  29515  submomnd  29519  xrge0omnd  29520  reofld  29649
 Copyright terms: Public domain W3C validator