![]() |
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 17783 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndass 17655 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
5 | 1, 4 | sylan 577 | 1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 = wceq 1658 ∈ wcel 2166 ‘cfv 6123 (class class class)co 6905 Basecbs 16222 +gcplusg 16305 Mndcmnd 17647 Grpcgrp 17776 |
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 2391 ax-ext 2803 ax-nul 5013 |
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 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-iota 6086 df-fv 6131 df-ov 6908 df-sgrp 17637 df-mnd 17648 df-grp 17779 |
This theorem is referenced by: grprcan 17809 grprinv 17823 grpinvid1 17824 grpinvid2 17825 grplcan 17831 grpasscan1 17832 grpasscan2 17833 grplmulf1o 17843 grpinvadd 17847 grpsubadd 17857 grpaddsubass 17859 grpsubsub4 17862 dfgrp3 17868 grplactcnv 17872 imasgrp 17885 mulgaddcomlem 17916 mulgaddcom 17917 mulgdirlem 17924 issubg2 17960 isnsg3 17979 nmzsubg 17986 ssnmz 17987 eqger 17995 eqgcpbl 17999 qusgrp 18000 conjghm 18042 conjnmz 18045 subgga 18083 cntzsubg 18119 sylow1lem2 18365 sylow2blem1 18386 sylow2blem2 18387 sylow2blem3 18388 sylow3lem1 18393 sylow3lem2 18394 lsmass 18434 lsmmod 18439 lsmdisj2 18446 gex2abl 18607 ringcom 18933 lmodass 19234 psrgrp 19759 evpmodpmf1o 20302 ghmcnp 22288 qustgpopn 22293 cnncvsaddassdemo 23332 ogrpaddltbi 30264 ogrpaddltrbid 30266 ogrpinvlt 30269 archiabllem2c 30294 lfladdass 35148 dvhvaddass 37172 |
Copyright terms: Public domain | W3C validator |