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 35382
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 4766 . . . . . 6 (𝑔 = (1st𝑅) → ⟨𝑔, ⟩ = ⟨(1st𝑅), ⟩)
21eleq1d 2877 . . . . 5 (𝑔 = (1st𝑅) → (⟨𝑔, ⟩ ∈ RingOps ↔ ⟨(1st𝑅), ⟩ ∈ RingOps))
3 id 22 . . . . . . . . . . . 12 (𝑔 = (1st𝑅) → 𝑔 = (1st𝑅))
4 drngi.1 . . . . . . . . . . . 12 𝐺 = (1st𝑅)
53, 4eqtr4di 2854 . . . . . . . . . . 11 (𝑔 = (1st𝑅) → 𝑔 = 𝐺)
65rneqd 5776 . . . . . . . . . 10 (𝑔 = (1st𝑅) → ran 𝑔 = ran 𝐺)
7 drngi.3 . . . . . . . . . 10 𝑋 = ran 𝐺
86, 7eqtr4di 2854 . . . . . . . . 9 (𝑔 = (1st𝑅) → ran 𝑔 = 𝑋)
95fveq2d 6653 . . . . . . . . . . 11 (𝑔 = (1st𝑅) → (GId‘𝑔) = (GId‘𝐺))
10 drngi.4 . . . . . . . . . . 11 𝑍 = (GId‘𝐺)
119, 10eqtr4di 2854 . . . . . . . . . 10 (𝑔 = (1st𝑅) → (GId‘𝑔) = 𝑍)
1211sneqd 4540 . . . . . . . . 9 (𝑔 = (1st𝑅) → {(GId‘𝑔)} = {𝑍})
138, 12difeq12d 4054 . . . . . . . 8 (𝑔 = (1st𝑅) → (ran 𝑔 ∖ {(GId‘𝑔)}) = (𝑋 ∖ {𝑍}))
1413sqxpeqd 5555 . . . . . . 7 (𝑔 = (1st𝑅) → ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
1514reseq2d 5822 . . . . . 6 (𝑔 = (1st𝑅) → ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) = ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
1615eleq1d 2877 . . . . 5 (𝑔 = (1st𝑅) → (( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp ↔ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
172, 16anbi12d 633 . . . 4 (𝑔 = (1st𝑅) → ((⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp) ↔ (⟨(1st𝑅), ⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
18 opeq2 4768 . . . . . . 7 ( = (2nd𝑅) → ⟨(1st𝑅), ⟩ = ⟨(1st𝑅), (2nd𝑅)⟩)
1918eleq1d 2877 . . . . . 6 ( = (2nd𝑅) → (⟨(1st𝑅), ⟩ ∈ RingOps ↔ ⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps))
2019anbi1d 632 . . . . 5 ( = (2nd𝑅) → ((⟨(1st𝑅), ⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
21 drngi.2 . . . . . . . . 9 𝐻 = (2nd𝑅)
22 id 22 . . . . . . . . 9 ( = (2nd𝑅) → = (2nd𝑅))
2321, 22eqtr4id 2855 . . . . . . . 8 ( = (2nd𝑅) → 𝐻 = )
2423reseq1d 5821 . . . . . . 7 ( = (2nd𝑅) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
2524eleq1d 2877 . . . . . 6 ( = (2nd𝑅) → ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ↔ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
2625anbi2d 631 . . . . 5 ( = (2nd𝑅) → ((⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
2720, 26bitr4d 285 . . . 4 ( = (2nd𝑅) → ((⟨(1st𝑅), ⟩ ∈ RingOps ∧ ( ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
2817, 27elopabi 7746 . . 3 (𝑅 ∈ {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} → (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
29 df-drngo 35380 . . 3 DivRingOps = {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}
3028, 29eleq2s 2911 . 2 (𝑅 ∈ DivRingOps → (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
3129relopabi 5662 . . . . 5 Rel DivRingOps
32 1st2nd 7724 . . . . 5 ((Rel DivRingOps ∧ 𝑅 ∈ DivRingOps) → 𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩)
3331, 32mpan 689 . . . 4 (𝑅 ∈ DivRingOps → 𝑅 = ⟨(1st𝑅), (2nd𝑅)⟩)
3433eleq1d 2877 . . 3 (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ↔ ⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps))
3534anbi1d 632 . 2 (𝑅 ∈ DivRingOps → ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (⟨(1st𝑅), (2nd𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))
3630, 35mpbird 260 1 (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2112  cdif 3881  {csn 4528  cop 4534  {copab 5095   × cxp 5521  ran crn 5524  cres 5525  Rel wrel 5528  cfv 6328  1st c1st 7673  2nd c2nd 7674  GrpOpcgr 28275  GIdcgi 28276  RingOpscrngo 35325  DivRingOpscdrng 35379
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-iota 6287  df-fun 6330  df-fv 6336  df-1st 7675  df-2nd 7676  df-drngo 35380
This theorem is referenced by:  dvrunz  35385  fldcrng  35435
  Copyright terms: Public domain W3C validator