Metamath Proof Explorer


Theorem eqger

Description: The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses eqger.x X = Base G
eqger.r ˙ = G ~ QG Y
Assertion eqger Y SubGrp G ˙ Er X

Proof

Step Hyp Ref Expression
1 eqger.x X = Base G
2 eqger.r ˙ = G ~ QG Y
3 2 releqg Rel ˙
4 3 a1i Y SubGrp G Rel ˙
5 subgrcl Y SubGrp G G Grp
6 1 subgss Y SubGrp G Y X
7 eqid inv g G = inv g G
8 eqid + G = + G
9 1 7 8 2 eqgval G Grp Y X x ˙ y x X y X inv g G x + G y Y
10 5 6 9 syl2anc Y SubGrp G x ˙ y x X y X inv g G x + G y Y
11 10 biimpa Y SubGrp G x ˙ y x X y X inv g G x + G y Y
12 11 simp2d Y SubGrp G x ˙ y y X
13 11 simp1d Y SubGrp G x ˙ y x X
14 5 adantr Y SubGrp G x ˙ y G Grp
15 1 7 14 13 grpinvcld Y SubGrp G x ˙ y inv g G x X
16 1 8 7 grpinvadd G Grp inv g G x X y X inv g G inv g G x + G y = inv g G y + G inv g G inv g G x
17 14 15 12 16 syl3anc Y SubGrp G x ˙ y inv g G inv g G x + G y = inv g G y + G inv g G inv g G x
18 1 7 grpinvinv G Grp x X inv g G inv g G x = x
19 14 13 18 syl2anc Y SubGrp G x ˙ y inv g G inv g G x = x
20 19 oveq2d Y SubGrp G x ˙ y inv g G y + G inv g G inv g G x = inv g G y + G x
21 17 20 eqtrd Y SubGrp G x ˙ y inv g G inv g G x + G y = inv g G y + G x
22 11 simp3d Y SubGrp G x ˙ y inv g G x + G y Y
23 7 subginvcl Y SubGrp G inv g G x + G y Y inv g G inv g G x + G y Y
24 22 23 syldan Y SubGrp G x ˙ y inv g G inv g G x + G y Y
25 21 24 eqeltrrd Y SubGrp G x ˙ y inv g G y + G x Y
26 6 adantr Y SubGrp G x ˙ y Y X
27 1 7 8 2 eqgval G Grp Y X y ˙ x y X x X inv g G y + G x Y
28 14 26 27 syl2anc Y SubGrp G x ˙ y y ˙ x y X x X inv g G y + G x Y
29 12 13 25 28 mpbir3and Y SubGrp G x ˙ y y ˙ x
30 13 adantrr Y SubGrp G x ˙ y y ˙ z x X
31 1 7 8 2 eqgval G Grp Y X y ˙ z y X z X inv g G y + G z Y
32 5 6 31 syl2anc Y SubGrp G y ˙ z y X z X inv g G y + G z Y
33 32 biimpa Y SubGrp G y ˙ z y X z X inv g G y + G z Y
34 33 adantrl Y SubGrp G x ˙ y y ˙ z y X z X inv g G y + G z Y
35 34 simp2d Y SubGrp G x ˙ y y ˙ z z X
36 5 adantr Y SubGrp G x ˙ y y ˙ z G Grp
37 1 7 36 30 grpinvcld Y SubGrp G x ˙ y y ˙ z inv g G x X
38 12 adantrr Y SubGrp G x ˙ y y ˙ z y X
39 1 7 36 38 grpinvcld Y SubGrp G x ˙ y y ˙ z inv g G y X
40 1 8 36 39 35 grpcld Y SubGrp G x ˙ y y ˙ z inv g G y + G z X
41 1 8 36 37 38 40 grpassd Y SubGrp G x ˙ y y ˙ z inv g G x + G y + G inv g G y + G z = inv g G x + G y + G inv g G y + G z
42 eqid 0 G = 0 G
43 1 8 42 7 grprinv G Grp y X y + G inv g G y = 0 G
44 36 38 43 syl2anc Y SubGrp G x ˙ y y ˙ z y + G inv g G y = 0 G
45 44 oveq1d Y SubGrp G x ˙ y y ˙ z y + G inv g G y + G z = 0 G + G z
46 1 8 36 38 39 35 grpassd Y SubGrp G x ˙ y y ˙ z y + G inv g G y + G z = y + G inv g G y + G z
47 1 8 42 36 35 grplidd Y SubGrp G x ˙ y y ˙ z 0 G + G z = z
48 45 46 47 3eqtr3d Y SubGrp G x ˙ y y ˙ z y + G inv g G y + G z = z
49 48 oveq2d Y SubGrp G x ˙ y y ˙ z inv g G x + G y + G inv g G y + G z = inv g G x + G z
50 41 49 eqtrd Y SubGrp G x ˙ y y ˙ z inv g G x + G y + G inv g G y + G z = inv g G x + G z
51 simpl Y SubGrp G x ˙ y y ˙ z Y SubGrp G
52 22 adantrr Y SubGrp G x ˙ y y ˙ z inv g G x + G y Y
53 34 simp3d Y SubGrp G x ˙ y y ˙ z inv g G y + G z Y
54 8 subgcl Y SubGrp G inv g G x + G y Y inv g G y + G z Y inv g G x + G y + G inv g G y + G z Y
55 51 52 53 54 syl3anc Y SubGrp G x ˙ y y ˙ z inv g G x + G y + G inv g G y + G z Y
56 50 55 eqeltrrd Y SubGrp G x ˙ y y ˙ z inv g G x + G z Y
57 6 adantr Y SubGrp G x ˙ y y ˙ z Y X
58 1 7 8 2 eqgval G Grp Y X x ˙ z x X z X inv g G x + G z Y
59 36 57 58 syl2anc Y SubGrp G x ˙ y y ˙ z x ˙ z x X z X inv g G x + G z Y
60 30 35 56 59 mpbir3and Y SubGrp G x ˙ y y ˙ z x ˙ z
61 1 8 42 7 grplinv G Grp x X inv g G x + G x = 0 G
62 5 61 sylan Y SubGrp G x X inv g G x + G x = 0 G
63 42 subg0cl Y SubGrp G 0 G Y
64 63 adantr Y SubGrp G x X 0 G Y
65 62 64 eqeltrd Y SubGrp G x X inv g G x + G x Y
66 65 ex Y SubGrp G x X inv g G x + G x Y
67 66 pm4.71rd Y SubGrp G x X inv g G x + G x Y x X
68 1 7 8 2 eqgval G Grp Y X x ˙ x x X x X inv g G x + G x Y
69 5 6 68 syl2anc Y SubGrp G x ˙ x x X x X inv g G x + G x Y
70 df-3an x X x X inv g G x + G x Y x X x X inv g G x + G x Y
71 anidm x X x X x X
72 71 anbi2ci x X x X inv g G x + G x Y inv g G x + G x Y x X
73 70 72 bitri x X x X inv g G x + G x Y inv g G x + G x Y x X
74 69 73 bitrdi Y SubGrp G x ˙ x inv g G x + G x Y x X
75 67 74 bitr4d Y SubGrp G x X x ˙ x
76 4 29 60 75 iserd Y SubGrp G ˙ Er X