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 grpinvcl G Grp x X inv g G x X
16 14 13 15 syl2anc Y SubGrp G x ˙ y inv g G x X
17 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
18 14 16 12 17 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
19 1 7 grpinvinv G Grp x X inv g G inv g G x = x
20 14 13 19 syl2anc Y SubGrp G x ˙ y inv g G inv g G x = x
21 20 oveq2d Y SubGrp G x ˙ y inv g G y + G inv g G inv g G x = inv g G y + G x
22 18 21 eqtrd Y SubGrp G x ˙ y inv g G inv g G x + G y = inv g G y + G x
23 11 simp3d Y SubGrp G x ˙ y inv g G x + G y Y
24 7 subginvcl Y SubGrp G inv g G x + G y Y inv g G inv g G x + G y Y
25 23 24 syldan Y SubGrp G x ˙ y inv g G inv g G x + G y Y
26 22 25 eqeltrrd Y SubGrp G x ˙ y inv g G y + G x Y
27 6 adantr Y SubGrp G x ˙ y Y X
28 1 7 8 2 eqgval G Grp Y X y ˙ x y X x X inv g G y + G x Y
29 14 27 28 syl2anc Y SubGrp G x ˙ y y ˙ x y X x X inv g G y + G x Y
30 12 13 26 29 mpbir3and Y SubGrp G x ˙ y y ˙ x
31 13 adantrr Y SubGrp G x ˙ y y ˙ z x X
32 1 7 8 2 eqgval G Grp Y X y ˙ z y X z X inv g G y + G z Y
33 5 6 32 syl2anc Y SubGrp G y ˙ z y X z X inv g G y + G z Y
34 33 biimpa Y SubGrp G y ˙ z y X z X inv g G y + G z Y
35 34 adantrl Y SubGrp G x ˙ y y ˙ z y X z X inv g G y + G z Y
36 35 simp2d Y SubGrp G x ˙ y y ˙ z z X
37 5 adantr Y SubGrp G x ˙ y y ˙ z G Grp
38 37 31 15 syl2anc Y SubGrp G x ˙ y y ˙ z inv g G x X
39 12 adantrr Y SubGrp G x ˙ y y ˙ z y X
40 1 7 grpinvcl G Grp y X inv g G y X
41 37 39 40 syl2anc Y SubGrp G x ˙ y y ˙ z inv g G y X
42 1 8 grpcl G Grp inv g G y X z X inv g G y + G z X
43 37 41 36 42 syl3anc Y SubGrp G x ˙ y y ˙ z inv g G y + G z X
44 1 8 grpass G Grp inv g G x X y X inv g G y + G z X 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
45 37 38 39 43 44 syl13anc 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
46 eqid 0 G = 0 G
47 1 8 46 7 grprinv G Grp y X y + G inv g G y = 0 G
48 37 39 47 syl2anc Y SubGrp G x ˙ y y ˙ z y + G inv g G y = 0 G
49 48 oveq1d Y SubGrp G x ˙ y y ˙ z y + G inv g G y + G z = 0 G + G z
50 1 8 grpass G Grp y X inv g G y X z X y + G inv g G y + G z = y + G inv g G y + G z
51 37 39 41 36 50 syl13anc Y SubGrp G x ˙ y y ˙ z y + G inv g G y + G z = y + G inv g G y + G z
52 1 8 46 grplid G Grp z X 0 G + G z = z
53 37 36 52 syl2anc Y SubGrp G x ˙ y y ˙ z 0 G + G z = z
54 49 51 53 3eqtr3d Y SubGrp G x ˙ y y ˙ z y + G inv g G y + G z = z
55 54 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
56 45 55 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
57 simpl Y SubGrp G x ˙ y y ˙ z Y SubGrp G
58 23 adantrr Y SubGrp G x ˙ y y ˙ z inv g G x + G y Y
59 35 simp3d Y SubGrp G x ˙ y y ˙ z inv g G y + G z Y
60 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
61 57 58 59 60 syl3anc Y SubGrp G x ˙ y y ˙ z inv g G x + G y + G inv g G y + G z Y
62 56 61 eqeltrrd Y SubGrp G x ˙ y y ˙ z inv g G x + G z Y
63 6 adantr Y SubGrp G x ˙ y y ˙ z Y X
64 1 7 8 2 eqgval G Grp Y X x ˙ z x X z X inv g G x + G z Y
65 37 63 64 syl2anc Y SubGrp G x ˙ y y ˙ z x ˙ z x X z X inv g G x + G z Y
66 31 36 62 65 mpbir3and Y SubGrp G x ˙ y y ˙ z x ˙ z
67 1 8 46 7 grplinv G Grp x X inv g G x + G x = 0 G
68 5 67 sylan Y SubGrp G x X inv g G x + G x = 0 G
69 46 subg0cl Y SubGrp G 0 G Y
70 69 adantr Y SubGrp G x X 0 G Y
71 68 70 eqeltrd Y SubGrp G x X inv g G x + G x Y
72 71 ex Y SubGrp G x X inv g G x + G x Y
73 72 pm4.71rd Y SubGrp G x X inv g G x + G x Y x X
74 1 7 8 2 eqgval G Grp Y X x ˙ x x X x X inv g G x + G x Y
75 5 6 74 syl2anc Y SubGrp G x ˙ x x X x X inv g G x + G x Y
76 df-3an x X x X inv g G x + G x Y x X x X inv g G x + G x Y
77 anidm x X x X x X
78 77 anbi2ci x X x X inv g G x + G x Y inv g G x + G x Y x X
79 76 78 bitri x X x X inv g G x + G x Y inv g G x + G x Y x X
80 75 79 bitrdi Y SubGrp G x ˙ x inv g G x + G x Y x X
81 73 80 bitr4d Y SubGrp G x X x ˙ x
82 4 30 66 81 iserd Y SubGrp G ˙ Er X