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 19100

Description: The identity element of a group is a right identity. Deduction associated with grprid 19098. (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 19098	. 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 6537 (class class class)co 7417 Basecbs 17307 +_gcplusg 17348 0_gc0g 17530 Grpcgrp 19063

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 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pr 5402

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-br 5108 df-opab 5172 df-mpt 5191 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-iota 6493 df-fun 6539 df-fv 6545 df-riota 7374 df-ov 7420 df-0g 17532 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-grp 19066

This theorem is used by: grprcan 19103 ghmqusnsglem1 19413 ablsubaddsub 19947 rnglidlmcl 21410 rloccring 33719 ressply1evls1 33983 evl1deg1 33994 evl1deg2 33995 evl1deg3 33996 mplgsum 34071 esplyind 34093 esplyfvn 34095 irredminply 34234 rtelextdg2lem 34244 primrootscoprmpow 42973 primrootscoprbij 42976

W3C validator