![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ablsubsub4 | Structured version Visualization version GIF version |
Description: Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
Ref | Expression |
---|---|
ablsubadd.b | ⊢ 𝐵 = (Base‘𝐺) |
ablsubadd.p | ⊢ + = (+g‘𝐺) |
ablsubadd.m | ⊢ − = (-g‘𝐺) |
ablsubsub.g | ⊢ (𝜑 → 𝐺 ∈ Abel) |
ablsubsub.x | ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
ablsubsub.y | ⊢ (𝜑 → 𝑌 ∈ 𝐵) |
ablsubsub.z | ⊢ (𝜑 → 𝑍 ∈ 𝐵) |
Ref | Expression |
---|---|
ablsubsub4 | ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ablsubsub.g | . . . . 5 ⊢ (𝜑 → 𝐺 ∈ Abel) | |
2 | ablgrp 18517 | . . . . 5 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | |
3 | 1, 2 | syl 17 | . . . 4 ⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | ablsubsub.x | . . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵) | |
5 | ablsubsub.y | . . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐵) | |
6 | ablsubadd.b | . . . . 5 ⊢ 𝐵 = (Base‘𝐺) | |
7 | ablsubadd.m | . . . . 5 ⊢ − = (-g‘𝐺) | |
8 | 6, 7 | grpsubcl 17815 | . . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵) |
9 | 3, 4, 5, 8 | syl3anc 1491 | . . 3 ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝐵) |
10 | ablsubsub.z | . . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐵) | |
11 | ablsubadd.p | . . . 4 ⊢ + = (+g‘𝐺) | |
12 | eqid 2803 | . . . 4 ⊢ (invg‘𝐺) = (invg‘𝐺) | |
13 | 6, 11, 12, 7 | grpsubval 17785 | . . 3 ⊢ (((𝑋 − 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 − 𝑌) − 𝑍) = ((𝑋 − 𝑌) + ((invg‘𝐺)‘𝑍))) |
14 | 9, 10, 13 | syl2anc 580 | . 2 ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = ((𝑋 − 𝑌) + ((invg‘𝐺)‘𝑍))) |
15 | 6, 12 | grpinvcl 17787 | . . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵) → ((invg‘𝐺)‘𝑍) ∈ 𝐵) |
16 | 3, 10, 15 | syl2anc 580 | . . 3 ⊢ (𝜑 → ((invg‘𝐺)‘𝑍) ∈ 𝐵) |
17 | 6, 11, 7, 1, 4, 5, 16 | ablsubsub 18542 | . 2 ⊢ (𝜑 → (𝑋 − (𝑌 − ((invg‘𝐺)‘𝑍))) = ((𝑋 − 𝑌) + ((invg‘𝐺)‘𝑍))) |
18 | 6, 11, 7, 12, 3, 5, 10 | grpsubinv 17808 | . . 3 ⊢ (𝜑 → (𝑌 − ((invg‘𝐺)‘𝑍)) = (𝑌 + 𝑍)) |
19 | 18 | oveq2d 6898 | . 2 ⊢ (𝜑 → (𝑋 − (𝑌 − ((invg‘𝐺)‘𝑍))) = (𝑋 − (𝑌 + 𝑍))) |
20 | 14, 17, 19 | 3eqtr2d 2843 | 1 ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ∈ wcel 2157 ‘cfv 6105 (class class class)co 6882 Basecbs 16188 +gcplusg 16271 Grpcgrp 17742 invgcminusg 17743 -gcsg 17744 Abelcabl 18513 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2379 ax-ext 2781 ax-rep 4968 ax-sep 4979 ax-nul 4987 ax-pow 5039 ax-pr 5101 ax-un 7187 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2593 df-eu 2611 df-clab 2790 df-cleq 2796 df-clel 2799 df-nfc 2934 df-ne 2976 df-ral 3098 df-rex 3099 df-reu 3100 df-rmo 3101 df-rab 3102 df-v 3391 df-sbc 3638 df-csb 3733 df-dif 3776 df-un 3778 df-in 3780 df-ss 3787 df-nul 4120 df-if 4282 df-pw 4355 df-sn 4373 df-pr 4375 df-op 4379 df-uni 4633 df-iun 4716 df-br 4848 df-opab 4910 df-mpt 4927 df-id 5224 df-xp 5322 df-rel 5323 df-cnv 5324 df-co 5325 df-dm 5326 df-rn 5327 df-res 5328 df-ima 5329 df-iota 6068 df-fun 6107 df-fn 6108 df-f 6109 df-f1 6110 df-fo 6111 df-f1o 6112 df-fv 6113 df-riota 6843 df-ov 6885 df-oprab 6886 df-mpt2 6887 df-1st 7405 df-2nd 7406 df-0g 16421 df-mgm 17561 df-sgrp 17603 df-mnd 17614 df-grp 17745 df-minusg 17746 df-sbg 17747 df-cmn 18514 df-abl 18515 |
This theorem is referenced by: ablsub32 18546 ablnnncan 18547 ip2subdi 20317 cpmadugsumlemF 21013 baerlem5alem2 37736 |
Copyright terms: Public domain | W3C validator |