![]() |
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 2724 | . . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅) | |
3 | 1, 2 | issubrg 20463 | . . 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 1533 ∈ wcel 2098 ⊆ wss 3940 ‘cfv 6533 (class class class)co 7401 Basecbs 17143 ↾s cress 17172 1rcur 20076 Ringcrg 20128 SubRingcsubrg 20459 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6485 df-fun 6535 df-fv 6541 df-ov 7404 df-subrg 20461 |
This theorem is referenced by: subrgsubg 20469 subrg1 20474 subrgsubm 20477 subrgdvds 20478 subrguss 20479 subrginv 20480 subrgdv 20481 subrgmre 20489 subsubrg 20490 issubdrg 20621 sdrgss 20634 sdrgacs 20642 subdrgint 20644 abvres 20672 sralmod 21033 cnsubrg 21289 issubassa3 21728 sraassab 21730 sraassa 21731 sraassaOLD 21732 aspid 21737 issubassa2 21754 resspsrbas 21845 resspsradd 21846 resspsrmul 21847 resspsrvsca 21848 mplassa 21891 ressmplbas2 21892 subrgascl 21937 subrgasclcl 21938 mplind 21941 evlsval2 21960 evlssca 21962 evlsscasrng 21970 mpfconst 21974 mpff 21977 mpfaddcl 21978 mpfmulcl 21979 mpfind 21980 ply1assa 22041 evls1val 22161 evls1rhm 22163 evls1sca 22164 evls1scasrng 22180 pf1f 22191 sranlm 24523 clmsscn 24928 cphreccllem 25028 cphdivcl 25032 cphabscl 25035 cphsqrtcl2 25036 cphsqrtcl3 25037 cphipcl 25041 4cphipval2 25092 resscdrg 25208 srabn 25210 plypf1 26066 dvply2g 26139 taylply2 26221 0ringsubrg 32847 fldgenssp 32874 idlinsubrg 33018 evls1fpws 33113 evls1vsca 33117 asclply1subcl 33127 sralvec 33151 lsssra 33154 drgext0g 33155 drgextvsca 33156 drgext0gsca 33157 drgextsubrg 33158 drgextlsp 33159 drgextgsum 33160 fedgmullem1 33193 fedgmullem2 33194 fedgmul 33195 extdggt0 33215 fldexttr 33216 extdg1id 33221 elirng 33230 irngss 33231 0ringirng 33233 evls1maplmhm 33240 ply1annnr 33244 imacrhmcl 41580 evlsval3 41620 evlsvvval 41624 evlsbagval 41627 evlsevl 41632 evlsmhpvvval 41656 mhphf 41658 mhphf2 41659 mhphf3 41660 cnsrexpcl 42396 fsumcnsrcl 42397 cnsrplycl 42398 rgspnid 42403 rngunsnply 42404 |
Copyright terms: Public domain | W3C validator |