| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > subrgbas | Structured version Visualization version GIF version | ||
| Description: Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| Ref | Expression |
|---|---|
| subrgbas.b | ⊢ 𝑆 = (𝑅 ↾s 𝐴) |
| Ref | Expression |
|---|---|
| subrgbas | ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | subrgsubg 20650 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) | |
| 2 | subrgbas.b | . . 3 ⊢ 𝑆 = (𝑅 ↾s 𝐴) | |
| 3 | 2 | subgbas 19184 | . 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝐴 = (Base‘𝑆)) |
| 4 | 1, 3 | syl 18 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1563 ∈ wcel 2145 ‘cfv 6525 (class class class)co 7400 Basecbs 17257 ↾s cress 17278 SubGrpcsubg 19174 SubRingcsubrg 20642 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-cnex 11144 ax-1cn 11146 ax-addcl 11148 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-nn 12222 df-sets 17212 df-slot 17230 df-ndx 17242 df-base 17258 df-ress 17279 df-subg 19177 df-ring 20305 df-subrg 20643 |
| This theorem is referenced by: subrg1 20655 subrgdvds 20659 subrguss 20660 subrginv 20661 subrgdv 20662 subrgunit 20663 subsubrg 20671 issubdrg 20849 abvres 20900 qsssubdrg 21533 gzrngunitlem 21539 gzrngunit 21540 issubassa3 21973 sraassab 21975 resspsrbas 22080 resspsradd 22081 resspsrmul 22082 resspsrvsca 22083 subrgpsr 22084 subrgascl 22174 subrgasclcl 22175 evlsvvval 22201 evlsscaval 22234 evlsevl 22240 dmatcrng 22616 scmatcrng 22635 scmatstrbas 22640 sranlm 24798 isclmi 25193 plypf1 26326 sdrgdvcl 33530 sdrginvcl 33531 idlinsubrg 33650 evlsbagval 43175 evlsmhpvvval 43184 mhphf 43186 |
| Copyright terms: Public domain | W3C validator |