Description: Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sdrgid.1 | |
|
Assertion | sdrgid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sdrgid.1 | |
|
2 | id | |
|
3 | drngring | |
|
4 | 1 | subrgid | |
5 | 3 4 | syl | |
6 | 1 | ressid | |
7 | 6 2 | eqeltrd | |
8 | issdrg | |
|
9 | 2 5 7 8 | syl3anbrc | |