Theorem ablogrpo 30526

Description: An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
ablogrpo	⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)

Proof of Theorem ablogrpo

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ ran 𝐺 = ran 𝐺
2	1	isablo 30525	. 2 ⊢ (𝐺 ∈ AbelOp ↔ (𝐺 ∈ GrpOp ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥𝐺𝑦) = (𝑦𝐺𝑥)))
3	2	simplbi 497	1 ⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ran crn 5632  (class class class)co 7369  GrpOpcgr 30468  AbelOpcablo 30523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642  df-iota 6452  df-fv 6507  df-ov 7372  df-ablo 30524

This theorem is referenced by:  ablo32  30528  ablo4  30529  ablomuldiv  30531  ablodivdiv  30532  ablodivdiv4  30533  ablonncan  30535  ablonnncan1  30536  vcgrp  30549  isvcOLD  30558  isvciOLD  30559  cnidOLD  30561  nvgrp  30596  cnnv  30656  cnnvba  30658  cncph  30798  hilid  31140  hhnv  31144  hhba  31146  hhph  31157  hhssabloilem  31240  hhssnv  31243  ablo4pnp  37867  rngogrpo  37897  iscringd  37985