Theorem grpinvid1 18923

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

Hypotheses

Ref	Expression
grpinv.b	⊢ 𝐵 = (Base‘𝐺)
grpinv.p	⊢ + = (+g‘𝐺)
grpinv.u	⊢ 0 = (0g‘𝐺)
grpinv.n	⊢ 𝑁 = (invg‘𝐺)

Assertion

Ref	Expression
grpinvid1	⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) = 𝑌 ↔ (𝑋 + 𝑌) = 0 ))

Proof of Theorem grpinvid1

Step	Hyp	Ref	Expression
1		oveq2 7366	. . . 4 ⊢ ((𝑁‘𝑋) = 𝑌 → (𝑋 + (𝑁‘𝑋)) = (𝑋 + 𝑌))
2	1	adantl 481	. . 3 ⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑁‘𝑋) = 𝑌) → (𝑋 + (𝑁‘𝑋)) = (𝑋 + 𝑌))
3		grpinv.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
4		grpinv.p	. . . . . 6 ⊢ + = (+g‘𝐺)
5		grpinv.u	. . . . . 6 ⊢ 0 = (0g‘𝐺)
6		grpinv.n	. . . . . 6 ⊢ 𝑁 = (invg‘𝐺)
7	3, 4, 5, 6	grprinv 18922	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + (𝑁‘𝑋)) = 0 )
8	7	3adant3 1132	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + (𝑁‘𝑋)) = 0 )
9	8	adantr 480	. . 3 ⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑁‘𝑋) = 𝑌) → (𝑋 + (𝑁‘𝑋)) = 0 )
10	2, 9	eqtr3d 2773	. 2 ⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑁‘𝑋) = 𝑌) → (𝑋 + 𝑌) = 0 )
11		oveq2 7366	. . . 4 ⊢ ((𝑋 + 𝑌) = 0 → ((𝑁‘𝑋) + (𝑋 + 𝑌)) = ((𝑁‘𝑋) + 0 ))
12	11	adantl 481	. . 3 ⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 + 𝑌) = 0 ) → ((𝑁‘𝑋) + (𝑋 + 𝑌)) = ((𝑁‘𝑋) + 0 ))
13	3, 4, 5, 6	grplinv 18921	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑁‘𝑋) + 𝑋) = 0 )
14	13	oveq1d 7373	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (((𝑁‘𝑋) + 𝑋) + 𝑌) = ( 0 + 𝑌))
15	14	3adant3 1132	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((𝑁‘𝑋) + 𝑋) + 𝑌) = ( 0 + 𝑌))
16	3, 6	grpinvcl 18919	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵)
17	16	adantrr 717	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑁‘𝑋) ∈ 𝐵)
18		simprl 770	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
19		simprr 772	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
20	17, 18, 19	3jca 1128	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁‘𝑋) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
21	3, 4	grpass 18874	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ ((𝑁‘𝑋) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝑁‘𝑋) + 𝑋) + 𝑌) = ((𝑁‘𝑋) + (𝑋 + 𝑌)))
22	20, 21	syldan 591	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝑁‘𝑋) + 𝑋) + 𝑌) = ((𝑁‘𝑋) + (𝑋 + 𝑌)))
23	22	3impb 1114	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((𝑁‘𝑋) + 𝑋) + 𝑌) = ((𝑁‘𝑋) + (𝑋 + 𝑌)))
24	15, 23	eqtr3d 2773	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( 0 + 𝑌) = ((𝑁‘𝑋) + (𝑋 + 𝑌)))
25	3, 4, 5	grplid 18899	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵) → ( 0 + 𝑌) = 𝑌)
26	25	3adant2 1131	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( 0 + 𝑌) = 𝑌)
27	24, 26	eqtr3d 2773	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) + (𝑋 + 𝑌)) = 𝑌)
28	27	adantr 480	. . 3 ⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 + 𝑌) = 0 ) → ((𝑁‘𝑋) + (𝑋 + 𝑌)) = 𝑌)
29	3, 4, 5	grprid 18900	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑁‘𝑋) ∈ 𝐵) → ((𝑁‘𝑋) + 0 ) = (𝑁‘𝑋))
30	16, 29	syldan 591	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑁‘𝑋) + 0 ) = (𝑁‘𝑋))
31	30	3adant3 1132	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) + 0 ) = (𝑁‘𝑋))
32	31	adantr 480	. . 3 ⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 + 𝑌) = 0 ) → ((𝑁‘𝑋) + 0 ) = (𝑁‘𝑋))
33	12, 28, 32	3eqtr3rd 2780	. 2 ⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 + 𝑌) = 0 ) → (𝑁‘𝑋) = 𝑌)
34	10, 33	impbida 800	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) = 𝑌 ↔ (𝑋 + 𝑌) = 0 ))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  (class class class)co 7358  Basecbs 17138  +_gcplusg 17179  0_gc0g 17361  Grpcgrp 18865  inv_gcminusg 18866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-riota 7315  df-ov 7361  df-0g 17363  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-grp 18868  df-minusg 18869

This theorem is referenced by:  grpinvid  18931  grpinvcnv  18938  grpinvadd  18950  subginv  19065  qusinv  19121  ghminv  19154  symginv  19333  frgpinv  19695  cnaddinv  19802  rngmneg1  20104  ringnegl  20239  lmodindp1  20967  lmodvsinv2  20991  cnfldneg  21352  zringinvg  21422  mdetunilem6  22563  invrvald  22622  dchrinv  27230  elrgspnlem1  33326  baerlem3lem1  41989