![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cmn4 | Structured version Visualization version GIF version |
Description: Commutative/associative law for Abelian groups. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
Ref | Expression |
---|---|
ablcom.b | ⊢ 𝐵 = (Base‘𝐺) |
ablcom.p | ⊢ + = (+g‘𝐺) |
Ref | Expression |
---|---|
cmn4 | ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ablcom.b | . 2 ⊢ 𝐵 = (Base‘𝐺) | |
2 | ablcom.p | . 2 ⊢ + = (+g‘𝐺) | |
3 | simp1 1172 | . . 3 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝐺 ∈ CMnd) | |
4 | cmnmnd 18560 | . . 3 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) | |
5 | 3, 4 | syl 17 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝐺 ∈ Mnd) |
6 | simp2l 1262 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝑋 ∈ 𝐵) | |
7 | simp2r 1263 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝑌 ∈ 𝐵) | |
8 | simp3l 1264 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝑍 ∈ 𝐵) | |
9 | simp3r 1265 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝑊 ∈ 𝐵) | |
10 | 1, 2 | cmncom 18561 | . . 3 ⊢ ((𝐺 ∈ CMnd ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑍 + 𝑌)) |
11 | 3, 7, 8, 10 | syl3anc 1496 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (𝑌 + 𝑍) = (𝑍 + 𝑌)) |
12 | 1, 2, 5, 6, 7, 8, 9, 11 | mnd4g 17659 | 1 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 = wceq 1658 ∈ wcel 2166 ‘cfv 6122 (class class class)co 6904 Basecbs 16221 +gcplusg 16304 Mndcmnd 17646 CMndccmn 18545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-nul 5012 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-sbc 3662 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-iota 6085 df-fv 6130 df-ov 6907 df-mgm 17594 df-sgrp 17636 df-mnd 17647 df-cmn 18547 |
This theorem is referenced by: ablsub4 18570 ghmplusg 18601 lmod4 19268 evlslem1 19874 ip2di 20347 clmsub4 23274 lfladdcl 35145 |
Copyright terms: Public domain | W3C validator |