Metamath Proof Explorer


Theorem issrgid

Description: Properties showing that an element I is the unity element of a semiring. (Contributed by NM, 7-Aug-2013) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses srgidm.b 𝐵 = ( Base ‘ 𝑅 )
srgidm.t · = ( .r𝑅 )
srgidm.u 1 = ( 1r𝑅 )
Assertion issrgid ( 𝑅 ∈ SRing → ( ( 𝐼𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) ) ↔ 1 = 𝐼 ) )

Proof

Step Hyp Ref Expression
1 srgidm.b 𝐵 = ( Base ‘ 𝑅 )
2 srgidm.t · = ( .r𝑅 )
3 srgidm.u 1 = ( 1r𝑅 )
4 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5 4 1 mgpbas 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
6 4 3 ringidval 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
7 4 2 mgpplusg · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
8 1 2 srgideu ( 𝑅 ∈ SRing → ∃! 𝑦𝐵𝑥𝐵 ( ( 𝑦 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑦 ) = 𝑥 ) )
9 reurex ( ∃! 𝑦𝐵𝑥𝐵 ( ( 𝑦 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑦 ) = 𝑥 ) → ∃ 𝑦𝐵𝑥𝐵 ( ( 𝑦 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑦 ) = 𝑥 ) )
10 8 9 syl ( 𝑅 ∈ SRing → ∃ 𝑦𝐵𝑥𝐵 ( ( 𝑦 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑦 ) = 𝑥 ) )
11 5 6 7 10 ismgmid ( 𝑅 ∈ SRing → ( ( 𝐼𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) ) ↔ 1 = 𝐼 ) )