| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > grpsubcl | Structured version Visualization version GIF version | ||
| Description: Closure of group subtraction. (Contributed by NM, 31-Mar-2014.) |
| Ref | Expression |
|---|---|
| grpsubcl.b | ⊢ 𝐵 = (Base‘𝐺) |
| grpsubcl.m | ⊢ − = (-g‘𝐺) |
| Ref | Expression |
|---|---|
| grpsubcl | ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpsubcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
| 2 | grpsubcl.m | . . 3 ⊢ − = (-g‘𝐺) | |
| 3 | 1, 2 | grpsubf 19076 | . 2 ⊢ (𝐺 ∈ Grp → − :(𝐵 × 𝐵)⟶𝐵) |
| 4 | fovcdm 7570 | . 2 ⊢ (( − :(𝐵 × 𝐵)⟶𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵) | |
| 5 | 3, 4 | syl3an1 1179 | 1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 × cxp 5650 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 Basecbs 17259 Grpcgrp 18990 -gcsg 18992 |
| 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 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 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-rmo 3370 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-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-1st 7974 df-2nd 7975 df-0g 17484 df-mgm 18688 df-sgrp 18767 df-mnd 18783 df-grp 18993 df-minusg 18994 df-sbg 18995 |
| This theorem is referenced by: grpsubsub 19086 grpsubsub4 19090 grpnpncan 19092 grpnnncan2 19094 dfgrp3 19096 xpsgrpsub 19118 nsgconj 19216 nsgacs 19219 nsgid 19227 ghmnsgpreima 19302 ghmeqker 19304 ghmf1 19307 conjghm 19310 conjnmz 19313 conjnmzb 19314 sylow3lem2 19689 abladdsub4 19872 abladdsub 19873 ablsubaddsub 19875 ablpncan3 19877 ablsubsub4 19879 ablpnpcan 19880 ablnnncan 19883 ablnnncan1 19884 telgsumfzslem 20049 telgsumfzs 20050 telgsums 20054 ogrpsublt 20203 isdomn4 20791 ornglmulle 20939 orngrmulle 20940 lmodvsubcl 20997 lvecvscan2 21205 rngqiprngimfolem 21392 rngqiprngimfo 21403 rngqiprngfulem3 21415 rngqiprngfulem4 21416 rngqiprngfulem5 21417 ipsubdir 21752 ipsubdi 21753 ip2subdi 21754 coe1subfv 22387 evl1subd 22463 dmatsubcl 22616 scmatsubcl 22635 mdetunilem9 22738 mdetuni0 22739 chmatcl 22946 chpmat1d 22954 chpdmatlem1 22956 chpscmat 22960 chpidmat 22965 chfacfisf 22972 cpmadugsumlemF 22994 cpmidgsum2 22997 tgpconncomp 24231 ghmcnp 24233 nrmmetd 24692 ngpds2 24724 ngpds3 24726 isngp4 24730 nmsub 24741 nm2dif 24743 nmtri2 24745 subgngp 24753 ngptgp 24754 nrgdsdi 24783 nrgdsdir 24784 nlmdsdi 24799 nlmdsdir 24800 nrginvrcnlem 24809 nmods 24862 tcphcphlem1 25355 tcphcph 25357 cphipval2 25361 4cphipval2 25362 cphipval 25363 ipcnlem2 25364 deg1sublt 26228 ply1divmo 26254 ply1divex 26255 r1pcl 26277 r1pid 26279 ply1remlem 26283 idomrootle 26291 ig1peu 26293 dchr2sum 27395 lgsqrlem2 27469 lgsqrlem3 27470 lgsqrlem4 27471 ttgcontlem1 29143 grpsubcld 33274 archiabllem1a 33424 archiabllem2a 33427 archiabllem2c 33428 erler 33498 rlocf1 33507 fracerl 33542 evls1subd 33779 q1pvsca 33811 irngss 33994 2sqr3minply 34087 lclkrlem2m 42155 aks6d1c2lem4 42756 aks6d1c6lem2 42800 aks6d1c6lem3 42801 aks5lem2 42816 lidldomn1 48851 linply1 49024 |
| Copyright terms: Public domain | W3C validator |