![]() |
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 2736 | . . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
3 | eqid 2736 | . . . . 5 ⊢ (1r‘𝑅) = (1r‘𝑅) | |
4 | 2, 3 | issubrg 20218 | . . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ (Base‘𝑅) ∧ (1r‘𝑅) ∈ 𝐴))) |
5 | 4 | simplbi 498 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring)) |
6 | 5 | simprd 496 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring) |
7 | 1, 6 | eqeltrid 2842 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ⊆ wss 3909 ‘cfv 6494 (class class class)co 7354 Basecbs 17080 ↾s cress 17109 1rcur 19909 Ringcrg 19960 SubRingcsubrg 20214 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2888 df-ne 2943 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5530 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6446 df-fun 6496 df-fv 6502 df-ov 7357 df-subrg 20216 |
This theorem is referenced by: subrgcrng 20222 subrgsubg 20224 subrg1 20228 subrgmcl 20230 subrgsubm 20231 subrguss 20233 subrginv 20234 subrgunit 20236 subrgugrp 20237 issubdrg 20243 subsubrg 20244 resrhm 20247 subdrgint 20266 abvres 20294 sralmod 20652 subrgnzr 20734 gzrngunitlem 20858 gzrngunit 20859 issubassa3 21267 subrgpsr 21384 mplring 21420 subrgmvrf 21431 subrgascl 21470 subrgasclcl 21471 evlssca 21495 evlsvar 21496 evlsgsumadd 21497 evlsvarpw 21500 mpfconst 21507 mpfproj 21508 mpfsubrg 21509 gsumply1subr 21601 ply1ring 21615 evls1sca 21685 evls1gsumadd 21686 evls1varpw 21689 dmatcrng 21847 scmatcrng 21866 scmatsgrp1 21867 scmatsrng1 21868 scmatmhm 21879 scmatrhm 21880 m2cpmrhm 22091 isclmp 24456 reefgim 25805 amgmlem 26335 cntrcrng 31799 evls1varpwval 32161 evls1fpws 32162 evls1addd 32164 evls1muld 32165 ressply10g 32168 asclply1subcl 32172 0ringirng 32254 resrhm2b 40683 rncrhmcl 40684 evlsscaval 40724 evlsvarval 40725 evlsbagval 40726 mhphf 40747 amgmwlem 47219 |
Copyright terms: Public domain | W3C validator |