Metamath Proof Explorer

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 ⊢ G = 1 st ⁡ R
ringi.2 ⊢ H = 2 nd ⁡ R
ringi.3 ⊢ X = ran ⁡ G
Assertion rngoid ⊢ R ∈ RingOps ∧ A ∈ X → ∃ u ∈ X u H A = A ∧ A H u = A

Proof

Step Hyp Ref Expression
1 ringi.1 ⊢ G = 1 st ⁡ R
2 ringi.2 ⊢ H = 2 nd ⁡ R
3 ringi.3 ⊢ X = ran ⁡ G
4 1 2 3 rngoi ⊢ R ∈ RingOps → G ∈ AbelOp ∧ H : X × X ⟶ X ∧ ∀ u ∈ X ∀ x ∈ X ∀ y ∈ X u H x H y = u H x H y ∧ u H x G y = u H x G u H y ∧ u G x H y = u H y G x H y ∧ ∃ u ∈ X ∀ x ∈ X u H x = x ∧ x H u = x
5 4 simprrd ⊢ R ∈ RingOps → ∃ u ∈ X ∀ x ∈ X u H x = x ∧ x H u = x
6 r19.12 ⊢ ∃ u ∈ X ∀ x ∈ X u H x = x ∧ x H u = x → ∀ x ∈ X ∃ u ∈ X u H x = x ∧ x H u = x
7 5 6 syl ⊢ R ∈ RingOps → ∀ x ∈ X ∃ u ∈ X u H x = x ∧ x H u = x
8 oveq2 ⊢ x = A → u H x = u H A
9 id ⊢ x = A → x = A
10 8 9 eqeq12d ⊢ x = A → u H x = x ↔ u H A = A
11 oveq1 ⊢ x = A → x H u = A H u
12 11 9 eqeq12d ⊢ x = A → x H u = x ↔ A H u = A
13 10 12 anbi12d ⊢ x = A → u H x = x ∧ x H u = x ↔ u H A = A ∧ A H u = A
14 13 rexbidv ⊢ x = A → ∃ u ∈ X u H x = x ∧ x H u = x ↔ ∃ u ∈ X u H A = A ∧ A H u = A
15 14 rspccva ⊢ ∀ x ∈ X ∃ u ∈ X u H x = x ∧ x H u = x ∧ A ∈ X → ∃ u ∈ X u H A = A ∧ A H u = A
16 7 15 sylan ⊢ R ∈ RingOps ∧ A ∈ X → ∃ u ∈ X u H A = A ∧ A H u = A