Theorem rngoid

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) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringi.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	ringi.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	ringi.3	⊢ 𝑋 = ran 𝐺
Assertion	rngoid	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ringi.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		ringi.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		ringi.3	⊢ 𝑋 = ran 𝐺
4	1 2 3	rngoi	⊢ ( 𝑅 ∈ RingOps → ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑢 𝐻 𝑥 ) 𝐻 𝑦 ) = ( 𝑢 𝐻 ( 𝑥 𝐻 𝑦 ) ) ∧ ( 𝑢 𝐻 ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑢 𝐻 𝑥 ) 𝐺 ( 𝑢 𝐻 𝑦 ) ) ∧ ( ( 𝑢 𝐺 𝑥 ) 𝐻 𝑦 ) = ( ( 𝑢 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑦 ) ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) ) )
5	4	simprrd	⊢ ( 𝑅 ∈ RingOps → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
6		r19.12	⊢ ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
7	5 6	syl	⊢ ( 𝑅 ∈ RingOps → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
8		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑢 𝐻 𝑥 ) = ( 𝑢 𝐻 𝐴 ) )
9		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
10	8 9	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑢 𝐻 𝐴 ) = 𝐴 ) )
11		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐻 𝑢 ) = ( 𝐴 𝐻 𝑢 ) )
12	11 9	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐻 𝑢 ) = 𝑥 ↔ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) )
13	10 12	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ( ( 𝑢 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) ) )
14	13	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) ) )
15	14	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) )
16	7 15	sylan	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) )