Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ablo4pnp Structured version   Visualization version   GIF version

Theorem ablo4pnp 35228
Description: A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.)
Hypotheses
Ref Expression
abl4pnp.1 𝑋 = ran 𝐺
abl4pnp.2 𝐷 = ( /𝑔𝐺)
Assertion
Ref Expression
ablo4pnp ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))

Proof of Theorem ablo4pnp
StepHypRef Expression
1 df-3an 1086 . . . . 5 ((𝐴𝑋𝐵𝑋𝐶𝑋) ↔ ((𝐴𝑋𝐵𝑋) ∧ 𝐶𝑋))
2 abl4pnp.1 . . . . . 6 𝑋 = ran 𝐺
3 abl4pnp.2 . . . . . 6 𝐷 = ( /𝑔𝐺)
42, 3ablomuldiv 28331 . . . . 5 ((𝐺 ∈ AbelOp ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐺𝐵))
51, 4sylan2br 597 . . . 4 ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ 𝐶𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐺𝐵))
65adantrrr 724 . . 3 ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → ((𝐴𝐺𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐺𝐵))
76oveq1d 7160 . 2 ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → (((𝐴𝐺𝐵)𝐷𝐶)𝐷𝐹) = (((𝐴𝐷𝐶)𝐺𝐵)𝐷𝐹))
8 ablogrpo 28326 . . . . . . 7 (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)
92grpocl 28279 . . . . . . . 8 ((𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
1093expib 1119 . . . . . . 7 (𝐺 ∈ GrpOp → ((𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) ∈ 𝑋))
118, 10syl 17 . . . . . 6 (𝐺 ∈ AbelOp → ((𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) ∈ 𝑋))
1211anim1d 613 . . . . 5 (𝐺 ∈ AbelOp → (((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋)) → ((𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐶𝑋𝐹𝑋))))
13 3anass 1092 . . . . 5 (((𝐴𝐺𝐵) ∈ 𝑋𝐶𝑋𝐹𝑋) ↔ ((𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐶𝑋𝐹𝑋)))
1412, 13syl6ibr 255 . . . 4 (𝐺 ∈ AbelOp → (((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋)) → ((𝐴𝐺𝐵) ∈ 𝑋𝐶𝑋𝐹𝑋)))
1514imp 410 . . 3 ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → ((𝐴𝐺𝐵) ∈ 𝑋𝐶𝑋𝐹𝑋))
162, 3ablodivdiv4 28333 . . 3 ((𝐺 ∈ AbelOp ∧ ((𝐴𝐺𝐵) ∈ 𝑋𝐶𝑋𝐹𝑋)) → (((𝐴𝐺𝐵)𝐷𝐶)𝐷𝐹) = ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)))
1715, 16syldan 594 . 2 ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → (((𝐴𝐺𝐵)𝐷𝐶)𝐷𝐹) = ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)))
182, 3grpodivcl 28318 . . . . . . . 8 ((𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐶𝑋) → (𝐴𝐷𝐶) ∈ 𝑋)
19183expib 1119 . . . . . . 7 (𝐺 ∈ GrpOp → ((𝐴𝑋𝐶𝑋) → (𝐴𝐷𝐶) ∈ 𝑋))
2019anim1d 613 . . . . . 6 (𝐺 ∈ GrpOp → (((𝐴𝑋𝐶𝑋) ∧ (𝐵𝑋𝐹𝑋)) → ((𝐴𝐷𝐶) ∈ 𝑋 ∧ (𝐵𝑋𝐹𝑋))))
21 an4 655 . . . . . 6 (((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋)) ↔ ((𝐴𝑋𝐶𝑋) ∧ (𝐵𝑋𝐹𝑋)))
22 3anass 1092 . . . . . 6 (((𝐴𝐷𝐶) ∈ 𝑋𝐵𝑋𝐹𝑋) ↔ ((𝐴𝐷𝐶) ∈ 𝑋 ∧ (𝐵𝑋𝐹𝑋)))
2320, 21, 223imtr4g 299 . . . . 5 (𝐺 ∈ GrpOp → (((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋)) → ((𝐴𝐷𝐶) ∈ 𝑋𝐵𝑋𝐹𝑋)))
2423imp 410 . . . 4 ((𝐺 ∈ GrpOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → ((𝐴𝐷𝐶) ∈ 𝑋𝐵𝑋𝐹𝑋))
252, 3grpomuldivass 28320 . . . 4 ((𝐺 ∈ GrpOp ∧ ((𝐴𝐷𝐶) ∈ 𝑋𝐵𝑋𝐹𝑋)) → (((𝐴𝐷𝐶)𝐺𝐵)𝐷𝐹) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))
2624, 25syldan 594 . . 3 ((𝐺 ∈ GrpOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → (((𝐴𝐷𝐶)𝐺𝐵)𝐷𝐹) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))
278, 26sylan 583 . 2 ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → (((𝐴𝐷𝐶)𝐺𝐵)𝐷𝐹) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))
287, 17, 273eqtr3d 2867 1 ((𝐺 ∈ AbelOp ∧ ((𝐴𝑋𝐵𝑋) ∧ (𝐶𝑋𝐹𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2115  ran crn 5543  cfv 6343  (class class class)co 7145  GrpOpcgr 28268   /𝑔 cgs 28271  AbelOpcablo 28323
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-op 4556  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7679  df-2nd 7680  df-grpo 28272  df-gid 28273  df-ginv 28274  df-gdiv 28275  df-ablo 28324
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator