Metamath Proof Explorer

Definition df-rngo

Description: Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006) (New usage is discouraged.)

Ref Expression
Assertion df-rngo RingOps = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crngo ⊢ RingOps
1 vg ⊢ 𝑔
2 vh ⊢ ℎ
3 1 cv ⊢ 𝑔
4 cablo ⊢ AbelOp
5 3 4 wcel ⊢ 𝑔 ∈ AbelOp
6 2 cv ⊢ ℎ
7 3 crn ⊢ ran 𝑔
8 7 7 cxp ⊢ ( ran 𝑔 × ran 𝑔 )
9 8 7 6 wf ⊢ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔
10 5 9 wa ⊢ ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 )
11 vx ⊢ 𝑥
12 vy ⊢ 𝑦
13 vz ⊢ 𝑧
14 11 cv ⊢ 𝑥
15 12 cv ⊢ 𝑦
16 14 15 6 co ⊢ ( 𝑥 ℎ 𝑦 )
17 13 cv ⊢ 𝑧
18 16 17 6 co ⊢ ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 )
19 15 17 6 co ⊢ ( 𝑦 ℎ 𝑧 )
20 14 19 6 co ⊢ ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) )
21 18 20 wceq ⊢ ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) )
22 15 17 3 co ⊢ ( 𝑦 𝑔 𝑧 )
23 14 22 6 co ⊢ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) )
24 14 17 6 co ⊢ ( 𝑥 ℎ 𝑧 )
25 16 24 3 co ⊢ ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) )
26 23 25 wceq ⊢ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) )
27 14 15 3 co ⊢ ( 𝑥 𝑔 𝑦 )
28 27 17 6 co ⊢ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 )
29 24 19 3 co ⊢ ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) )
30 28 29 wceq ⊢ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) )
31 21 26 30 w3a ⊢ ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) )
32 31 13 7 wral ⊢ ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) )
33 32 12 7 wral ⊢ ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) )
34 33 11 7 wral ⊢ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) )
35 16 15 wceq ⊢ ( 𝑥 ℎ 𝑦 ) = 𝑦
36 15 14 6 co ⊢ ( 𝑦 ℎ 𝑥 )
37 36 15 wceq ⊢ ( 𝑦 ℎ 𝑥 ) = 𝑦
38 35 37 wa ⊢ ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 )
39 38 12 7 wral ⊢ ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 )
40 39 11 7 wrex ⊢ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 )
41 34 40 wa ⊢ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) )
42 10 41 wa ⊢ ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) )
43 42 1 2 copab ⊢ { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ) }
44 0 43 wceq ⊢ RingOps = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ) }