Theorem ringid

Description: The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-Dec-2013) (Revised by AV, 24-Aug-2021)

	Ref	Expression
Hypotheses	ringid.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringid.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	ringid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ( ( 𝑢 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 𝑢 ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ringid.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringid.t	⊢ · = ( .r ‘ 𝑅 )
3		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4	1 3	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
5	4	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
6		oveq1	⊢ ( 𝑢 = ( 1r ‘ 𝑅 ) → ( 𝑢 · 𝑋 ) = ( ( 1r ‘ 𝑅 ) · 𝑋 ) )
7	6	eqeq1d	⊢ ( 𝑢 = ( 1r ‘ 𝑅 ) → ( ( 𝑢 · 𝑋 ) = 𝑋 ↔ ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 ) )
8		oveq2	⊢ ( 𝑢 = ( 1r ‘ 𝑅 ) → ( 𝑋 · 𝑢 ) = ( 𝑋 · ( 1r ‘ 𝑅 ) ) )
9	8	eqeq1d	⊢ ( 𝑢 = ( 1r ‘ 𝑅 ) → ( ( 𝑋 · 𝑢 ) = 𝑋 ↔ ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 ) )
10	7 9	anbi12d	⊢ ( 𝑢 = ( 1r ‘ 𝑅 ) → ( ( ( 𝑢 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 𝑢 ) = 𝑋 ) ↔ ( ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 ∧ ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 ) ) )
11	10	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑢 = ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑢 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 𝑢 ) = 𝑋 ) ↔ ( ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 ∧ ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 ) ) )
12	1 2 3	ringidmlem	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 ∧ ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 ) )
13	5 11 12	rspcedvd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ( ( 𝑢 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 𝑢 ) = 𝑋 ) )