Metamath Proof Explorer

Definition df-com2

Description: A device to add commutativity to various sorts of rings. I use ran g because I suppose g has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009) (New usage is discouraged.)

Ref Expression
Assertion df-com2 ⊢ Com2 = g h | ∀ a ∈ ran ⁡ g ∀ b ∈ ran ⁡ g a h b = b h a

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccm2 class Com2
1 vg setvar g
2 vh setvar h
3 va setvar a
4 1 cv setvar g
5 4 crn class ran ⁡ g
6 vb setvar b
7 3 cv setvar a
8 2 cv setvar h
9 6 cv setvar b
10 7 9 8 co class a h b
11 9 7 8 co class b h a
12 10 11 wceq wff a h b = b h a
13 12 6 5 wral wff ∀ b ∈ ran ⁡ g a h b = b h a
14 13 3 5 wral wff ∀ a ∈ ran ⁡ g ∀ b ∈ ran ⁡ g a h b = b h a
15 14 1 2 copab class g h | ∀ a ∈ ran ⁡ g ∀ b ∈ ran ⁡ g a h b = b h a
16 0 15 wceq wff Com2 = g h | ∀ a ∈ ran ⁡ g ∀ b ∈ ran ⁡ g a h b = b h a