grpridd - Metamath Proof Explorer

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

Theorem grpridd 19210

Description: The identity element of a group is a right identity. Deduction associated with grprid 19208. (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
grpridd	⊢ (𝜑 → (𝑋 + 0 ) = 𝑋)

**Proof of Theorem grpridd**
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	grprid 19208	. 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: grprcan 19213 ghmqusnsglem1 19524 ablsubaddsub 20058 rnglidlmcl 21525 rloccring 33902 ressply1evls1 34167 evl1deg1 34178 evl1deg2 34179 evl1deg3 34180 mplgsum 34255 esplyind 34277 esplyfvn 34279 irredminply 34418 rtelextdg2lem 34428 primrootscoprmpow 43341 primrootscoprbij 43344

W3C validator