Metamath Proof Explorer

Theorem rngoi

Description: The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007) (Proof shortened by Mario Carneiro, 21-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 rngoi ⊢ R ∈ RingOps → G ∈ AbelOp ∧ H : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z ∧ ∃ x ∈ X ∀ y ∈ X x H y = y ∧ y H x = y

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 opeq12i ⊢ G H = 1 st ⁡ R 2 nd ⁡ R
5 relrngo ⊢ Rel ⁡ RingOps
6 1st2nd ⊢ Rel ⁡ RingOps ∧ R ∈ RingOps → R = 1 st ⁡ R 2 nd ⁡ R
7 5 6 mpan ⊢ R ∈ RingOps → R = 1 st ⁡ R 2 nd ⁡ R
8 4 7 eqtr4id ⊢ R ∈ RingOps → G H = R
9 id ⊢ R ∈ RingOps → R ∈ RingOps
10 8 9 eqeltrd ⊢ R ∈ RingOps → G H ∈ RingOps
11 2 fvexi ⊢ H ∈ V
12 3 isrngo ⊢ H ∈ V → G H ∈ RingOps ↔ G ∈ AbelOp ∧ H : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z ∧ ∃ x ∈ X ∀ y ∈ X x H y = y ∧ y H x = y
13 11 12 ax-mp ⊢ G H ∈ RingOps ↔ G ∈ AbelOp ∧ H : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z ∧ ∃ x ∈ X ∀ y ∈ X x H y = y ∧ y H x = y
14 10 13 sylib ⊢ R ∈ RingOps → G ∈ AbelOp ∧ H : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z ∧ ∃ x ∈ X ∀ y ∈ X x H y = y ∧ y H x = y