![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ablcom | Structured version Visualization version GIF version |
Description: An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.) |
Ref | Expression |
---|---|
ablcom.b | ⊢ 𝐵 = (Base‘𝐺) |
ablcom.p | ⊢ + = (+g‘𝐺) |
Ref | Expression |
---|---|
ablcom | ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ablcmn 19639 | . 2 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd) | |
2 | ablcom.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | ablcom.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | cmncom 19650 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) |
5 | 1, 4 | syl3an1 1164 | 1 ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ‘cfv 6535 (class class class)co 7396 Basecbs 17131 +gcplusg 17184 CMndccmn 19632 Abelcabl 19633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4905 df-br 5145 df-iota 6487 df-fv 6543 df-ov 7399 df-cmn 19634 df-abl 19635 |
This theorem is referenced by: ablinvadd 19658 ablsub2inv 19659 ablsubadd 19660 abladdsub 19663 ablsubaddsub 19665 ablpncan3 19667 ablsub32 19672 ablnnncan 19673 ablsubsub23 19675 eqgabl 19685 subgabl 19687 ablnsg 19698 lsmcomx 19707 qusabl 19716 frgpnabl 19726 imasabl 19727 ngplcan 24089 clmnegsubdi2 24590 clmvsubval2 24595 ncvspi 24642 r1pid 25646 abliso 32168 lindsunlem 32647 cnaddcom 37748 toycom 37749 lflsub 37843 lfladdcom 37848 subrngringnsg 46603 |
Copyright terms: Public domain | W3C validator |