Theorem issdrg 20865

Description: Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.)

Assertion

Ref	Expression
issdrg	⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))

Proof of Theorem issdrg

Dummy variables 𝑤 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sdrg 20864	. . . 4 ⊢ SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing})
2	1	mptrcl 6997	. . 3 ⊢ (𝑆 ∈ (SubDRing‘𝑅) → 𝑅 ∈ DivRing)
3		fveq2 6879	. . . . . . 7 ⊢ (𝑤 = 𝑅 → (SubRing‘𝑤) = (SubRing‘𝑅))
4		oveq1 7415	. . . . . . . 8 ⊢ (𝑤 = 𝑅 → (𝑤 ↾s 𝑠) = (𝑅 ↾s 𝑠))
5	4	eleq1d 2854	. . . . . . 7 ⊢ (𝑤 = 𝑅 → ((𝑤 ↾s 𝑠) ∈ DivRing ↔ (𝑅 ↾s 𝑠) ∈ DivRing))
6	3, 5	rabeqbidv 3441	. . . . . 6 ⊢ (𝑤 = 𝑅 → {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing} = {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing})
7		fvex 6892	. . . . . . 7 ⊢ (SubRing‘𝑅) ∈ V
8	7	rabex 5307	. . . . . 6 ⊢ {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing} ∈ V
9	6, 1, 8	fvmpt 6987	. . . . 5 ⊢ (𝑅 ∈ DivRing → (SubDRing‘𝑅) = {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing})
10	9	eleq2d 2855	. . . 4 ⊢ (𝑅 ∈ DivRing → (𝑆 ∈ (SubDRing‘𝑅) ↔ 𝑆 ∈ {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing}))
11		oveq2 7416	. . . . . 6 ⊢ (𝑠 = 𝑆 → (𝑅 ↾s 𝑠) = (𝑅 ↾s 𝑆))
12	11	eleq1d 2854	. . . . 5 ⊢ (𝑠 = 𝑆 → ((𝑅 ↾s 𝑠) ∈ DivRing ↔ (𝑅 ↾s 𝑆) ∈ DivRing))
13	12	elrab 3659	. . . 4 ⊢ (𝑆 ∈ {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing} ↔ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))
14	10, 13	bitrdi 290	. . 3 ⊢ (𝑅 ∈ DivRing → (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)))
15	2, 14	biadanii 833	. 2 ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)))
16		3anass 1109	. 2 ⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing) ↔ (𝑅 ∈ DivRing ∧ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)))
17	15, 16	bitr4i 281	1 ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  {crab 3423  ‘cfv 6534  (class class class)co 7408   ↾_s cress 17286  SubRingcsubrg 20650  DivRingcdr 20809  SubDRingcsdrg 20863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fv 6542  df-ov 7411  df-sdrg 20864

This theorem is referenced by:  sdrgrcl  20866  sdrgdrng  20867  sdrgsubrg  20868  sdrgid  20869  sdrgss  20870  issdrg2  20872  fldsdrgfld  20875  sdrgint  20881  primefld  20882  primefld0cl  20883  primefld1cl  20884  subsdrg  33558  sdrgdvcl  33559  sdrginvcl  33560  primefldchr  33561  fldgensdrg  33574  fldgenssp  33578  primefldgen1  33581  1fldgenq  33582  fldextsdrg  33985  fldextrspunlem2  34008  fldextrspundgdvdslem  34011  fldextrspundgdvds  34012  irngnzply1lem  34021  irngnzply1  34022  ply1annig1p  34035  minplycl  34037  ply1annprmidl  34038  algextdeglem1  34048  algextdeglem2  34049  algextdeglem3  34050  algextdeglem4  34051  algextdeglem5  34052  constrextdg2  34080  constrext2chnlem  34081  constrcon  34105  2sqr3minply  34111  cos9thpiminply  34119