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 19160

Description: The identity element of a group is a left identity. Deduction associated with grplid 19158. (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 19158	. 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 2145 ‘cfv 6531 (class class class)co 7412 Basecbs 17367 +_gcplusg 17408 0_gc0g 17590 Grpcgrp 19124

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-pr 5391

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-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-iota 6487 df-fun 6533 df-fv 6539 df-riota 7369 df-ov 7415 df-0g 17592 df-mgm 18796 df-sgrp 18888 df-mnd 18904 df-grp 19127

This theorem is used by: eqger 19370 conjnmz 19446 rngqiprngimfolem 21566 rngqiprngfulem5 21591 qsnzr 21619 ofldchr 21862 mhpaddcl 22452 r1pid2 26460 conjga 33713 erler 33808 rlocaddval 33812 rlocmulval 33813 rloccring 33814 rloc0g 33815 qsdrngilem 34000 drnglring 34006 ressply1evls1 34079 mplgsum 34167 esplyind 34189 dimkerim 34241 rtelextdg2lem 34340 primrootspoweq0 43124 aks6d1c6lem5 43195 grpcominv1 43540

W3C validator