| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cmnbascntr.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
| 2 |
|
cmnbascntr.z |
⊢ 𝑍 = ( Cntr ‘ 𝐺 ) |
| 3 |
|
eqid |
⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 ) |
| 4 |
1 3
|
cntrval |
⊢ ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = ( Cntr ‘ 𝐺 ) |
| 5 |
|
ssid |
⊢ 𝐵 ⊆ 𝐵 |
| 6 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
| 7 |
1 6 3
|
cntzval |
⊢ ( 𝐵 ⊆ 𝐵 → ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) } ) |
| 8 |
5 7
|
ax-mp |
⊢ ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) } |
| 9 |
2 4 8
|
3eqtr2i |
⊢ 𝑍 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) } |
| 10 |
1 6
|
cmncom |
⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) |
| 11 |
10
|
3expa |
⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) |
| 12 |
11
|
ralrimiva |
⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) |
| 13 |
12
|
rabeqcda |
⊢ ( 𝐺 ∈ CMnd → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) } = 𝐵 ) |
| 14 |
9 13
|
eqtr2id |
⊢ ( 𝐺 ∈ CMnd → 𝐵 = 𝑍 ) |