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 19171

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 2760	. . . 4 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		grpinvid.u	. . . 4 ⊢ 0 = (0_g‘𝐺)
3	1, 2	grpidcl 19137	. . 3 ⊢ (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
4		eqid 2760	. . . 4 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
5	1, 4, 2	grplid 19139	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 0 ∈ (Base‘𝐺)) → ( 0 (+_g‘𝐺) 0 ) = 0 )
6	3, 5	mpdan 700	. 2 ⊢ (𝐺 ∈ Grp → ( 0 (+_g‘𝐺) 0 ) = 0 )
7		grpinvid.n	. . . 4 ⊢ 𝑁 = (inv_g‘𝐺)
8	1, 4, 2, 7	grpinvid1 19163	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 0 ∈ (Base‘𝐺) ∧ 0 ∈ (Base‘𝐺)) → ((𝑁‘ 0 ) = 0 ↔ ( 0 (+_g‘𝐺) 0 ) = 0 ))
9	3, 3, 8	mpd3an23 1492	. 2 ⊢ (𝐺 ∈ Grp → ((𝑁‘ 0 ) = 0 ↔ ( 0 (+_g‘𝐺) 0 ) = 0 ))
10	6, 9	mpbird 260	1 ⊢ (𝐺 ∈ Grp → (𝑁‘ 0 ) = 0 )

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 = wceq 1570 ∈ wcel 2145 ‘cfv 6527 (class class class)co 7408 Basecbs 17348 +_gcplusg 17389 0_gc0g 17571 Grpcgrp 19105 inv_gcminusg 19106

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5542 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-fv 6535 df-riota 7365 df-ov 7411 df-0g 17573 df-mgm 18777 df-sgrp 18869 df-mnd 18885 df-grp 19108 df-minusg 19109

This theorem is used by: grpinvnz 19181 grpsubid1 19196 mulgneg 19263 mulginvcom 19270 mulgz 19273 0subg 19323 eqgid 19353 odnncl 19720 gexdvds 19759 gsumzinv 20120 gsumsub 20123 dprdfinv 20196 qsnzr 21600 dsmmsubg 22010 mplsubglem 22267 mhpinvcl 22434 dchrisum0re 27803 erler 33759 qusker 33843 baerlem3lem1 42684 primrootscoprbij 43072

W3C validator