This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 ) ) → ( [ 𝑋 ] ∼ = 𝐻 ↔ 𝑋 ∈ 𝐻 ) )