![]() |
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 17551 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndass 17424 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
5 | 1, 4 | sylan 489 | 1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 = wceq 1596 ∈ wcel 2103 ‘cfv 6001 (class class class)co 6765 Basecbs 15980 +gcplusg 16064 Mndcmnd 17416 Grpcgrp 17544 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-nul 4897 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ral 3019 df-rex 3020 df-rab 3023 df-v 3306 df-sbc 3542 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-br 4761 df-iota 5964 df-fv 6009 df-ov 6768 df-sgrp 17406 df-mnd 17417 df-grp 17547 |
This theorem is referenced by: grprcan 17577 grprinv 17591 grpinvid1 17592 grpinvid2 17593 grplcan 17599 grpasscan1 17600 grpasscan2 17601 grplmulf1o 17611 grpinvadd 17615 grpsubadd 17625 grpaddsubass 17627 grpsubsub4 17630 dfgrp3 17636 grplactcnv 17640 imasgrp 17653 mulgaddcomlem 17685 mulgaddcom 17686 mulgdirlem 17694 issubg2 17731 isnsg3 17750 nmzsubg 17757 ssnmz 17758 eqger 17766 eqgcpbl 17770 qusgrp 17771 conjghm 17813 conjnmz 17816 subgga 17854 cntzsubg 17890 sylow1lem2 18135 sylow2blem1 18156 sylow2blem2 18157 sylow2blem3 18158 sylow3lem1 18163 sylow3lem2 18164 lsmass 18204 lsmmod 18209 lsmdisj2 18216 gex2abl 18375 ringcom 18700 lmodass 19001 psrgrp 19521 evpmodpmf1o 20065 ghmcnp 22040 qustgpopn 22045 cnncvsaddassdemo 23084 ogrpaddltbi 29949 ogrpaddltrbid 29951 ogrpinvlt 29954 archiabllem2c 29979 lfladdass 34780 dvhvaddass 36805 |
Copyright terms: Public domain | W3C validator |