ablsubsub4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ablsubsub4		Structured version Visualization version GIF version

Theorem ablsubsub4 19784

Description: Law for double subtraction. (Contributed by NM, 7-Apr-2015.)

**Hypotheses**
Ref	Expression
ablsubadd.b	⊢ 𝐵 = (Base‘𝐺)
ablsubadd.p	⊢ + = (+_g‘𝐺)
ablsubadd.m	⊢ − = (-_g‘𝐺)
ablsubsub.g	⊢ (𝜑 → 𝐺 ∈ Abel)
ablsubsub.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
ablsubsub.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
ablsubsub.z	⊢ (𝜑 → 𝑍 ∈ 𝐵)

**Assertion**
Ref	Expression
ablsubsub4	⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍)))

**Proof of Theorem ablsubsub4**
Step	Hyp	Ref	Expression
1		ablsubsub.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ Abel)
2		ablgrp 19751	. . . . 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 18987	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)
9	3, 4, 5, 8	syl3anc 1374	. . 3 ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝐵)
10		ablsubsub.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
11		ablsubadd.p	. . . 4 ⊢ + = (+_g‘𝐺)
12		eqid 2737	. . . 4 ⊢ (inv_g‘𝐺) = (inv_g‘𝐺)
13	6, 11, 12, 7	grpsubval 18952	. . 3 ⊢ (((𝑋 − 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 − 𝑌) − 𝑍) = ((𝑋 − 𝑌) + ((inv_g‘𝐺)‘𝑍)))
14	9, 10, 13	syl2anc 585	. 2 ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = ((𝑋 − 𝑌) + ((inv_g‘𝐺)‘𝑍)))
15	6, 12	grpinvcl 18954	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵) → ((inv_g‘𝐺)‘𝑍) ∈ 𝐵)
16	3, 10, 15	syl2anc 585	. . 3 ⊢ (𝜑 → ((inv_g‘𝐺)‘𝑍) ∈ 𝐵)
17	6, 11, 7, 1, 4, 5, 16	ablsubsub 19783	. 2 ⊢ (𝜑 → (𝑋 − (𝑌 − ((inv_g‘𝐺)‘𝑍))) = ((𝑋 − 𝑌) + ((inv_g‘𝐺)‘𝑍)))
18	6, 11, 7, 12, 3, 5, 10	grpsubinv 18979	. . 3 ⊢ (𝜑 → (𝑌 − ((inv_g‘𝐺)‘𝑍)) = (𝑌 + 𝑍))
19	18	oveq2d 7376	. 2 ⊢ (𝜑 → (𝑋 − (𝑌 − ((inv_g‘𝐺)‘𝑍))) = (𝑋 − (𝑌 + 𝑍)))
20	14, 17, 19	3eqtr2d 2778	1 ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ‘cfv 6492 (class class class)co 7360 Basecbs 17170 +_gcplusg 17211 Grpcgrp 18900 inv_gcminusg 18901 -_gcsg 18902 Abelcabl 19747

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-fv 6500 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-1st 7935 df-2nd 7936 df-0g 17395 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-grp 18903 df-minusg 18904 df-sbg 18905 df-cmn 19748 df-abl 19749

This theorem is referenced by: ablsub32 19787 ablnnncan 19788 rngqiprngfulem4 21304 ip2subdi 21634 cpmadugsumlemF 22851 baerlem5alem2 42171

W3C validator