Metamath Proof Explorer

Definition df-grpo

Description: Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of Herstein p. 54. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)

Ref Expression
Assertion df-grpo GrpOp = { 𝑔 ∣ ∃ 𝑡 ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgr ⊢ GrpOp
1 vg ⊢ 𝑔
2 vt ⊢ 𝑡
3 1 cv ⊢ 𝑔
4 2 cv ⊢ 𝑡
5 4 4 cxp ⊢ ( 𝑡 × 𝑡 )
6 5 4 3 wf ⊢ 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡
7 vx ⊢ 𝑥
8 vy ⊢ 𝑦
9 vz ⊢ 𝑧
10 7 cv ⊢ 𝑥
11 8 cv ⊢ 𝑦
12 10 11 3 co ⊢ ( 𝑥 𝑔 𝑦 )
13 9 cv ⊢ 𝑧
14 12 13 3 co ⊢ ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 )
15 11 13 3 co ⊢ ( 𝑦 𝑔 𝑧 )
16 10 15 3 co ⊢ ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
17 14 16 wceq ⊢ ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
18 17 9 4 wral ⊢ ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
19 18 8 4 wral ⊢ ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
20 19 7 4 wral ⊢ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) )
21 vu ⊢ 𝑢
22 21 cv ⊢ 𝑢
23 22 10 3 co ⊢ ( 𝑢 𝑔 𝑥 )
24 23 10 wceq ⊢ ( 𝑢 𝑔 𝑥 ) = 𝑥
25 11 10 3 co ⊢ ( 𝑦 𝑔 𝑥 )
26 25 22 wceq ⊢ ( 𝑦 𝑔 𝑥 ) = 𝑢
27 26 8 4 wrex ⊢ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢
28 24 27 wa ⊢ ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 )
29 28 7 4 wral ⊢ ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 )
30 29 21 4 wrex ⊢ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 )
31 6 20 30 w3a ⊢ ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) )
32 31 2 wex ⊢ ∃ 𝑡 ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) )
33 32 1 cab ⊢ { 𝑔 ∣ ∃ 𝑡 ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) ) }
34 0 33 wceq ⊢ GrpOp = { 𝑔 ∣ ∃ 𝑡 ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) ) }