Metamath Proof Explorer


Theorem eqgcpbl

Description: The subgroup coset equivalence relation is compatible with addition when the subgroup is normal. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses eqger.x X = Base G
eqger.r ˙ = G ~ QG Y
eqgcpbl.p + ˙ = + G
Assertion eqgcpbl Y NrmSGrp G A ˙ C B ˙ D A + ˙ B ˙ C + ˙ D

Proof

Step Hyp Ref Expression
1 eqger.x X = Base G
2 eqger.r ˙ = G ~ QG Y
3 eqgcpbl.p + ˙ = + G
4 nsgsubg Y NrmSGrp G Y SubGrp G
5 4 adantr Y NrmSGrp G A ˙ C B ˙ D Y SubGrp G
6 subgrcl Y SubGrp G G Grp
7 5 6 syl Y NrmSGrp G A ˙ C B ˙ D G Grp
8 simprl Y NrmSGrp G A ˙ C B ˙ D A ˙ C
9 1 subgss Y SubGrp G Y X
10 5 9 syl Y NrmSGrp G A ˙ C B ˙ D Y X
11 eqid inv g G = inv g G
12 1 11 3 2 eqgval G Grp Y X A ˙ C A X C X inv g G A + ˙ C Y
13 7 10 12 syl2anc Y NrmSGrp G A ˙ C B ˙ D A ˙ C A X C X inv g G A + ˙ C Y
14 8 13 mpbid Y NrmSGrp G A ˙ C B ˙ D A X C X inv g G A + ˙ C Y
15 14 simp1d Y NrmSGrp G A ˙ C B ˙ D A X
16 simprr Y NrmSGrp G A ˙ C B ˙ D B ˙ D
17 1 11 3 2 eqgval G Grp Y X B ˙ D B X D X inv g G B + ˙ D Y
18 7 10 17 syl2anc Y NrmSGrp G A ˙ C B ˙ D B ˙ D B X D X inv g G B + ˙ D Y
19 16 18 mpbid Y NrmSGrp G A ˙ C B ˙ D B X D X inv g G B + ˙ D Y
20 19 simp1d Y NrmSGrp G A ˙ C B ˙ D B X
21 1 3 grpcl G Grp A X B X A + ˙ B X
22 7 15 20 21 syl3anc Y NrmSGrp G A ˙ C B ˙ D A + ˙ B X
23 14 simp2d Y NrmSGrp G A ˙ C B ˙ D C X
24 19 simp2d Y NrmSGrp G A ˙ C B ˙ D D X
25 1 3 grpcl G Grp C X D X C + ˙ D X
26 7 23 24 25 syl3anc Y NrmSGrp G A ˙ C B ˙ D C + ˙ D X
27 1 3 11 grpinvadd G Grp A X B X inv g G A + ˙ B = inv g G B + ˙ inv g G A
28 7 15 20 27 syl3anc Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ B = inv g G B + ˙ inv g G A
29 28 oveq1d Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ B + ˙ C + ˙ D = inv g G B + ˙ inv g G A + ˙ C + ˙ D
30 1 11 grpinvcl G Grp B X inv g G B X
31 7 20 30 syl2anc Y NrmSGrp G A ˙ C B ˙ D inv g G B X
32 1 11 grpinvcl G Grp A X inv g G A X
33 7 15 32 syl2anc Y NrmSGrp G A ˙ C B ˙ D inv g G A X
34 1 3 grpass G Grp inv g G B X inv g G A X C + ˙ D X inv g G B + ˙ inv g G A + ˙ C + ˙ D = inv g G B + ˙ inv g G A + ˙ C + ˙ D
35 7 31 33 26 34 syl13anc Y NrmSGrp G A ˙ C B ˙ D inv g G B + ˙ inv g G A + ˙ C + ˙ D = inv g G B + ˙ inv g G A + ˙ C + ˙ D
36 29 35 eqtrd Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ B + ˙ C + ˙ D = inv g G B + ˙ inv g G A + ˙ C + ˙ D
37 1 3 grpass G Grp inv g G A X C X D X inv g G A + ˙ C + ˙ D = inv g G A + ˙ C + ˙ D
38 7 33 23 24 37 syl13anc Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C + ˙ D = inv g G A + ˙ C + ˙ D
39 38 oveq1d Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C + ˙ D + ˙ inv g G B = inv g G A + ˙ C + ˙ D + ˙ inv g G B
40 1 3 grpcl G Grp inv g G A X C X inv g G A + ˙ C X
41 7 33 23 40 syl3anc Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C X
42 1 3 grpass G Grp inv g G A + ˙ C X D X inv g G B X inv g G A + ˙ C + ˙ D + ˙ inv g G B = inv g G A + ˙ C + ˙ D + ˙ inv g G B
43 7 41 24 31 42 syl13anc Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C + ˙ D + ˙ inv g G B = inv g G A + ˙ C + ˙ D + ˙ inv g G B
44 39 43 eqtr3d Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C + ˙ D + ˙ inv g G B = inv g G A + ˙ C + ˙ D + ˙ inv g G B
45 14 simp3d Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C Y
46 19 simp3d Y NrmSGrp G A ˙ C B ˙ D inv g G B + ˙ D Y
47 simpl Y NrmSGrp G A ˙ C B ˙ D Y NrmSGrp G
48 1 3 nsgbi Y NrmSGrp G inv g G B X D X inv g G B + ˙ D Y D + ˙ inv g G B Y
49 47 31 24 48 syl3anc Y NrmSGrp G A ˙ C B ˙ D inv g G B + ˙ D Y D + ˙ inv g G B Y
50 46 49 mpbid Y NrmSGrp G A ˙ C B ˙ D D + ˙ inv g G B Y
51 3 subgcl Y SubGrp G inv g G A + ˙ C Y D + ˙ inv g G B Y inv g G A + ˙ C + ˙ D + ˙ inv g G B Y
52 5 45 50 51 syl3anc Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C + ˙ D + ˙ inv g G B Y
53 44 52 eqeltrd Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C + ˙ D + ˙ inv g G B Y
54 1 3 grpcl G Grp inv g G A X C + ˙ D X inv g G A + ˙ C + ˙ D X
55 7 33 26 54 syl3anc Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C + ˙ D X
56 1 3 nsgbi Y NrmSGrp G inv g G A + ˙ C + ˙ D X inv g G B X inv g G A + ˙ C + ˙ D + ˙ inv g G B Y inv g G B + ˙ inv g G A + ˙ C + ˙ D Y
57 47 55 31 56 syl3anc Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ C + ˙ D + ˙ inv g G B Y inv g G B + ˙ inv g G A + ˙ C + ˙ D Y
58 53 57 mpbid Y NrmSGrp G A ˙ C B ˙ D inv g G B + ˙ inv g G A + ˙ C + ˙ D Y
59 36 58 eqeltrd Y NrmSGrp G A ˙ C B ˙ D inv g G A + ˙ B + ˙ C + ˙ D Y
60 1 11 3 2 eqgval G Grp Y X A + ˙ B ˙ C + ˙ D A + ˙ B X C + ˙ D X inv g G A + ˙ B + ˙ C + ˙ D Y
61 7 10 60 syl2anc Y NrmSGrp G A ˙ C B ˙ D A + ˙ B ˙ C + ˙ D A + ˙ B X C + ˙ D X inv g G A + ˙ B + ˙ C + ˙ D Y
62 22 26 59 61 mpbir3and Y NrmSGrp G A ˙ C B ˙ D A + ˙ B ˙ C + ˙ D
63 62 ex Y NrmSGrp G A ˙ C B ˙ D A + ˙ B ˙ C + ˙ D