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

Theorem drngoi 36814
Description: The properties of a division ring. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.)
Hypotheses
Ref Expression
drngi.1 𝐺 = (1st𝑅)
drngi.2 𝐻 = (2nd𝑅)
drngi.3 𝑋 = ran 𝐺
drngi.4 𝑍 = (GId‘𝐺)
Assertion
Ref Expression
drngoi (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))

Proof of Theorem drngoi
Dummy variables 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 4873 . . . . . 6 (𝑔 = (1st𝑅) → ⟨𝑔, ⟩ = ⟨(1st𝑅), ⟩)
21eleq1d 2818 . . . . 5 (𝑔 = (1st𝑅) → (⟨𝑔, ⟩ ∈ RingOps ↔ ⟨(1st𝑅), ⟩ ∈ RingOps))
3 id 22 . . . . . . . . . . . 12 (𝑔 = (1st𝑅) → 𝑔 = (1st𝑅))
4 drngi.1 . . . . . . . . . . . 12 𝐺 = (1st𝑅)
53, 4eqtr4di 2790 . . . . . . . . . . 11 (𝑔 = (1st𝑅) → 𝑔 = 𝐺)
65rneqd 5937 . . . . . . . . . 10 (𝑔 = (1st𝑅) → ran 𝑔 = ran 𝐺)
7 drngi.3 . . . . . . . . . 10 𝑋 = ran 𝐺
86, 7eqtr4di 2790 . . . . . . . . 9 (𝑔 = (1st𝑅) → ran 𝑔 = 𝑋)
95fveq2d 6895 . . . . . . . . . . 11 (𝑔 = (1st𝑅) → (GId‘𝑔) = (GId‘𝐺))
10 drngi.4 . . . . . . . . . . 11 𝑍 = (GId‘𝐺)
119, 10eqtr4di 2790 . . . . . . . . . 10 (𝑔 = (1st𝑅) → (GId‘𝑔) = 𝑍)
1211sneqd 4640 . . . . . . . . 9 (𝑔 = (1st𝑅) → {(GId‘𝑔)} = {𝑍})
138, 12difeq12d 4123 . . . . . . . 8 (𝑔 = (1st𝑅) → (ran 𝑔 ∖ {(GId‘𝑔)}) = (𝑋 ∖ {𝑍}))
1413sqxpeqd 5708 . . . . . . 7 (𝑔 = (1st𝑅) → ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
1514reseq2d 5981 . . . . . 6 (𝑔 = (1st𝑅) → ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) = ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
1615eleq1d 2818 . . . . 5 (𝑔 = (1st𝑅) → (( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp ↔ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
172, 16anbi12d 631 . . . 4 (𝑔 = (1st𝑅) → ((⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp) ↔ (⟨(1st𝑅), ⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
18 opeq2 4874 . . . . . . 7 ( = (2nd𝑅) → ⟨(1st𝑅), ⟩ = ⟨(1st𝑅), (2nd𝑅)⟩)
1918eleq1d 2818 . . . . . 6 ( = (2nd𝑅) → (⟨(1st𝑅), ⟩ ∈ RingOps ↔ ⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps))
2019anbi1d 630 . . . . 5 ( = (2nd𝑅) → ((⟨(1st𝑅), ⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
21 drngi.2 . . . . . . . . 9 𝐻 = (2nd𝑅)
22 id 22 . . . . . . . . 9 ( = (2nd𝑅) → = (2nd𝑅))
2321, 22eqtr4id 2791 . . . . . . . 8 ( = (2nd𝑅) → 𝐻 = )
2423reseq1d 5980 . . . . . . 7 ( = (2nd𝑅) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
2524eleq1d 2818 . . . . . 6 ( = (2nd𝑅) → ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ↔ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
2625anbi2d 629 . . . . 5 ( = (2nd𝑅) → ((⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
2720, 26bitr4d 281 . . . 4 ( = (2nd𝑅) → ((⟨(1st𝑅), ⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
2817, 27elopabi 8047 . . 3 (𝑅 ∈ {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} → (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
29 df-drngo 36812 . . 3 DivRingOps = {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}
3028, 29eleq2s 2851 . 2 (𝑅 ∈ DivRingOps → (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
3129relopabiv 5820 . . . . 5 Rel DivRingOps
32 1st2nd 8024 . . . . 5 ((Rel DivRingOps ∧ 𝑅 ∈ DivRingOps) → 𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩)
3331, 32mpan 688 . . . 4 (𝑅 ∈ DivRingOps → 𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩)
3433eleq1d 2818 . . 3 (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ↔ ⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps))
3534anbi1d 630 . 2 (𝑅 ∈ DivRingOps → ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
3630, 35mpbird 256 1 (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  cdif 3945  {csn 4628  cop 4634  {copab 5210   × cxp 5674  ran crn 5677  cres 5678  Rel wrel 5681  cfv 6543  1st c1st 7972  2nd c2nd 7973  GrpOpcgr 29737  GIdcgi 29738  RingOpscrngo 36757  DivRingOpscdrng 36811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-iota 6495  df-fun 6545  df-fv 6551  df-1st 7974  df-2nd 7975  df-drngo 36812
This theorem is referenced by:  dvrunz  36817  fldcrngo  36867
  Copyright terms: Public domain W3C validator