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 19186

Description: The identity element of a group is a right identity. Deduction associated with grprid 19184. (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 19184	. 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: grprcan 19189 ghmqusnsglem1 19499 ablsubaddsub 20033 rnglidlmcl 21500 rloccring 33878 ressply1evls1 34143 evl1deg1 34154 evl1deg2 34155 evl1deg3 34156 mplgsum 34231 esplyind 34253 esplyfvn 34255 irredminply 34394 rtelextdg2lem 34404 primrootscoprmpow 43242 primrootscoprbij 43245

W3C validator