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

Theorem iscrngo2 34833
Description: The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.)
Hypotheses
Ref Expression
iscring2.1 𝐺 = (1st𝑅)
iscring2.2 𝐻 = (2nd𝑅)
iscring2.3 𝑋 = ran 𝐺
Assertion
Ref Expression
iscrngo2 (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
Distinct variable groups:   𝑥,𝑅,𝑦   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐺(𝑥,𝑦)   𝐻(𝑥,𝑦)

Proof of Theorem iscrngo2
StepHypRef Expression
1 iscrngo 34832 . 2 (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2))
2 relrngo 34732 . . . . 5 Rel RingOps
3 1st2nd 7599 . . . . 5 ((Rel RingOps ∧ 𝑅 ∈ RingOps) → 𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩)
42, 3mpan 686 . . . 4 (𝑅 ∈ RingOps → 𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩)
5 eleq1 2870 . . . . 5 (𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩ → (𝑅 ∈ Com2 ↔ ⟨(1st𝑅), (2nd𝑅)⟩ ∈ Com2))
6 iscring2.3 . . . . . . . 8 𝑋 = ran 𝐺
7 iscring2.1 . . . . . . . . 9 𝐺 = (1st𝑅)
87rneqi 5694 . . . . . . . 8 ran 𝐺 = ran (1st𝑅)
96, 8eqtri 2819 . . . . . . 7 𝑋 = ran (1st𝑅)
109raleqi 3373 . . . . . 6 (∀𝑥𝑋𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥) ↔ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥))
11 iscring2.2 . . . . . . . . . 10 𝐻 = (2nd𝑅)
1211oveqi 7034 . . . . . . . . 9 (𝑥𝐻𝑦) = (𝑥(2nd𝑅)𝑦)
1311oveqi 7034 . . . . . . . . 9 (𝑦𝐻𝑥) = (𝑦(2nd𝑅)𝑥)
1412, 13eqeq12i 2809 . . . . . . . 8 ((𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ (𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥))
159, 14raleqbii 3198 . . . . . . 7 (∀𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ ∀𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥))
1615ralbii 3132 . . . . . 6 (∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ ∀𝑥𝑋𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥))
17 fvex 6556 . . . . . . 7 (1st𝑅) ∈ V
18 fvex 6556 . . . . . . 7 (2nd𝑅) ∈ V
19 iscom2 34831 . . . . . . 7 (((1st𝑅) ∈ V ∧ (2nd𝑅) ∈ V) → (⟨(1st𝑅), (2nd𝑅)⟩ ∈ Com2 ↔ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥)))
2017, 18, 19mp2an 688 . . . . . 6 (⟨(1st𝑅), (2nd𝑅)⟩ ∈ Com2 ↔ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥))
2110, 16, 203bitr4ri 305 . . . . 5 (⟨(1st𝑅), (2nd𝑅)⟩ ∈ Com2 ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))
225, 21syl6bb 288 . . . 4 (𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩ → (𝑅 ∈ Com2 ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
234, 22syl 17 . . 3 (𝑅 ∈ RingOps → (𝑅 ∈ Com2 ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
2423pm5.32i 575 . 2 ((𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2) ↔ (𝑅 ∈ RingOps ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
251, 24bitri 276 1 (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1522  wcel 2081  wral 3105  Vcvv 3437  cop 4482  ran crn 5449  Rel wrel 5453  cfv 6230  (class class class)co 7021  1st c1st 7548  2nd c2nd 7549  RingOpscrngo 34730  Com2ccm2 34825  CRingOpsccring 34829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-iota 6194  df-fun 6232  df-fv 6238  df-ov 7024  df-1st 7550  df-2nd 7551  df-rngo 34731  df-com2 34826  df-crngo 34830
This theorem is referenced by:  crngocom  34837  crngohomfo  34842
  Copyright terms: Public domain W3C validator