This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = 𝐼 ) )