Metamath Proof Explorer


Theorem eqg0el

Description: Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024)

Ref Expression
Hypothesis eqg0el.1 = ( 𝐺 ~QG 𝐻 )
Assertion eqg0el ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( [ 𝑋 ] = 𝐻𝑋𝐻 ) )

Proof

Step Hyp Ref Expression
1 eqg0el.1 = ( 𝐺 ~QG 𝐻 )
2 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 2 1 eqger ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → Er ( Base ‘ 𝐺 ) )
4 3 adantl ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → Er ( Base ‘ 𝐺 ) )
5 eqid ( 0g𝐺 ) = ( 0g𝐺 )
6 2 5 grpidcl ( 𝐺 ∈ Grp → ( 0g𝐺 ) ∈ ( Base ‘ 𝐺 ) )
7 6 adantr ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 0g𝐺 ) ∈ ( Base ‘ 𝐺 ) )
8 4 7 erth ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 0g𝐺 ) 𝑋 ↔ [ ( 0g𝐺 ) ] = [ 𝑋 ] ) )
9 2 1 5 eqgid ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → [ ( 0g𝐺 ) ] = 𝐻 )
10 9 adantl ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → [ ( 0g𝐺 ) ] = 𝐻 )
11 10 eqeq1d ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( [ ( 0g𝐺 ) ] = [ 𝑋 ] 𝐻 = [ 𝑋 ] ) )
12 eqcom ( 𝐻 = [ 𝑋 ] ↔ [ 𝑋 ] = 𝐻 )
13 12 a1i ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐻 = [ 𝑋 ] ↔ [ 𝑋 ] = 𝐻 ) )
14 8 11 13 3bitrrd ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( [ 𝑋 ] = 𝐻 ↔ ( 0g𝐺 ) 𝑋 ) )
15 errel ( Er ( Base ‘ 𝐺 ) → Rel )
16 relelec ( Rel → ( 𝑋 ∈ [ ( 0g𝐺 ) ] ↔ ( 0g𝐺 ) 𝑋 ) )
17 3 15 16 3syl ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑋 ∈ [ ( 0g𝐺 ) ] ↔ ( 0g𝐺 ) 𝑋 ) )
18 17 adantl ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑋 ∈ [ ( 0g𝐺 ) ] ↔ ( 0g𝐺 ) 𝑋 ) )
19 10 eleq2d ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑋 ∈ [ ( 0g𝐺 ) ] 𝑋𝐻 ) )
20 14 18 19 3bitr2d ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( [ 𝑋 ] = 𝐻𝑋𝐻 ) )