![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > grpinvcl | Unicode version |
Description: A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 4-May-2015.) |
Ref | Expression |
---|---|
grpinvcl.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
grpinvcl.n |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
grpinvcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpinvcl.b |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | grpinvcl.n |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | grpinvf 12852 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | ffvelcdmda 5650 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4117 ax-sep 4120 ax-pow 4173 ax-pr 4208 ax-un 4432 ax-cnex 7899 ax-resscn 7900 ax-1re 7902 ax-addrcl 7905 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-un 3133 df-in 3135 df-ss 3142 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-int 3845 df-iun 3888 df-br 4003 df-opab 4064 df-mpt 4065 df-id 4292 df-xp 4631 df-rel 4632 df-cnv 4633 df-co 4634 df-dm 4635 df-rn 4636 df-res 4637 df-ima 4638 df-iota 5177 df-fun 5217 df-fn 5218 df-f 5219 df-f1 5220 df-fo 5221 df-f1o 5222 df-fv 5223 df-riota 5828 df-ov 5875 df-inn 8916 df-2 8974 df-ndx 12457 df-slot 12458 df-base 12460 df-plusg 12541 df-0g 12695 df-mgm 12707 df-sgrp 12740 df-mnd 12750 df-grp 12812 df-minusg 12813 |
This theorem is referenced by: grprinv 12855 grpinvid1 12856 grpinvid2 12857 grplrinv 12859 grpressid 12863 grplcan 12864 grpasscan1 12865 grpasscan2 12866 grpinvinv 12869 grpinvcnv 12870 grpinvnzcl 12874 grpsubinv 12875 grplmulf1o 12876 grpinvssd 12879 grpinvadd 12880 grpsubf 12881 grpsubrcan 12883 grpinvsub 12884 grpinvval2 12885 grpsubeq0 12888 grpsubadd 12890 grpaddsubass 12892 grpnpcan 12894 dfgrp3m 12901 grplactcnv 12904 grpsubpropd2 12907 ghmgrp 12914 mulgcl 12932 mulgaddcomlem 12937 mulginvcom 12939 mulginvinv 12940 mulgneg2 12948 subginv 12972 subginvcl 12974 issubg4m 12984 grpissubg 12985 subgintm 12989 0subg 12990 isnsg3 12998 nmzsubg 13001 eqger 13014 eqglact 13015 eqgcpbl 13018 ablinvadd 13044 ablsub2inv 13045 ablsub4 13047 ablsubsub4 13053 ringnegl 13159 rngnegr 13160 ringmneg1 13161 ringmneg2 13162 ringm2neg 13163 ringsubdi 13164 rngsubdir 13165 dvdsrneg 13203 unitinvcl 13223 unitnegcl 13230 |
Copyright terms: Public domain | W3C validator |