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 19185

Description: The identity element of a group is a left identity. Deduction associated with grplid 19183. (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 19183	. 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 1569 ∈ wcel 2144 ‘cfv 6538 (class class class)co 7420 Basecbs 17392 +_gcplusg 17433 0_gc0g 17615 Grpcgrp 19149

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pr 5390

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-iota 6494 df-fun 6540 df-fv 6546 df-riota 7377 df-ov 7423 df-0g 17617 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-grp 19152

This theorem is used by: eqger 19395 conjnmz 19471 rngqiprngimfolem 21591 rngqiprngfulem5 21616 qsnzr 21644 ofldchr 21887 mhpaddcl 22477 r1pid2 26485 conjga 33777 erler 33872 rlocaddval 33876 rlocmulval 33877 rloccring 33878 rloc0g 33879 qsdrngilem 34064 drnglring 34070 ressply1evls1 34143 mplgsum 34231 esplyind 34253 dimkerim 34305 rtelextdg2lem 34404 primrootspoweq0 43249 aks6d1c6lem5 43320 grpcominv1 43668

W3C validator