![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subrgss | Structured version Visualization version GIF version |
Description: A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
Ref | Expression |
---|---|
subrgss.1 | ⊢ 𝐵 = (Base‘𝑅) |
Ref | Expression |
---|---|
subrgss | ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subrgss.1 | . . . 4 ⊢ 𝐵 = (Base‘𝑅) | |
2 | eqid 2734 | . . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅) | |
3 | 1, 2 | issubrg 20587 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴))) |
4 | 3 | simprbi 496 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴)) |
5 | 4 | simpld 494 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1536 ∈ wcel 2105 ⊆ wss 3962 ‘cfv 6562 (class class class)co 7430 Basecbs 17244 ↾s cress 17273 1rcur 20198 Ringcrg 20250 SubRingcsubrg 20585 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fv 6570 df-ov 7433 df-subrg 20586 |
This theorem is referenced by: subrgsubg 20593 subrg1 20598 subrgsubm 20601 subrgdvds 20602 subrguss 20603 subrginv 20604 subrgdv 20605 subrgmre 20613 subsubrg 20614 issubdrg 20797 sdrgss 20810 sdrgacs 20818 subdrgint 20820 abvres 20848 sralmod 21211 cnsubrg 21462 issubassa3 21903 sraassab 21905 sraassa 21906 sraassaOLD 21907 aspid 21912 issubassa2 21929 resspsrbas 22011 resspsradd 22012 resspsrmul 22013 resspsrvsca 22014 mplassa 22059 ressmplbas2 22062 subrgascl 22107 subrgasclcl 22108 mplind 22111 evlsval2 22128 evlssca 22130 evlsscasrng 22138 mpfconst 22142 mpff 22145 mpfaddcl 22146 mpfmulcl 22147 mpfind 22148 ply1assa 22216 evls1val 22339 evls1rhm 22341 evls1sca 22342 evls1scasrng 22358 pf1f 22369 evls1fpws 22388 evls1vsca 22392 asclply1subcl 22393 evls1maplmhm 22396 sranlm 24720 clmsscn 25125 cphreccllem 25225 cphdivcl 25229 cphabscl 25232 cphsqrtcl2 25233 cphsqrtcl3 25234 cphipcl 25238 4cphipval2 25289 resscdrg 25405 srabn 25407 plypf1 26265 dvply2g 26340 dvply2gOLD 26341 taylply2 26423 taylply2OLD 26424 0ringsubrg 33237 subrdom 33268 fldgenssp 33299 idlinsubrg 33438 ressasclcl 33575 sralvec 33614 lsssra 33617 drgext0g 33618 drgextvsca 33619 drgext0gsca 33620 drgextsubrg 33621 drgextlsp 33622 drgextgsum 33623 fedgmullem1 33656 fedgmullem2 33657 fedgmul 33658 extdggt0 33684 fldexttr 33685 extdg1id 33690 elirng 33700 irngss 33701 0ringirng 33703 ply1annnr 33710 imacrhmcl 42500 evlsval3 42545 evlsvvval 42549 evlsbagval 42552 evlsevl 42557 evlsmhpvvval 42581 mhphf 42583 mhphf2 42584 mhphf3 42585 cnsrexpcl 43153 fsumcnsrcl 43154 cnsrplycl 43155 rgspnid 43156 rngunsnply 43157 |
Copyright terms: Public domain | W3C validator |