![]() |
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 17868 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndass 17741 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
5 | 1, 4 | sylan 580 | 1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 = wceq 1522 ∈ wcel 2081 ‘cfv 6225 (class class class)co 7016 Basecbs 16312 +gcplusg 16394 Mndcmnd 17733 Grpcgrp 17861 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 ax-nul 5101 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-iota 6189 df-fv 6233 df-ov 7019 df-sgrp 17723 df-mnd 17734 df-grp 17864 |
This theorem is referenced by: grprcan 17894 grprinv 17910 grpinvid1 17911 grpinvid2 17912 grplcan 17918 grpasscan1 17919 grpasscan2 17920 grplmulf1o 17930 grpinvadd 17934 grpsubadd 17944 grpaddsubass 17946 grpsubsub4 17949 dfgrp3 17955 grplactcnv 17959 imasgrp 17972 mulgaddcomlem 18004 mulgaddcom 18005 mulgdirlem 18012 issubg2 18048 isnsg3 18067 nmzsubg 18074 ssnmz 18075 eqger 18083 eqgcpbl 18087 qusgrp 18088 conjghm 18130 conjnmz 18133 subgga 18171 cntzsubg 18208 sylow1lem2 18454 sylow2blem1 18475 sylow2blem2 18476 sylow2blem3 18477 sylow3lem1 18482 sylow3lem2 18483 lsmass 18523 lsmmod 18528 lsmdisj2 18535 gex2abl 18694 ringcom 19019 lmodass 19339 psrgrp 19866 evpmodpmf1o 20422 ghmcnp 22406 qustgpopn 22411 cnncvsaddassdemo 23450 ogrpaddltbi 30379 ogrpaddltrbid 30381 ogrpinvlt 30384 cyc3genpmlem 30431 archiabllem2c 30462 lfladdass 35740 dvhvaddass 37764 |
Copyright terms: Public domain | W3C validator |