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 37168
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 37167 . 2 (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2))
2 relrngo 37067 . . . . 5 Rel RingOps
3 1st2nd 8027 . . . . 5 ((Rel RingOps ∧ 𝑅 ∈ RingOps) → 𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩)
42, 3mpan 686 . . . 4 (𝑅 ∈ RingOps → 𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩)
5 eleq1 2819 . . . . 5 (𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩ → (𝑅 ∈ Com2 ↔ ⟨(1st𝑅), (2nd𝑅)⟩ ∈ Com2))
6 iscring2.3 . . . . . . . 8 𝑋 = ran 𝐺
7 iscring2.1 . . . . . . . . 9 𝐺 = (1st𝑅)
87rneqi 5935 . . . . . . . 8 ran 𝐺 = ran (1st𝑅)
96, 8eqtri 2758 . . . . . . 7 𝑋 = ran (1st𝑅)
109raleqi 3321 . . . . . 6 (∀𝑥𝑋𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥) ↔ ∀𝑥 ∈ ran (1st𝑅)∀𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥))
11 iscring2.2 . . . . . . . . . 10 𝐻 = (2nd𝑅)
1211oveqi 7424 . . . . . . . . 9 (𝑥𝐻𝑦) = (𝑥(2nd𝑅)𝑦)
1311oveqi 7424 . . . . . . . . 9 (𝑦𝐻𝑥) = (𝑦(2nd𝑅)𝑥)
1412, 13eqeq12i 2748 . . . . . . . 8 ((𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ (𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥))
159, 14raleqbii 3336 . . . . . . 7 (∀𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ ∀𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥))
1615ralbii 3091 . . . . . 6 (∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ ∀𝑥𝑋𝑦 ∈ ran (1st𝑅)(𝑥(2nd𝑅)𝑦) = (𝑦(2nd𝑅)𝑥))
17 fvex 6903 . . . . . . 7 (1st𝑅) ∈ V
18 fvex 6903 . . . . . . 7 (2nd𝑅) ∈ V
19 iscom2 37166 . . . . . . 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 303 . . . . 5 (⟨(1st𝑅), (2nd𝑅)⟩ ∈ Com2 ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))
225, 21bitrdi 286 . . . 4 (𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩ → (𝑅 ∈ Com2 ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
234, 22syl 17 . . 3 (𝑅 ∈ RingOps → (𝑅 ∈ Com2 ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
2423pm5.32i 573 . 2 ((𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2) ↔ (𝑅 ∈ RingOps ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
251, 24bitri 274 1 (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394   = wceq 1539  wcel 2104  wral 3059  Vcvv 3472  cop 4633  ran crn 5676  Rel wrel 5680  cfv 6542  (class class class)co 7411  1st c1st 7975  2nd c2nd 7976  RingOpscrngo 37065  Com2ccm2 37160  CRingOpsccring 37164
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6494  df-fun 6544  df-fv 6550  df-ov 7414  df-1st 7977  df-2nd 7978  df-rngo 37066  df-com2 37161  df-crngo 37165
This theorem is referenced by:  crngocom  37172  crngohomfo  37177
  Copyright terms: Public domain W3C validator