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