![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > grpass | Structured version Visualization version GIF version |
Description: A group operation is associative. (Contributed by NM, 14-Aug-2011.) |
Ref | Expression |
---|---|
grpcl.b | ⊢ 𝐵 = (Base‘𝐺) |
grpcl.p | ⊢ + = (+g‘𝐺) |
Ref | Expression |
---|---|
grpass | ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpmnd 18902 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndass 18708 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
5 | 1, 4 | sylan 578 | 1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ‘cfv 6551 (class class class)co 7424 Basecbs 17185 +gcplusg 17238 Mndcmnd 18699 Grpcgrp 18895 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 ax-nul 5308 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-ne 2937 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-br 5151 df-iota 6503 df-fv 6559 df-ov 7427 df-sgrp 18684 df-mnd 18700 df-grp 18898 |
This theorem is referenced by: grpassd 18907 grprcan 18935 grprinv 18952 grpinvid1 18953 grpinvid2 18954 grplcan 18962 grpasscan1 18963 grpasscan2 18964 grpinvadd 18979 grpsubadd 18989 grpaddsubass 18991 grpsubsub4 18994 dfgrp3 19000 grplactcnv 19004 imasgrp 19017 mulgaddcomlem 19057 mulgaddcom 19058 mulgdirlem 19065 issubg2 19101 isnsg3 19120 nmzsubg 19125 ssnmz 19126 eqgcpbl 19142 qusgrp 19146 conjghm 19208 subgga 19256 cntzsubg 19295 sylow1lem2 19559 sylow2blem1 19580 sylow2blem2 19581 sylow2blem3 19582 sylow3lem1 19587 sylow3lem2 19588 lsmass 19629 lsmmod 19635 lsmdisj2 19642 gex2abl 19811 ringcom 20221 lmodass 20764 evpmodpmf1o 21533 psrgrpOLD 21905 ghmcnp 24037 qustgpopn 24042 cnncvsaddassdemo 25109 ogrpaddltbi 32816 ogrpaddltrbid 32818 ogrpinvlt 32821 cyc3genpmlem 32890 archiabllem2c 32921 quslsm 33133 lfladdass 38549 dvhvaddass 40574 |
Copyright terms: Public domain | W3C validator |