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

Theorem rngomndo 34221
Description: In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
Hypothesis
Ref Expression
unmnd.1 𝐻 = (2nd𝑅)
Assertion
Ref Expression
rngomndo (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)

Proof of Theorem rngomndo
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2799 . . . 4 (1st𝑅) = (1st𝑅)
2 unmnd.1 . . . 4 𝐻 = (2nd𝑅)
3 eqid 2799 . . . 4 ran (1st𝑅) = ran (1st𝑅)
41, 2, 3rngosm 34186 . . 3 (𝑅 ∈ RingOps → 𝐻:(ran (1st𝑅) × ran (1st𝑅))⟶ran (1st𝑅))
51, 2, 3rngoass 34192 . . . 4 ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)))
65ralrimivvva 3153 . . 3 (𝑅 ∈ RingOps → ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)∀𝑧 ∈ ran (1st𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)))
71, 2, 3rngoi 34185 . . . 4 (𝑅 ∈ RingOps → (((1st𝑅) ∈ AbelOp ∧ 𝐻:(ran (1st𝑅) × ran (1st𝑅))⟶ran (1st𝑅)) ∧ (∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)∀𝑧 ∈ ran (1st𝑅)(((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦(1st𝑅)𝑧)) = ((𝑥𝐻𝑦)(1st𝑅)(𝑥𝐻𝑧)) ∧ ((𝑥(1st𝑅)𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)(1st𝑅)(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))
87simprrd 791 . . 3 (𝑅 ∈ RingOps → ∃𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))
92, 1rngorn1 34219 . . . 4 (𝑅 ∈ RingOps → ran (1st𝑅) = dom dom 𝐻)
10 xpid11 5550 . . . . . . . 8 ((dom dom 𝐻 × dom dom 𝐻) = (ran (1st𝑅) × ran (1st𝑅)) ↔ dom dom 𝐻 = ran (1st𝑅))
1110biimpri 220 . . . . . . 7 (dom dom 𝐻 = ran (1st𝑅) → (dom dom 𝐻 × dom dom 𝐻) = (ran (1st𝑅) × ran (1st𝑅)))
12 feq23 6240 . . . . . . 7 (((dom dom 𝐻 × dom dom 𝐻) = (ran (1st𝑅) × ran (1st𝑅)) ∧ dom dom 𝐻 = ran (1st𝑅)) → (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻𝐻:(ran (1st𝑅) × ran (1st𝑅))⟶ran (1st𝑅)))
1311, 12mpancom 680 . . . . . 6 (dom dom 𝐻 = ran (1st𝑅) → (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻𝐻:(ran (1st𝑅) × ran (1st𝑅))⟶ran (1st𝑅)))
14 raleq 3321 . . . . . . . 8 (dom dom 𝐻 = ran (1st𝑅) → (∀𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ↔ ∀𝑧 ∈ ran (1st𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))))
1514raleqbi1dv 3329 . . . . . . 7 (dom dom 𝐻 = ran (1st𝑅) → (∀𝑦 ∈ dom dom 𝐻𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ↔ ∀𝑦 ∈ ran (1st𝑅)∀𝑧 ∈ ran (1st𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))))
1615raleqbi1dv 3329 . . . . . 6 (dom dom 𝐻 = ran (1st𝑅) → (∀𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ↔ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)∀𝑧 ∈ ran (1st𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))))
17 raleq 3321 . . . . . . 7 (dom dom 𝐻 = ran (1st𝑅) → (∀𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦) ↔ ∀𝑦 ∈ ran (1st𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))
1817rexeqbi1dv 3330 . . . . . 6 (dom dom 𝐻 = ran (1st𝑅) → (∃𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦) ↔ ∃𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))
1913, 16, 183anbi123d 1561 . . . . 5 (dom dom 𝐻 = ran (1st𝑅) → ((𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)) ↔ (𝐻:(ran (1st𝑅) × ran (1st𝑅))⟶ran (1st𝑅) ∧ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)∀𝑧 ∈ ran (1st𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))
2019eqcoms 2807 . . . 4 (ran (1st𝑅) = dom dom 𝐻 → ((𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)) ↔ (𝐻:(ran (1st𝑅) × ran (1st𝑅))⟶ran (1st𝑅) ∧ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)∀𝑧 ∈ ran (1st𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))
219, 20syl 17 . . 3 (𝑅 ∈ RingOps → ((𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)) ↔ (𝐻:(ran (1st𝑅) × ran (1st𝑅))⟶ran (1st𝑅) ∧ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)∀𝑧 ∈ ran (1st𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))
224, 6, 8, 21mpbir3and 1443 . 2 (𝑅 ∈ RingOps → (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))
23 fvex 6424 . . . 4 (2nd𝑅) ∈ V
24 eleq1 2866 . . . 4 (𝐻 = (2nd𝑅) → (𝐻 ∈ V ↔ (2nd𝑅) ∈ V))
2523, 24mpbiri 250 . . 3 (𝐻 = (2nd𝑅) → 𝐻 ∈ V)
26 eqid 2799 . . . 4 dom dom 𝐻 = dom dom 𝐻
2726ismndo1 34159 . . 3 (𝐻 ∈ V → (𝐻 ∈ MndOp ↔ (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))
282, 25, 27mp2b 10 . 2 (𝐻 ∈ MndOp ↔ (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))
2922, 28sylibr 226 1 (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  w3a 1108   = wceq 1653  wcel 2157  wral 3089  wrex 3090  Vcvv 3385   × cxp 5310  dom cdm 5312  ran crn 5313  wf 6097  cfv 6101  (class class class)co 6878  1st c1st 7399  2nd c2nd 7400  AbelOpcablo 27924  MndOpcmndo 34152  RingOpscrngo 34180
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097  ax-un 7183
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-iun 4712  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fo 6107  df-fv 6109  df-ov 6881  df-1st 7401  df-2nd 7402  df-grpo 27873  df-ablo 27925  df-ass 34129  df-exid 34131  df-mgmOLD 34135  df-sgrOLD 34147  df-mndo 34153  df-rngo 34181
This theorem is referenced by:  rngoidmlem  34222  rngo1cl  34225  isdrngo2  34244
  Copyright terms: Public domain W3C validator