# Metamath Proof Explorer

## Theorem issdrg

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

Ref Expression
Assertion issdrg ${⊢}{S}\in \mathrm{SubDRing}\left({R}\right)↔\left({R}\in \mathrm{DivRing}\wedge {S}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{S}\in \mathrm{DivRing}\right)$

### Proof

Step Hyp Ref Expression
1 df-sdrg ${⊢}\mathrm{SubDRing}=\left({w}\in \mathrm{DivRing}⟼\left\{{s}\in \mathrm{SubRing}\left({w}\right)|{w}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}\right)$
2 1 mptrcl ${⊢}{S}\in \mathrm{SubDRing}\left({R}\right)\to {R}\in \mathrm{DivRing}$
3 fveq2 ${⊢}{w}={R}\to \mathrm{SubRing}\left({w}\right)=\mathrm{SubRing}\left({R}\right)$
4 oveq1 ${⊢}{w}={R}\to {w}{↾}_{𝑠}{s}={R}{↾}_{𝑠}{s}$
5 4 eleq1d ${⊢}{w}={R}\to \left({w}{↾}_{𝑠}{s}\in \mathrm{DivRing}↔{R}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right)$
6 3 5 rabeqbidv ${⊢}{w}={R}\to \left\{{s}\in \mathrm{SubRing}\left({w}\right)|{w}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}=\left\{{s}\in \mathrm{SubRing}\left({R}\right)|{R}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}$
7 fvex ${⊢}\mathrm{SubRing}\left({R}\right)\in \mathrm{V}$
8 7 rabex ${⊢}\left\{{s}\in \mathrm{SubRing}\left({R}\right)|{R}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}\in \mathrm{V}$
9 6 1 8 fvmpt ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubDRing}\left({R}\right)=\left\{{s}\in \mathrm{SubRing}\left({R}\right)|{R}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}$
10 9 eleq2d ${⊢}{R}\in \mathrm{DivRing}\to \left({S}\in \mathrm{SubDRing}\left({R}\right)↔{S}\in \left\{{s}\in \mathrm{SubRing}\left({R}\right)|{R}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}\right)$
11 oveq2 ${⊢}{s}={S}\to {R}{↾}_{𝑠}{s}={R}{↾}_{𝑠}{S}$
12 11 eleq1d ${⊢}{s}={S}\to \left({R}{↾}_{𝑠}{s}\in \mathrm{DivRing}↔{R}{↾}_{𝑠}{S}\in \mathrm{DivRing}\right)$
13 12 elrab ${⊢}{S}\in \left\{{s}\in \mathrm{SubRing}\left({R}\right)|{R}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right\}↔\left({S}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{S}\in \mathrm{DivRing}\right)$
14 10 13 syl6bb ${⊢}{R}\in \mathrm{DivRing}\to \left({S}\in \mathrm{SubDRing}\left({R}\right)↔\left({S}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{S}\in \mathrm{DivRing}\right)\right)$
15 2 14 biadanii ${⊢}{S}\in \mathrm{SubDRing}\left({R}\right)↔\left({R}\in \mathrm{DivRing}\wedge \left({S}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{S}\in \mathrm{DivRing}\right)\right)$
16 3anass ${⊢}\left({R}\in \mathrm{DivRing}\wedge {S}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{S}\in \mathrm{DivRing}\right)↔\left({R}\in \mathrm{DivRing}\wedge \left({S}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{S}\in \mathrm{DivRing}\right)\right)$
17 15 16 bitr4i ${⊢}{S}\in \mathrm{SubDRing}\left({R}\right)↔\left({R}\in \mathrm{DivRing}\wedge {S}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{S}\in \mathrm{DivRing}\right)$