![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subrgring | Structured version Visualization version GIF version |
Description: A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
Ref | Expression |
---|---|
subrgring.1 | β’ π = (π βΎs π΄) |
Ref | Expression |
---|---|
subrgring | β’ (π΄ β (SubRingβπ ) β π β Ring) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subrgring.1 | . 2 β’ π = (π βΎs π΄) | |
2 | eqid 2730 | . . . . 5 β’ (Baseβπ ) = (Baseβπ ) | |
3 | eqid 2730 | . . . . 5 β’ (1rβπ ) = (1rβπ ) | |
4 | 2, 3 | issubrg 20461 | . . . 4 β’ (π΄ β (SubRingβπ ) β ((π β Ring β§ (π βΎs π΄) β Ring) β§ (π΄ β (Baseβπ ) β§ (1rβπ ) β π΄))) |
5 | 4 | simplbi 496 | . . 3 β’ (π΄ β (SubRingβπ ) β (π β Ring β§ (π βΎs π΄) β Ring)) |
6 | 5 | simprd 494 | . 2 β’ (π΄ β (SubRingβπ ) β (π βΎs π΄) β Ring) |
7 | 1, 6 | eqeltrid 2835 | 1 β’ (π΄ β (SubRingβπ ) β π β Ring) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 394 = wceq 1539 β wcel 2104 β wss 3947 βcfv 6542 (class class class)co 7411 Basecbs 17148 βΎs cress 17177 1rcur 20075 Ringcrg 20127 SubRingcsubrg 20457 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6494 df-fun 6544 df-fv 6550 df-ov 7414 df-subrg 20459 |
This theorem is referenced by: subrgcrng 20465 subrgsubg 20467 subrg1 20472 subrgsubm 20475 subrguss 20477 subrginv 20478 subrgunit 20480 subrgugrp 20481 subrgnzr 20484 subsubrg 20488 resrhm 20491 resrhm2b 20492 issubdrg 20544 imadrhmcl 20556 subdrgint 20562 abvres 20590 sralmod 20954 ring2idlqus 21068 gzrngunitlem 21210 gzrngunit 21211 issubassa3 21639 subrgpsr 21758 mplring 21797 subrgmvrf 21808 subrgascl 21846 subrgasclcl 21847 evlssca 21871 evlsvar 21872 evlsgsumadd 21873 evlsvarpw 21876 mpfconst 21883 mpfproj 21884 mpfsubrg 21885 gsumply1subr 21976 ply1ring 21990 evls1sca 22062 evls1gsumadd 22063 evls1varpw 22066 dmatcrng 22224 scmatcrng 22243 scmatsgrp1 22244 scmatsrng1 22245 scmatmhm 22256 scmatrhm 22257 m2cpmrhm 22468 isclmp 24844 reefgim 26198 amgmlem 26730 cntrcrng 32484 evls1varpwval 32919 evls1fpws 32920 evls1addd 32922 evls1muld 32923 ressply10g 32930 asclply1subcl 32934 evls1fldgencl 33033 0ringirng 33042 evls1maplmhm 33049 ply1annnr 33053 irngnminplynz 33060 algextdeglem6 33067 imacrhmcl 41393 evlsscaval 41438 evlsvarval 41439 evlsbagval 41440 evlsmaprhm 41444 amgmwlem 47936 |
Copyright terms: Public domain | W3C validator |