| 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 20504 | . . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ (Base‘𝑅) ∧ (1r‘𝑅) ∈ 𝐴))) |
| 5 | 4 | simplbi 497 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring)) |
| 6 | 5 | simprd 495 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring) |
| 7 | 1, 6 | eqeltrid 2840 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ⊆ wss 3901 ‘cfv 6492 (class class class)co 7358 Basecbs 17136 ↾s cress 17157 1rcur 20116 Ringcrg 20168 SubRingcsubrg 20502 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fv 6500 df-ov 7361 df-subrg 20503 |
| This theorem is referenced by: subrgcrng 20508 subrgsubg 20510 subrg1 20515 subrgsubm 20518 subrguss 20520 subrginv 20521 subrgunit 20523 subrgugrp 20524 subrgnzr 20527 subsubrg 20531 resrhm 20534 resrhm2b 20535 issubdrg 20713 imadrhmcl 20730 subdrgint 20736 abvres 20764 sralmod 21139 ring2idlqus 21264 gzrngunitlem 21387 gzrngunit 21388 issubassa3 21821 subrgpsr 21933 mplring 21974 subrgmvrf 21989 subrgascl 22021 subrgasclcl 22022 evlssca 22049 evlsvar 22050 evlsgsumadd 22051 evlsvarpw 22054 mpfconst 22064 mpfproj 22065 mpfsubrg 22066 gsumply1subr 22174 ply1ring 22188 evls1sca 22267 evls1gsumadd 22268 evls1varpw 22271 evls1varpwval 22312 evls1fpws 22313 evls1addd 22315 evls1muld 22316 asclply1subcl 22318 evls1maplmhm 22321 dmatcrng 22446 scmatcrng 22465 scmatsgrp1 22466 scmatsrng1 22467 scmatmhm 22478 scmatrhm 22479 m2cpmrhm 22690 isclmp 25053 reefgim 26416 amgmlem 26956 cntrcrng 33163 ressply1evls1 33646 ressply10g 33648 evls1subd 33653 evls1monply1 33660 vr1nz 33674 evls1fldgencl 33827 0ringirng 33846 extdgfialglem2 33850 ply1annnr 33860 irngnminplynz 33869 minplyelirng 33872 algextdeglem6 33879 imacrhmcl 42769 evlsscaval 42810 evlsvarval 42811 evlsbagval 42812 evlsmaprhm 42816 amgmwlem 50047 |
| Copyright terms: Public domain | W3C validator |