Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eqg Structured version   Unicode version

Definition df-eqg 14974
 Description: Define the equivalence relation in a quotient ring or quotient group (where is a two-sided ideal or a normal subgroup). For non-normal subgroups this generates the left cosets. (Contributed by Mario Carneiro, 15-Jun-2015.)
Assertion
Ref Expression
df-eqg ~QG
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-eqg
StepHypRef Expression
1 cqg 14971 . 2 ~QG
2 vr . . 3
3 vi . . 3
4 cvv 2962 . . 3
5 vx . . . . . . . 8
65cv 1652 . . . . . . 7
7 vy . . . . . . . 8
87cv 1652 . . . . . . 7
96, 8cpr 3839 . . . . . 6
102cv 1652 . . . . . . 7
11 cbs 13500 . . . . . . 7
1210, 11cfv 5483 . . . . . 6
139, 12wss 3306 . . . . 5
14 cminusg 14717 . . . . . . . . 9
1510, 14cfv 5483 . . . . . . . 8
166, 15cfv 5483 . . . . . . 7
17 cplusg 13560 . . . . . . . 8
1810, 17cfv 5483 . . . . . . 7
1916, 8, 18co 6110 . . . . . 6
203cv 1652 . . . . . 6
2119, 20wcel 1727 . . . . 5
2213, 21wa 360 . . . 4
2322, 5, 7copab 4290 . . 3
242, 3, 4, 4, 23cmpt2 6112 . 2
251, 24wceq 1653 1 ~QG
 Colors of variables: wff set class This definition is referenced by:  releqg  15018  eqgfval  15019
 Copyright terms: Public domain W3C validator