| 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 19073 | . 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 5649 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 Basecbs 17257 Grpcgrp 18988 -gcsg 18990 |
| 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 |
| 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 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 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-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 17482 df-mgm 18686 df-sgrp 18765 df-mnd 18781 df-grp 18991 df-minusg 18992 df-sbg 18993 |
| This theorem is referenced by: grpsubsub 19083 grpsubsub4 19087 grpnpncan 19089 grpnnncan2 19091 dfgrp3 19093 xpsgrpsub 19115 nsgconj 19213 nsgacs 19216 nsgid 19224 ghmnsgpreima 19299 ghmeqker 19301 ghmf1 19304 conjghm 19307 conjnmz 19310 conjnmzb 19311 sylow3lem2 19686 abladdsub4 19869 abladdsub 19870 ablsubaddsub 19872 ablpncan3 19874 ablsubsub4 19876 ablpnpcan 19877 ablnnncan 19880 ablnnncan1 19881 telgsumfzslem 20046 telgsumfzs 20047 telgsums 20051 ogrpsublt 20200 isdomn4 20788 ornglmulle 20936 orngrmulle 20937 lmodvsubcl 20994 lvecvscan2 21202 rngqiprngimfolem 21389 rngqiprngimfo 21400 rngqiprngfulem3 21412 rngqiprngfulem4 21413 rngqiprngfulem5 21414 ipsubdir 21749 ipsubdi 21750 ip2subdi 21751 coe1subfv 22384 evl1subd 22459 dmatsubcl 22612 scmatsubcl 22631 mdetunilem9 22734 mdetuni0 22735 chmatcl 22942 chpmat1d 22950 chpdmatlem1 22952 chpscmat 22956 chpidmat 22961 chfacfisf 22968 cpmadugsumlemF 22990 cpmidgsum2 22993 tgpconncomp 24227 ghmcnp 24229 nrmmetd 24688 ngpds2 24720 ngpds3 24722 isngp4 24726 nmsub 24737 nm2dif 24739 nmtri2 24741 subgngp 24749 ngptgp 24750 nrgdsdi 24779 nrgdsdir 24780 nlmdsdi 24795 nlmdsdir 24796 nrginvrcnlem 24805 nmods 24858 tcphcphlem1 25351 tcphcph 25353 cphipval2 25357 4cphipval2 25358 cphipval 25359 ipcnlem2 25360 deg1sublt 26224 ply1divmo 26250 ply1divex 26251 r1pcl 26273 r1pid 26275 ply1remlem 26279 idomrootle 26287 ig1peu 26289 dchr2sum 27391 lgsqrlem2 27465 lgsqrlem3 27466 lgsqrlem4 27467 ttgcontlem1 29139 grpsubcld 33269 archiabllem1a 33419 archiabllem2a 33422 archiabllem2c 33423 erler 33493 rlocf1 33502 fracerl 33537 evls1subd 33774 q1pvsca 33806 irngss 33989 2sqr3minply 34082 lclkrlem2m 42150 aks6d1c2lem4 42751 aks6d1c6lem2 42795 aks6d1c6lem3 42796 aks5lem2 42811 lidldomn1 48852 linply1 49025 |
| Copyright terms: Public domain | W3C validator |