grpolid - Metamath Proof Explorer

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

Theorem grpolid 30868

Description: The identity element of a group is a left identity. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
grpoidval.1	⊢ 𝑋 = ran 𝐺
grpoidval.2	⊢ 𝑈 = (GId‘𝐺)

**Assertion**
Ref	Expression
grpolid	⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑈𝐺𝐴) = 𝐴)

Proof of Theorem grpolid Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		grpoidval.1	. . 3 ⊢ 𝑋 = ran 𝐺
2		grpoidval.2	. . 3 ⊢ 𝑈 = (GId‘𝐺)
3	1, 2	grpoidinv2 30867	. 2 ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
4	3	simplld 779	1 ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑈𝐺𝐴) = 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ∃wrex 3089 ran crn 5662 ‘cfv 6536 (class class class)co 7410 GrpOpcgr 30841 GIdcgi 30842

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pr 5404 ax-un 7732

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-id 5556 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-fo 6542 df-fv 6544 df-riota 7367 df-ov 7413 df-grpo 30845 df-gid 30846

This theorem is referenced by: grpoid 30872 grpoinvid1 30880 grpoinvid2 30881 grpolcan 30882 grpoinvop 30885 ablonncan 30908 vcm 30928 nv0lid 30988 hhssabloilem 31613 grpoeqdivid 38552 ghomidOLD 38560 rngo0lid 38592 rngolz 38593 rngorz 38594 keridl 38703

W3C validator