Metamath Proof Explorer


Theorem sdrgacs

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

Ref Expression
Hypothesis subrgacs.b B = Base R
Assertion sdrgacs R DivRing SubDRing R ACS B

Proof

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