Metamath Proof Explorer


Theorem sdrgacs

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

Ref Expression
Hypothesis subrgacs.b B=BaseR
Assertion sdrgacs RDivRingSubDRingRACSB

Proof

Step Hyp Ref Expression
1 subrgacs.b B=BaseR
2 eqid invrR=invrR
3 eqid 0R=0R
4 2 3 issdrg2 sSubDRingRRDivRingsSubRingRxs0RinvrRxs
5 3anass RDivRingsSubRingRxs0RinvrRxsRDivRingsSubRingRxs0RinvrRxs
6 4 5 bitri sSubDRingRRDivRingsSubRingRxs0RinvrRxs
7 6 baib RDivRingsSubDRingRsSubRingRxs0RinvrRxs
8 1 subrgss sSubRingRsB
9 velpw s𝒫BsB
10 8 9 sylibr sSubRingRs𝒫B
11 10 adantl RDivRingsSubRingRs𝒫B
12 iftrue x=0Rifx=0RxinvrRx=x
13 12 eleq1d x=0Rifx=0RxinvrRxyxy
14 13 biimprd x=0Rxyifx=0RxinvrRxy
15 eldifsni xy0Rx0R
16 15 necon2bi x=0R¬xy0R
17 16 pm2.21d x=0Rxy0RinvrRxy
18 14 17 2thd x=0Rxyifx=0RxinvrRxyxy0RinvrRxy
19 eldifsn xy0Rxyx0R
20 19 rbaibr x0Rxyxy0R
21 ifnefalse x0Rifx=0RxinvrRx=invrRx
22 21 eleq1d x0Rifx=0RxinvrRxyinvrRxy
23 20 22 imbi12d x0Rxyifx=0RxinvrRxyxy0RinvrRxy
24 18 23 pm2.61ine xyifx=0RxinvrRxyxy0RinvrRxy
25 24 ralbii2 xyifx=0RxinvrRxyxy0RinvrRxy
26 difeq1 y=sy0R=s0R
27 eleq2w y=sinvrRxyinvrRxs
28 26 27 raleqbidv y=sxy0RinvrRxyxs0RinvrRxs
29 25 28 syl5bb y=sxyifx=0RxinvrRxyxs0RinvrRxs
30 29 elrab3 s𝒫Bsy𝒫B|xyifx=0RxinvrRxyxs0RinvrRxs
31 11 30 syl RDivRingsSubRingRsy𝒫B|xyifx=0RxinvrRxyxs0RinvrRxs
32 31 pm5.32da RDivRingsSubRingRsy𝒫B|xyifx=0RxinvrRxysSubRingRxs0RinvrRxs
33 7 32 bitr4d RDivRingsSubDRingRsSubRingRsy𝒫B|xyifx=0RxinvrRxy
34 elin sSubRingRy𝒫B|xyifx=0RxinvrRxysSubRingRsy𝒫B|xyifx=0RxinvrRxy
35 33 34 bitr4di RDivRingsSubDRingRsSubRingRy𝒫B|xyifx=0RxinvrRxy
36 35 eqrdv RDivRingSubDRingR=SubRingRy𝒫B|xyifx=0RxinvrRxy
37 1 fvexi BV
38 mreacs BVACSBMoore𝒫B
39 37 38 mp1i RDivRingACSBMoore𝒫B
40 drngring RDivRingRRing
41 1 subrgacs RRingSubRingRACSB
42 40 41 syl RDivRingSubRingRACSB
43 simplr RDivRingxBx=0RxB
44 df-ne x0R¬x=0R
45 1 3 2 drnginvrcl RDivRingxBx0RinvrRxB
46 45 3expa RDivRingxBx0RinvrRxB
47 44 46 sylan2br RDivRingxB¬x=0RinvrRxB
48 43 47 ifclda RDivRingxBifx=0RxinvrRxB
49 48 ralrimiva RDivRingxBifx=0RxinvrRxB
50 acsfn1 BVxBifx=0RxinvrRxBy𝒫B|xyifx=0RxinvrRxyACSB
51 37 49 50 sylancr RDivRingy𝒫B|xyifx=0RxinvrRxyACSB
52 mreincl ACSBMoore𝒫BSubRingRACSBy𝒫B|xyifx=0RxinvrRxyACSBSubRingRy𝒫B|xyifx=0RxinvrRxyACSB
53 39 42 51 52 syl3anc RDivRingSubRingRy𝒫B|xyifx=0RxinvrRxyACSB
54 36 53 eqeltrd RDivRingSubDRingRACSB