Theorem issdrg 20941

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 20940	. . . 4 ⊢ SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing})
2	1	mptrcl 7003	. . 3 ⊢ (𝑆 ∈ (SubDRing‘𝑅) → 𝑅 ∈ DivRing)
3		fveq2 6885	. . . . . . 7 ⊢ (𝑤 = 𝑅 → (SubRing‘𝑤) = (SubRing‘𝑅))
4		oveq1 7426	. . . . . . . 8 ⊢ (𝑤 = 𝑅 → (𝑤 ↾s 𝑠) = (𝑅 ↾s 𝑠))
5	4	eleq1d 2850	. . . . . . 7 ⊢ (𝑤 = 𝑅 → ((𝑤 ↾s 𝑠) ∈ DivRing ↔ (𝑅 ↾s 𝑠) ∈ DivRing))
6	3, 5	rabeqbidv 3436	. . . . . 6 ⊢ (𝑤 = 𝑅 → {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing} = {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing})
7		fvex 6898	. . . . . . 7 ⊢ (SubRing‘𝑅) ∈ V
8	7	rabex 5311	. . . . . 6 ⊢ {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing} ∈ V
9	6, 1, 8	fvmpt 6993	. . . . 5 ⊢ (𝑅 ∈ DivRing → (SubDRing‘𝑅) = {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing})
10	9	eleq2d 2851	. . . 4 ⊢ (𝑅 ∈ DivRing → (𝑆 ∈ (SubDRing‘𝑅) ↔ 𝑆 ∈ {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing}))
11		oveq2 7427	. . . . . 6 ⊢ (𝑠 = 𝑆 → (𝑅 ↾s 𝑠) = (𝑅 ↾s 𝑆))
12	11	eleq1d 2850	. . . . 5 ⊢ (𝑠 = 𝑆 → ((𝑅 ↾s 𝑠) ∈ DivRing ↔ (𝑅 ↾s 𝑆) ∈ DivRing))
13	12	elrab 3652	. . . 4 ⊢ (𝑆 ∈ {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing} ↔ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))
14	10, 13	bitrdi 290	. . 3 ⊢ (𝑅 ∈ DivRing → (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)))
15	2, 14	biadanii 834	. 2 ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)))
16		3anass 1111	. 2 ⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing) ↔ (𝑅 ∈ DivRing ∧ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)))
17	15, 16	bitr4i 281	1 ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  {crab 3418  ‘cfv 6540  (class class class)co 7419   ↾_s cress 17312  SubRingcsubrg 20718  DivRingcdr 20877  SubDRingcsdrg 20939

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7422  df-sdrg 20940

This theorem is used by:  sdrgrcl  20942  sdrgdrng  20943  sdrgsubrg  20944  sdrgid  20945  sdrgss  20946  issdrg2  20948  fldsdrgfld  20951  sdrgint  20957  primefld  20958  primefld0cl  20959  primefld1cl  20960  subsdrg  33683  sdrgdvcl  33684  sdrginvcl  33685  primefldchr  33686  fldgensdrg  33699  fldgenssp  33703  primefldgen1  33706  1fldgenq  33707  fldextsdrg  34108  fldextrspunlem2  34131  fldextrspundgdvdslem  34134  fldextrspundgdvds  34135  irngnzply1lem  34144  irngnzply1  34145  ply1annig1p  34158  minplycl  34160  ply1annprmidl  34161  algextdeglem1  34171  algextdeglem2  34172  algextdeglem3  34173  algextdeglem4  34174  algextdeglem5  34175  constrextdg2  34203  constrext2chnlem  34204  constrcon  34228  2sqr3minply  34234  cos9thpiminply  34242