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 = { 〈 𝑔 , ℎ 〉 ∣ ∀ 𝑎 ∈ ran 𝑔 ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccm2 | ⊢ Com2 | |
1 | vg | ⊢ 𝑔 | |
2 | vh | ⊢ ℎ | |
3 | va | ⊢ 𝑎 | |
4 | 1 | cv | ⊢ 𝑔 |
5 | 4 | crn | ⊢ ran 𝑔 |
6 | vb | ⊢ 𝑏 | |
7 | 3 | cv | ⊢ 𝑎 |
8 | 2 | cv | ⊢ ℎ |
9 | 6 | cv | ⊢ 𝑏 |
10 | 7 9 8 | co | ⊢ ( 𝑎 ℎ 𝑏 ) |
11 | 9 7 8 | co | ⊢ ( 𝑏 ℎ 𝑎 ) |
12 | 10 11 | wceq | ⊢ ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 ) |
13 | 12 6 5 | wral | ⊢ ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 ) |
14 | 13 3 5 | wral | ⊢ ∀ 𝑎 ∈ ran 𝑔 ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 ) |
15 | 14 1 2 | copab | ⊢ { 〈 𝑔 , ℎ 〉 ∣ ∀ 𝑎 ∈ ran 𝑔 ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 ) } |
16 | 0 15 | wceq | ⊢ Com2 = { 〈 𝑔 , ℎ 〉 ∣ ∀ 𝑎 ∈ ran 𝑔 ∀ 𝑏 ∈ ran 𝑔 ( 𝑎 ℎ 𝑏 ) = ( 𝑏 ℎ 𝑎 ) } |