# Metamath Proof Explorer

## Theorem sdrgacs

Description: Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypothesis subrgacs.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion sdrgacs ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubDRing}\left({R}\right)\in \mathrm{ACS}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 subrgacs.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 eqid ${⊢}{inv}_{r}\left({R}\right)={inv}_{r}\left({R}\right)$
3 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
4 2 3 issdrg2 ${⊢}{s}\in \mathrm{SubDRing}\left({R}\right)↔\left({R}\in \mathrm{DivRing}\wedge {s}\in \mathrm{SubRing}\left({R}\right)\wedge \forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)$
5 3anass ${⊢}\left({R}\in \mathrm{DivRing}\wedge {s}\in \mathrm{SubRing}\left({R}\right)\wedge \forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)↔\left({R}\in \mathrm{DivRing}\wedge \left({s}\in \mathrm{SubRing}\left({R}\right)\wedge \forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)\right)$
6 4 5 bitri ${⊢}{s}\in \mathrm{SubDRing}\left({R}\right)↔\left({R}\in \mathrm{DivRing}\wedge \left({s}\in \mathrm{SubRing}\left({R}\right)\wedge \forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)\right)$
7 6 baib ${⊢}{R}\in \mathrm{DivRing}\to \left({s}\in \mathrm{SubDRing}\left({R}\right)↔\left({s}\in \mathrm{SubRing}\left({R}\right)\wedge \forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)\right)$
8 1 subrgss ${⊢}{s}\in \mathrm{SubRing}\left({R}\right)\to {s}\subseteq {B}$
9 velpw ${⊢}{s}\in 𝒫{B}↔{s}\subseteq {B}$
10 8 9 sylibr ${⊢}{s}\in \mathrm{SubRing}\left({R}\right)\to {s}\in 𝒫{B}$
11 10 adantl ${⊢}\left({R}\in \mathrm{DivRing}\wedge {s}\in \mathrm{SubRing}\left({R}\right)\right)\to {s}\in 𝒫{B}$
12 iftrue ${⊢}{x}={0}_{{R}}\to if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)={x}$
13 12 eleq1d ${⊢}{x}={0}_{{R}}\to \left(if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}↔{x}\in {y}\right)$
14 13 biimprd ${⊢}{x}={0}_{{R}}\to \left({x}\in {y}\to if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right)$
15 eldifsni ${⊢}{x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)\to {x}\ne {0}_{{R}}$
16 15 necon2bi ${⊢}{x}={0}_{{R}}\to ¬{x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)$
17 16 pm2.21d ${⊢}{x}={0}_{{R}}\to \left({x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)\to {inv}_{r}\left({R}\right)\left({x}\right)\in {y}\right)$
18 14 17 2thd ${⊢}{x}={0}_{{R}}\to \left(\left({x}\in {y}\to if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right)↔\left({x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)\to {inv}_{r}\left({R}\right)\left({x}\right)\in {y}\right)\right)$
19 eldifsn ${⊢}{x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)↔\left({x}\in {y}\wedge {x}\ne {0}_{{R}}\right)$
20 19 rbaibr ${⊢}{x}\ne {0}_{{R}}\to \left({x}\in {y}↔{x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)\right)$
21 ifnefalse ${⊢}{x}\ne {0}_{{R}}\to if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)={inv}_{r}\left({R}\right)\left({x}\right)$
22 21 eleq1d ${⊢}{x}\ne {0}_{{R}}\to \left(if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}↔{inv}_{r}\left({R}\right)\left({x}\right)\in {y}\right)$
23 20 22 imbi12d ${⊢}{x}\ne {0}_{{R}}\to \left(\left({x}\in {y}\to if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right)↔\left({x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)\to {inv}_{r}\left({R}\right)\left({x}\right)\in {y}\right)\right)$
24 18 23 pm2.61ine ${⊢}\left({x}\in {y}\to if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right)↔\left({x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)\to {inv}_{r}\left({R}\right)\left({x}\right)\in {y}\right)$
25 24 ralbii2 ${⊢}\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}↔\forall {x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {y}$
26 difeq1 ${⊢}{y}={s}\to {y}\setminus \left\{{0}_{{R}}\right\}={s}\setminus \left\{{0}_{{R}}\right\}$
27 eleq2w ${⊢}{y}={s}\to \left({inv}_{r}\left({R}\right)\left({x}\right)\in {y}↔{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)$
28 26 27 raleqbidv ${⊢}{y}={s}\to \left(\forall {x}\in \left({y}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {y}↔\forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)$
29 25 28 syl5bb ${⊢}{y}={s}\to \left(\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}↔\forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)$
30 29 elrab3 ${⊢}{s}\in 𝒫{B}\to \left({s}\in \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}↔\forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)$
31 11 30 syl ${⊢}\left({R}\in \mathrm{DivRing}\wedge {s}\in \mathrm{SubRing}\left({R}\right)\right)\to \left({s}\in \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}↔\forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)$
32 31 pm5.32da ${⊢}{R}\in \mathrm{DivRing}\to \left(\left({s}\in \mathrm{SubRing}\left({R}\right)\wedge {s}\in \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\right)↔\left({s}\in \mathrm{SubRing}\left({R}\right)\wedge \forall {x}\in \left({s}\setminus \left\{{0}_{{R}}\right\}\right)\phantom{\rule{.4em}{0ex}}{inv}_{r}\left({R}\right)\left({x}\right)\in {s}\right)\right)$
33 7 32 bitr4d ${⊢}{R}\in \mathrm{DivRing}\to \left({s}\in \mathrm{SubDRing}\left({R}\right)↔\left({s}\in \mathrm{SubRing}\left({R}\right)\wedge {s}\in \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\right)\right)$
34 elin ${⊢}{s}\in \left(\mathrm{SubRing}\left({R}\right)\cap \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\right)↔\left({s}\in \mathrm{SubRing}\left({R}\right)\wedge {s}\in \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\right)$
35 33 34 syl6bbr ${⊢}{R}\in \mathrm{DivRing}\to \left({s}\in \mathrm{SubDRing}\left({R}\right)↔{s}\in \left(\mathrm{SubRing}\left({R}\right)\cap \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\right)\right)$
36 35 eqrdv ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubDRing}\left({R}\right)=\mathrm{SubRing}\left({R}\right)\cap \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}$
37 1 fvexi ${⊢}{B}\in \mathrm{V}$
38 mreacs ${⊢}{B}\in \mathrm{V}\to \mathrm{ACS}\left({B}\right)\in \mathrm{Moore}\left(𝒫{B}\right)$
39 37 38 mp1i ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{ACS}\left({B}\right)\in \mathrm{Moore}\left(𝒫{B}\right)$
40 drngring ${⊢}{R}\in \mathrm{DivRing}\to {R}\in \mathrm{Ring}$
41 1 subrgacs ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubRing}\left({R}\right)\in \mathrm{ACS}\left({B}\right)$
42 40 41 syl ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubRing}\left({R}\right)\in \mathrm{ACS}\left({B}\right)$
43 simplr ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge {x}\in {B}\right)\wedge {x}={0}_{{R}}\right)\to {x}\in {B}$
44 df-ne ${⊢}{x}\ne {0}_{{R}}↔¬{x}={0}_{{R}}$
45 1 3 2 drnginvrcl ${⊢}\left({R}\in \mathrm{DivRing}\wedge {x}\in {B}\wedge {x}\ne {0}_{{R}}\right)\to {inv}_{r}\left({R}\right)\left({x}\right)\in {B}$
46 45 3expa ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge {x}\in {B}\right)\wedge {x}\ne {0}_{{R}}\right)\to {inv}_{r}\left({R}\right)\left({x}\right)\in {B}$
47 44 46 sylan2br ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge {x}\in {B}\right)\wedge ¬{x}={0}_{{R}}\right)\to {inv}_{r}\left({R}\right)\left({x}\right)\in {B}$
48 43 47 ifclda ${⊢}\left({R}\in \mathrm{DivRing}\wedge {x}\in {B}\right)\to if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {B}$
49 48 ralrimiva ${⊢}{R}\in \mathrm{DivRing}\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {B}$
50 acsfn1 ${⊢}\left({B}\in \mathrm{V}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {B}\right)\to \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\in \mathrm{ACS}\left({B}\right)$
51 37 49 50 sylancr ${⊢}{R}\in \mathrm{DivRing}\to \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\in \mathrm{ACS}\left({B}\right)$
52 mreincl ${⊢}\left(\mathrm{ACS}\left({B}\right)\in \mathrm{Moore}\left(𝒫{B}\right)\wedge \mathrm{SubRing}\left({R}\right)\in \mathrm{ACS}\left({B}\right)\wedge \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\in \mathrm{ACS}\left({B}\right)\right)\to \mathrm{SubRing}\left({R}\right)\cap \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\in \mathrm{ACS}\left({B}\right)$
53 39 42 51 52 syl3anc ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubRing}\left({R}\right)\cap \left\{{y}\in 𝒫{B}|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}if\left({x}={0}_{{R}},{x},{inv}_{r}\left({R}\right)\left({x}\right)\right)\in {y}\right\}\in \mathrm{ACS}\left({B}\right)$
54 36 53 eqeltrd ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubDRing}\left({R}\right)\in \mathrm{ACS}\left({B}\right)$