ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  grpsubsub4 GIF version

Theorem grpsubsub4 12819
Description: Double group subtraction (subsub4 8161 analog). (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
grpsubadd.b 𝐵 = (Base‘𝐺)
grpsubadd.p + = (+g𝐺)
grpsubadd.m = (-g𝐺)
Assertion
Ref Expression
grpsubsub4 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) 𝑍) = (𝑋 (𝑍 + 𝑌)))

Proof of Theorem grpsubsub4
StepHypRef Expression
1 simpl 109 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐺 ∈ Grp)
2 grpsubadd.b . . . . . . . 8 𝐵 = (Base‘𝐺)
3 grpsubadd.m . . . . . . . 8 = (-g𝐺)
42, 3grpsubcl 12806 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
543adant3r3 1212 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 𝑌) ∈ 𝐵)
6 simpr3 1003 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑍𝐵)
7 grpsubadd.p . . . . . . 7 + = (+g𝐺)
82, 7, 3grpnpcan 12818 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑋 𝑌) ∈ 𝐵𝑍𝐵) → (((𝑋 𝑌) 𝑍) + 𝑍) = (𝑋 𝑌))
91, 5, 6, 8syl3anc 1236 . . . . 5 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((𝑋 𝑌) 𝑍) + 𝑍) = (𝑋 𝑌))
109oveq1d 5877 . . . 4 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((((𝑋 𝑌) 𝑍) + 𝑍) + 𝑌) = ((𝑋 𝑌) + 𝑌))
112, 3grpsubcl 12806 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑋 𝑌) ∈ 𝐵𝑍𝐵) → ((𝑋 𝑌) 𝑍) ∈ 𝐵)
121, 5, 6, 11syl3anc 1236 . . . . 5 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) 𝑍) ∈ 𝐵)
13 simpr2 1002 . . . . 5 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑌𝐵)
142, 7grpass 12744 . . . . 5 ((𝐺 ∈ Grp ∧ (((𝑋 𝑌) 𝑍) ∈ 𝐵𝑍𝐵𝑌𝐵)) → ((((𝑋 𝑌) 𝑍) + 𝑍) + 𝑌) = (((𝑋 𝑌) 𝑍) + (𝑍 + 𝑌)))
151, 12, 6, 13, 14syl13anc 1238 . . . 4 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((((𝑋 𝑌) 𝑍) + 𝑍) + 𝑌) = (((𝑋 𝑌) 𝑍) + (𝑍 + 𝑌)))
162, 7, 3grpnpcan 12818 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌) + 𝑌) = 𝑋)
17163adant3r3 1212 . . . 4 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) + 𝑌) = 𝑋)
1810, 15, 173eqtr3d 2214 . . 3 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((𝑋 𝑌) 𝑍) + (𝑍 + 𝑌)) = 𝑋)
19 simpr1 1001 . . . 4 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑋𝐵)
202, 7grpcl 12743 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑍𝐵𝑌𝐵) → (𝑍 + 𝑌) ∈ 𝐵)
211, 6, 13, 20syl3anc 1236 . . . 4 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑍 + 𝑌) ∈ 𝐵)
222, 7, 3grpsubadd 12814 . . . 4 ((𝐺 ∈ Grp ∧ (𝑋𝐵 ∧ (𝑍 + 𝑌) ∈ 𝐵 ∧ ((𝑋 𝑌) 𝑍) ∈ 𝐵)) → ((𝑋 (𝑍 + 𝑌)) = ((𝑋 𝑌) 𝑍) ↔ (((𝑋 𝑌) 𝑍) + (𝑍 + 𝑌)) = 𝑋))
231, 19, 21, 12, 22syl13anc 1238 . . 3 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 (𝑍 + 𝑌)) = ((𝑋 𝑌) 𝑍) ↔ (((𝑋 𝑌) 𝑍) + (𝑍 + 𝑌)) = 𝑋))
2418, 23mpbird 168 . 2 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (𝑍 + 𝑌)) = ((𝑋 𝑌) 𝑍))
2524eqcomd 2179 1 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) 𝑍) = (𝑋 (𝑍 + 𝑌)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 976   = wceq 1351  wcel 2144  cfv 5205  (class class class)co 5862  Basecbs 12425  +gcplusg 12489  Grpcgrp 12735  -gcsg 12737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 612  ax-in2 613  ax-io 707  ax-5 1443  ax-7 1444  ax-gen 1445  ax-ie1 1489  ax-ie2 1490  ax-8 1500  ax-10 1501  ax-11 1502  ax-i12 1503  ax-bndl 1505  ax-4 1506  ax-17 1522  ax-i9 1526  ax-ial 1530  ax-i5r 1531  ax-13 2146  ax-14 2147  ax-ext 2155  ax-coll 4110  ax-sep 4113  ax-pow 4166  ax-pr 4200  ax-un 4424  ax-setind 4527  ax-cnex 7874  ax-resscn 7875  ax-1re 7877  ax-addrcl 7880
This theorem depends on definitions:  df-bi 117  df-3an 978  df-tru 1354  df-fal 1357  df-nf 1457  df-sb 1759  df-eu 2025  df-mo 2026  df-clab 2160  df-cleq 2166  df-clel 2169  df-nfc 2304  df-ne 2344  df-ral 2456  df-rex 2457  df-reu 2458  df-rmo 2459  df-rab 2460  df-v 2735  df-sbc 2959  df-csb 3053  df-dif 3126  df-un 3128  df-in 3130  df-ss 3137  df-pw 3571  df-sn 3592  df-pr 3593  df-op 3595  df-uni 3803  df-int 3838  df-iun 3881  df-br 3996  df-opab 4057  df-mpt 4058  df-id 4284  df-xp 4623  df-rel 4624  df-cnv 4625  df-co 4626  df-dm 4627  df-rn 4628  df-res 4629  df-ima 4630  df-iota 5167  df-fun 5207  df-fn 5208  df-f 5209  df-f1 5210  df-fo 5211  df-f1o 5212  df-fv 5213  df-riota 5818  df-ov 5865  df-oprab 5866  df-mpo 5867  df-1st 6128  df-2nd 6129  df-inn 8888  df-2 8946  df-ndx 12428  df-slot 12429  df-base 12431  df-plusg 12502  df-0g 12625  df-mgm 12637  df-sgrp 12670  df-mnd 12680  df-grp 12738  df-minusg 12739  df-sbg 12740
This theorem is referenced by:  grppnpcan2  12820  grpnnncan2  12823
  Copyright terms: Public domain W3C validator