grplidd - Metamath Proof Explorer

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

Theorem grplidd 19209

Description: The identity element of a group is a left identity. Deduction associated with grplid 19207. (Contributed by SN, 29-Jan-2025.)

**Hypotheses**
Ref	Expression
grpbn0.b	⊢ 𝐵 = (Base‘𝐺)
grplid.p	⊢ + = (+_g‘𝐺)
grplid.o	⊢ 0 = (0_g‘𝐺)
grplidd.g	⊢ (𝜑 → 𝐺 ∈ Grp)
grplidd.1	⊢ (𝜑 → 𝑋 ∈ 𝐵)

**Assertion**
Ref	Expression
grplidd	⊢ (𝜑 → ( 0 + 𝑋) = 𝑋)

**Proof of Theorem grplidd**
Step	Hyp	Ref	Expression
1		grplidd.g	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
2		grplidd.1	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
3		grpbn0.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
4		grplid.p	. . 3 ⊢ + = (+_g‘𝐺)
5		grplid.o	. . 3 ⊢ 0 = (0_g‘𝐺)
6	3, 4, 5	grplid 19207	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
7	1, 2, 6	syl2anc 596	1 ⊢ (𝜑 → ( 0 + 𝑋) = 𝑋)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2147 ‘cfv 6558 (class class class)co 7443 Basecbs 17416 +_gcplusg 17457 0_gc0g 17639 Grpcgrp 19173

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pr 5395

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-br 5107 df-opab 5171 df-mpt 5190 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-iota 6512 df-fun 6560 df-fv 6566 df-riota 7400 df-ov 7446 df-0g 17641 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-grp 19176

This theorem is used by: eqger 19419 conjnmz 19495 rngqiprngimfolem 21616 rngqiprngfulem5 21641 qsnzr 21669 ofldchr 21912 mhpaddcl 22502 r1pid2 26510 conjga 33801 erler 33896 rlocaddval 33900 rlocmulval 33901 rloccring 33902 rloc0g 33903 qsdrngilem 34088 drnglring 34094 ressply1evls1 34167 mplgsum 34255 esplyind 34277 dimkerim 34329 rtelextdg2lem 34428 primrootspoweq0 43348 aks6d1c6lem5 43419 grpcominv1 43768

W3C validator