![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ringacl | Structured version Visualization version GIF version |
Description: Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.) |
Ref | Expression |
---|---|
ringacl.b | ⊢ 𝐵 = (Base‘𝑅) |
ringacl.p | ⊢ + = (+g‘𝑅) |
Ref | Expression |
---|---|
ringacl | ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringgrp 18598 | . 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
2 | ringacl.b | . . 3 ⊢ 𝐵 = (Base‘𝑅) | |
3 | ringacl.p | . . 3 ⊢ + = (+g‘𝑅) | |
4 | 2, 3 | grpcl 17477 | . 2 ⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
5 | 1, 4 | syl3an1 1399 | 1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1054 = wceq 1523 ∈ wcel 2030 ‘cfv 5926 (class class class)co 6690 Basecbs 15904 +gcplusg 15988 Grpcgrp 17469 Ringcrg 18593 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-nul 4822 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-sbc 3469 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-iota 5889 df-fv 5934 df-ov 6693 df-mgm 17289 df-sgrp 17331 df-mnd 17342 df-grp 17472 df-ring 18595 |
This theorem is referenced by: ringcom 18625 ringlghm 18650 ringrghm 18651 imasring 18665 qusring2 18666 cntzsubr 18860 srngadd 18905 issrngd 18909 lmodprop2d 18973 prdslmodd 19017 psrlmod 19449 mpfind 19584 coe1add 19682 ip2subdi 20037 mat1ghm 20337 scmatghm 20387 mdetrlin2 20461 mdetunilem5 20470 cpmatacl 20569 mdegaddle 23879 deg1addle2 23907 deg1add 23908 ply1divex 23941 dvhlveclem 36714 baerlem3lem1 37313 mendlmod 38080 cznrng 42280 lmod1lem3 42603 |
Copyright terms: Public domain | W3C validator |