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