grpinvinv - Metamath Proof Explorer

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

Theorem grpinvinv 19216

Description: Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 31-Mar-2014.)

**Hypotheses**
Ref	Expression
grpinvinv.b	⊢ 𝐵 = (Base‘𝐺)
grpinvinv.n	⊢ 𝑁 = (inv_g‘𝐺)

**Assertion**
Ref	Expression
grpinvinv	⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝑁‘𝑋)) = 𝑋)

**Proof of Theorem grpinvinv**
Step	Hyp	Ref	Expression
1		grpinvinv.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐺)
2		grpinvinv.n	. . . . 5 ⊢ 𝑁 = (inv_g‘𝐺)
3	1, 2	grpinvcl 19198	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵)
4		eqid 2761	. . . . 5 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
5		eqid 2761	. . . . 5 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
6	1, 4, 5, 2	grprinv 19201	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (𝑁‘𝑋) ∈ 𝐵) → ((𝑁‘𝑋)(+_g‘𝐺)(𝑁‘(𝑁‘𝑋))) = (0_g‘𝐺))
7	3, 6	syldan 603	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑁‘𝑋)(+_g‘𝐺)(𝑁‘(𝑁‘𝑋))) = (0_g‘𝐺))
8	1, 4, 5, 2	grplinv 19200	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑁‘𝑋)(+_g‘𝐺)𝑋) = (0_g‘𝐺))
9	7, 8	eqtr4d 2799	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑁‘𝑋)(+_g‘𝐺)(𝑁‘(𝑁‘𝑋))) = ((𝑁‘𝑋)(+_g‘𝐺)𝑋))
10		simpl 488	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → 𝐺 ∈ Grp)
11	1, 2	grpinvcl 19198	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (𝑁‘𝑋) ∈ 𝐵) → (𝑁‘(𝑁‘𝑋)) ∈ 𝐵)
12	3, 11	syldan 603	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝑁‘𝑋)) ∈ 𝐵)
13		simpr 490	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵)
14	1, 4	grplcan 19211	. . 3 ⊢ ((𝐺 ∈ Grp ∧ ((𝑁‘(𝑁‘𝑋)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑁‘𝑋) ∈ 𝐵)) → (((𝑁‘𝑋)(+_g‘𝐺)(𝑁‘(𝑁‘𝑋))) = ((𝑁‘𝑋)(+_g‘𝐺)𝑋) ↔ (𝑁‘(𝑁‘𝑋)) = 𝑋))
15	10, 12, 13, 3, 14	syl13anc 1399	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (((𝑁‘𝑋)(+_g‘𝐺)(𝑁‘(𝑁‘𝑋))) = ((𝑁‘𝑋)(+_g‘𝐺)𝑋) ↔ (𝑁‘(𝑁‘𝑋)) = 𝑋))
16	9, 15	mpbid 235	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝑁‘𝑋)) = 𝑋)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ‘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 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 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 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: grpinv11 19218 grpinvnz 19220 grpsubinv 19222 grpinvsub 19232 grpsubeq0 19236 grpnpcan 19242 mulgneg 19302 mulgnegneg 19303 mulginvinv 19310 mulgdir 19316 mulgass 19321 eqger 19390 frgpuptinv 19985 ablsub2inv 20022 mulgdi 20040 invghm 20047 rngm2neg 20391 unitinvinv 20621 unitnegcl 20627 irrednegb 20661 abvneg 21083 lspsnneg 21281 islindf4 22144 tgpconncomp 24432 grpinvinvd 33601 archirngz 33750 archiabllem1b 33753 ply1divalg3 36407 baerlem5amN 42773 baerlem5bmN 42774 baerlem5abmN 42775 fldhmf1 43140 nelsubginvcld 43560

W3C validator