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 19210

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 19176	. . 3 ⊢ (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
4		eqid 2760	. . . 4 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
5	1, 4, 2	grplid 19178	. . 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 19202	. . 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 1569 ∈ wcel 2144 ‘cfv 6538 (class class class)co 7420 Basecbs 17387 +_gcplusg 17428 0_gc0g 17610 Grpcgrp 19144 inv_gcminusg 19145

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 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-ss 3896 df-dif 4047 df-in 4091 df-un 4151 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 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-fv 6546 df-riota 7377 df-ov 7423 df-0g 17612 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-grp 19147 df-minusg 19148

This theorem is used by: grpinvnz 19220 grpsubid1 19235 mulgneg 19302 mulginvcom 19309 mulgz 19312 0subg 19362 eqgid 19392 odnncl 19759 gexdvds 19798 gsumzinv 20159 gsumsub 20162 dprdfinv 20235 qsnzr 21639 dsmmsubg 22049 mplsubglem 22306 mhpinvcl 22473 dchrisum0re 27840 erler 33826 qusker 33910 baerlem3lem1 42765 primrootscoprbij 43153

W3C validator