![]() |
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 18970 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndass 18768 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
5 | 1, 4 | sylan 580 | 1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1536 ∈ wcel 2105 ‘cfv 6562 (class class class)co 7430 Basecbs 17244 +gcplusg 17297 Mndcmnd 18759 Grpcgrp 18963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-nul 5311 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-sbc 3791 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-iota 6515 df-fv 6570 df-ov 7433 df-sgrp 18744 df-mnd 18760 df-grp 18966 |
This theorem is referenced by: grpassd 18975 grprcan 19003 grprinv 19020 grpinvid1 19021 grpinvid2 19022 grplcan 19030 grpasscan1 19031 grpasscan2 19032 grpinvadd 19048 grpsubadd 19058 grpaddsubass 19060 grpsubsub4 19063 dfgrp3 19069 grplactcnv 19073 imasgrp 19086 mulgaddcomlem 19127 mulgaddcom 19128 mulgdirlem 19135 issubg2 19171 isnsg3 19190 nmzsubg 19195 ssnmz 19196 eqgcpbl 19212 qusgrp 19216 conjghm 19279 subgga 19330 cntzsubg 19369 sylow1lem2 19631 sylow2blem1 19652 sylow2blem2 19653 sylow2blem3 19654 sylow3lem1 19659 sylow3lem2 19660 lsmass 19701 lsmmod 19707 lsmdisj2 19714 gex2abl 19883 ringcom 20293 lmodass 20890 evpmodpmf1o 21631 psrgrpOLD 21994 ghmcnp 24138 qustgpopn 24143 cnncvsaddassdemo 25210 ogrpaddltbi 33077 ogrpaddltrbid 33079 ogrpinvlt 33082 cyc3genpmlem 33153 archiabllem2c 33184 quslsm 33412 lfladdass 39054 dvhvaddass 41079 |
Copyright terms: Public domain | W3C validator |