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 𝑋 = ( Base ‘ 𝐺 )
eqger.r = ( 𝐺 ~QG 𝑌 )
Assertion eqger ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → Er 𝑋 )

Proof

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