Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > subrg1cl | Structured version Visualization version GIF version |
Description: A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
Ref | Expression |
---|---|
subrg1cl.a | ⊢ 1 = (1r‘𝑅) |
Ref | Expression |
---|---|
subrg1cl | ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
2 | subrg1cl.a | . . . 4 ⊢ 1 = (1r‘𝑅) | |
3 | 1, 2 | issubrg 19939 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ (Base‘𝑅) ∧ 1 ∈ 𝐴))) |
4 | 3 | simprbi 496 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐴 ⊆ (Base‘𝑅) ∧ 1 ∈ 𝐴)) |
5 | 4 | simprd 495 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ⊆ wss 3883 ‘cfv 6418 (class class class)co 7255 Basecbs 16840 ↾s cress 16867 1rcur 19652 Ringcrg 19698 SubRingcsubrg 19935 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fv 6426 df-ov 7258 df-subrg 19937 |
This theorem is referenced by: subrg1 19949 subrgsubm 19952 issubrg2 19959 subrgint 19961 subsubrg 19965 primefld1cl 19990 zsssubrg 20568 issubassa2 21006 subrgpsr 21098 mplassa 21137 mplbas2 21153 ply1assa 21280 isclmp 24166 taylply2 25432 subrgchr 31393 drgextlsp 31583 evlsbagval 40198 cnsrexpcl 40906 rngunsnply 40914 |
Copyright terms: Public domain | W3C validator |