Metamath Proof Explorer

Theorem eqgen

Description: Each coset is equipotent to the subgroup itself (which is also the coset containing the identity). (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses eqger.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
eqger.r ⊢ ∼ = ( 𝐺 ~QG 𝑌 )
Assertion eqgen ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( 𝑋 / ∼ ) ) → 𝑌 ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 eqger.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 eqger.r ⊢ ∼ = ( 𝐺 ~QG 𝑌 )
3 eqid ⊢ ( 𝑋 / ∼ ) = ( 𝑋 / ∼ )
4 breq2 ⊢ ( [ 𝑥 ] ∼ = 𝐴 → ( 𝑌 ≈ [ 𝑥 ] ∼ ↔ 𝑌 ≈ 𝐴 ) )
5 simpl ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
6 subgrcl ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
7 1 subgss ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 ⊆ 𝑋 )
8 6 7 jca ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) )
9 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
10 1 2 9 eqglact ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → [ 𝑥 ] ∼ = ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) )
11 10 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → [ 𝑥 ] ∼ = ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) )
12 8 11 sylan ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → [ 𝑥 ] ∼ = ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) )
13 2 ovexi ⊢ ∼ ∈ V
14 ecexg ⊢ ( ∼ ∈ V → [ 𝑥 ] ∼ ∈ V )
15 13 14 ax-mp ⊢ [ 𝑥 ] ∼ ∈ V
16 12 15 eqeltrrdi ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) ∈ V )
17 eqid ⊢ ( 𝑦 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
18 17 1 9 grplactf1o ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝑥 ) : 𝑋 –1-1-onto→ 𝑋 )
19 17 1 grplactfval ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑦 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝑥 ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) )
20 19 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝑥 ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) )
21 f1oeq1 ⊢ ( ( ( 𝑦 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝑥 ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) → ( ( ( 𝑦 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝑥 ) : 𝑋 –1-1-onto→ 𝑋 ↔ ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 ) )
22 20 21 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑦 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝑥 ) : 𝑋 –1-1-onto→ 𝑋 ↔ ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 ) )
23 18 22 mpbid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 )
24 6 23 sylan ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 )
25 f1of1 ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 → ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1→ 𝑋 )
26 24 25 syl ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1→ 𝑋 )
27 7 adantr ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑌 ⊆ 𝑋 )
28 f1ores ⊢ ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1→ 𝑋 ∧ 𝑌 ⊆ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) ↾ 𝑌 ) : 𝑌 –1-1-onto→ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) )
29 26 27 28 syl2anc ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) ↾ 𝑌 ) : 𝑌 –1-1-onto→ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) )
30 f1oen2g ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) ∈ V ∧ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) ↾ 𝑌 ) : 𝑌 –1-1-onto→ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) ) → 𝑌 ≈ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) )
31 5 16 29 30 syl3anc ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑌 ≈ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑌 ) )
32 31 12 breqtrrd ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑌 ≈ [ 𝑥 ] ∼ )
33 3 4 32 ectocld ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( 𝑋 / ∼ ) ) → 𝑌 ≈ 𝐴 )