Description: Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | subrgacs.b | |
|
Assertion | sdrgacs | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subrgacs.b | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | 2 3 | issdrg2 | |
5 | 3anass | |
|
6 | 4 5 | bitri | |
7 | 6 | baib | |
8 | 1 | subrgss | |
9 | velpw | |
|
10 | 8 9 | sylibr | |
11 | 10 | adantl | |
12 | iftrue | |
|
13 | 12 | eleq1d | |
14 | 13 | biimprd | |
15 | eldifsni | |
|
16 | 15 | necon2bi | |
17 | 16 | pm2.21d | |
18 | 14 17 | 2thd | |
19 | eldifsn | |
|
20 | 19 | rbaibr | |
21 | ifnefalse | |
|
22 | 21 | eleq1d | |
23 | 20 22 | imbi12d | |
24 | 18 23 | pm2.61ine | |
25 | 24 | ralbii2 | |
26 | difeq1 | |
|
27 | eleq2w | |
|
28 | 26 27 | raleqbidv | |
29 | 25 28 | syl5bb | |
30 | 29 | elrab3 | |
31 | 11 30 | syl | |
32 | 31 | pm5.32da | |
33 | 7 32 | bitr4d | |
34 | elin | |
|
35 | 33 34 | bitr4di | |
36 | 35 | eqrdv | |
37 | 1 | fvexi | |
38 | mreacs | |
|
39 | 37 38 | mp1i | |
40 | drngring | |
|
41 | 1 | subrgacs | |
42 | 40 41 | syl | |
43 | simplr | |
|
44 | df-ne | |
|
45 | 1 3 2 | drnginvrcl | |
46 | 45 | 3expa | |
47 | 44 46 | sylan2br | |
48 | 43 47 | ifclda | |
49 | 48 | ralrimiva | |
50 | acsfn1 | |
|
51 | 37 49 50 | sylancr | |
52 | mreincl | |
|
53 | 39 42 51 52 | syl3anc | |
54 | 36 53 | eqeltrd | |