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 18326 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndass 18136 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
5 | 1, 4 | sylan 583 | 1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2112 ‘cfv 6358 (class class class)co 7191 Basecbs 16666 +gcplusg 16749 Mndcmnd 18127 Grpcgrp 18319 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-nul 5184 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-sbc 3684 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-iota 6316 df-fv 6366 df-ov 7194 df-sgrp 18117 df-mnd 18128 df-grp 18322 |
This theorem is referenced by: grprcan 18355 grprinv 18371 grpinvid1 18372 grpinvid2 18373 grplcan 18379 grpasscan1 18380 grpasscan2 18381 grplmulf1o 18391 grpinvadd 18395 grpsubadd 18405 grpaddsubass 18407 grpsubsub4 18410 dfgrp3 18416 grplactcnv 18420 imasgrp 18433 mulgaddcomlem 18468 mulgaddcom 18469 mulgdirlem 18476 issubg2 18512 isnsg3 18530 nmzsubg 18535 ssnmz 18536 eqger 18548 eqgcpbl 18552 qusgrp 18553 conjghm 18607 conjnmz 18610 subgga 18648 cntzsubg 18685 sylow1lem2 18942 sylow2blem1 18963 sylow2blem2 18964 sylow2blem3 18965 sylow3lem1 18970 sylow3lem2 18971 lsmass 19013 lsmmod 19019 lsmdisj2 19026 gex2abl 19190 ringcom 19551 lmodass 19868 evpmodpmf1o 20512 psrgrp 20877 ghmcnp 22966 qustgpopn 22971 cnncvsaddassdemo 24014 ogrpaddltbi 31017 ogrpaddltrbid 31019 ogrpinvlt 31022 cyc3genpmlem 31091 archiabllem2c 31122 quslsm 31261 lfladdass 36773 dvhvaddass 38797 |
Copyright terms: Public domain | W3C validator |