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 19068

Description: The identity element of a group is a right identity. Deduction associated with grprid 19066. (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 19066	. 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 2146 ‘cfv 6543 (class class class)co 7423 Basecbs 17294 +_gcplusg 17335 0_gc0g 17517 Grpcgrp 19031

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pr 5409

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-iota 6499 df-fun 6545 df-fv 6551 df-riota 7380 df-ov 7426 df-0g 17519 df-mgm 18723 df-sgrp 18806 df-mnd 18822 df-grp 19034

This theorem is used by: grprcan 19071 ghmqusnsglem1 19381 ablsubaddsub 19915 rnglidlmcl 21378 rloccring 33622 ressply1evls1 33886 evl1deg1 33897 evl1deg2 33898 evl1deg3 33899 mplgsum 33974 esplyind 33996 esplyfvn 33998 irredminply 34137 rtelextdg2lem 34147 primrootscoprmpow 42906 primrootscoprbij 42909

W3C validator