grpinvid - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > grpinvid		Structured version Visualization version GIF version

Theorem grpinvid 18227

Description: The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.)

**Hypotheses**
Ref	Expression
grpinvid.u	⊢ 0 = (0_g‘𝐺)
grpinvid.n	⊢ 𝑁 = (inv_g‘𝐺)

**Assertion**
Ref	Expression
grpinvid	⊢ (𝐺 ∈ Grp → (𝑁‘ 0 ) = 0 )

**Proof of Theorem grpinvid**
Step	Hyp	Ref	Expression
1		eqid 2758	. . . 4 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		grpinvid.u	. . . 4 ⊢ 0 = (0_g‘𝐺)
3	1, 2	grpidcl 18198	. . 3 ⊢ (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
4		eqid 2758	. . . 4 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
5	1, 4, 2	grplid 18200	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 0 ∈ (Base‘𝐺)) → ( 0 (+_g‘𝐺) 0 ) = 0 )
6	3, 5	mpdan 686	. 2 ⊢ (𝐺 ∈ Grp → ( 0 (+_g‘𝐺) 0 ) = 0 )
7		grpinvid.n	. . . 4 ⊢ 𝑁 = (inv_g‘𝐺)
8	1, 4, 2, 7	grpinvid1 18221	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 0 ∈ (Base‘𝐺) ∧ 0 ∈ (Base‘𝐺)) → ((𝑁‘ 0 ) = 0 ↔ ( 0 (+_g‘𝐺) 0 ) = 0 ))
9	3, 3, 8	mpd3an23 1460	. 2 ⊢ (𝐺 ∈ Grp → ((𝑁‘ 0 ) = 0 ↔ ( 0 (+_g‘𝐺) 0 ) = 0 ))
10	6, 9	mpbird 260	1 ⊢ (𝐺 ∈ Grp → (𝑁‘ 0 ) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 = wceq 1538 ∈ wcel 2111 ‘cfv 6335 (class class class)co 7150 Basecbs 16541 +_gcplusg 16623 0_gc0g 16771 Grpcgrp 18169 inv_gcminusg 18170

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-op 4529 df-uni 4799 df-br 5033 df-opab 5095 df-mpt 5113 df-id 5430 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-fv 6343 df-riota 7108 df-ov 7153 df-0g 16773 df-mgm 17918 df-sgrp 17967 df-mnd 17978 df-grp 18172 df-minusg 18173

This theorem is referenced by: grpinvnz 18237 grpsubid1 18251 mulgneg 18313 mulginvcom 18319 mulgz 18322 0subg 18371 eqgid 18399 odnncl 18740 gexdvds 18776 gsumzinv 19133 gsumsub 19136 dprdfinv 19209 dsmmsubg 20508 mplsubglem 20764 mhpinvcl 20895 dchrisum0re 26196 qusker 31070 baerlem3lem1 39283

W3C validator