![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cmn4 | GIF version |
Description: Commutative/associative law for commutative monoids. (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 999 | . . 3 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝐺 ∈ CMnd) | |
4 | cmnmnd 13374 | . . 3 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) | |
5 | 3, 4 | syl 14 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝐺 ∈ Mnd) |
6 | simp2l 1025 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝑋 ∈ 𝐵) | |
7 | simp2r 1026 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝑌 ∈ 𝐵) | |
8 | simp3l 1027 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝑍 ∈ 𝐵) | |
9 | simp3r 1028 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → 𝑊 ∈ 𝐵) | |
10 | 1, 2 | cmncom 13375 | . . 3 ⊢ ((𝐺 ∈ CMnd ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑍 + 𝑌)) |
11 | 3, 7, 8, 10 | syl3anc 1249 | . 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (𝑌 + 𝑍) = (𝑍 + 𝑌)) |
12 | 1, 2, 5, 6, 7, 8, 9, 11 | mnd4g 13013 | 1 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 = wceq 1364 ∈ wcel 2164 ‘cfv 5255 (class class class)co 5919 Basecbs 12621 +gcplusg 12698 Mndcmnd 13000 CMndccmn 13357 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4148 ax-pow 4204 ax-pr 4239 ax-un 4465 ax-cnex 7965 ax-resscn 7966 ax-1re 7968 ax-addrcl 7971 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ral 2477 df-rex 2478 df-rab 2481 df-v 2762 df-sbc 2987 df-un 3158 df-in 3160 df-ss 3167 df-pw 3604 df-sn 3625 df-pr 3626 df-op 3628 df-uni 3837 df-int 3872 df-br 4031 df-opab 4092 df-mpt 4093 df-id 4325 df-xp 4666 df-rel 4667 df-cnv 4668 df-co 4669 df-dm 4670 df-rn 4671 df-res 4672 df-iota 5216 df-fun 5257 df-fn 5258 df-fv 5263 df-ov 5922 df-inn 8985 df-2 9043 df-ndx 12624 df-slot 12625 df-base 12627 df-plusg 12711 df-mgm 12942 df-sgrp 12988 df-mnd 13001 df-cmn 13359 |
This theorem is referenced by: ablsub4 13386 lmod4 13836 |
Copyright terms: Public domain | W3C validator |