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 19124

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 2762	. . . 4 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		grpinvid.u	. . . 4 ⊢ 0 = (0_g‘𝐺)
3	1, 2	grpidcl 19090	. . 3 ⊢ (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
4		eqid 2762	. . . 4 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
5	1, 4, 2	grplid 19092	. . 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 19116	. . 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 6537 (class class class)co 7416 Basecbs 17305 +_gcplusg 17346 0_gc0g 17528 Grpcgrp 19058 inv_gcminusg 19059

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 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-br 5108 df-opab 5172 df-mpt 5191 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fv 6545 df-riota 7373 df-ov 7419 df-0g 17530 df-mgm 18734 df-sgrp 18823 df-mnd 18839 df-grp 19061 df-minusg 19062

This theorem is used by: grpinvnz 19134 grpsubid1 19149 mulgneg 19216 mulginvcom 19223 mulgz 19226 0subg 19276 eqgid 19306 odnncl 19673 gexdvds 19712 gsumzinv 20073 gsumsub 20076 dprdfinv 20149 qsnzr 21547 dsmmsubg 21957 mplsubglem 22214 mhpinvcl 22381 dchrisum0re 27747 erler 33692 qusker 33776 baerlem3lem1 42567 primrootscoprbij 42955

W3C validator