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

Metamath Proof Explorer

Theorem eqglact

Description: A left coset can be expressed as the image of a left action. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses eqger.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
eqger.r ⊢ ∼ = ( 𝐺 ~QG 𝑌 )
eqglact.3 ⊢ + = ( +g ‘ 𝐺 )
Assertion eqglact ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) “ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 eqger.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 eqger.r ⊢ ∼ = ( 𝐺 ~QG 𝑌 )
3 eqglact.3 ⊢ + = ( +g ‘ 𝐺 )
4 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
5 1 4 3 2 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐴 ∼ 𝑥 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) ) )
6 3anass ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) ) )
7 5 6 bitrdi ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐴 ∼ 𝑥 ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) ) ) )
8 7 baibd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) ) )
9 8 3impa ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) ) )
10 9 abbidv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∣ 𝐴 ∼ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) } )
11 dfec2 ⊢ ( 𝐴 ∈ 𝑋 → [ 𝐴 ] ∼ = { 𝑥 ∣ 𝐴 ∼ 𝑥 } )
12 11 3ad2ant3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = { 𝑥 ∣ 𝐴 ∼ 𝑥 } )
13 eqid ⊢ ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) = ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) )
14 13 1 3 4 grplactcnv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) ) )
15 14 simprd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ◡ ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) )
16 13 1 grplactfval ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) )
17 16 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) )
18 17 cnveqd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ◡ ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ◡ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) )
19 1 4 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
20 13 1 grplactfval ⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) )
21 19 20 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) )
22 15 18 21 3eqtr3d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ◡ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) )
23 22 cnveqd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ◡ ◡ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) = ◡ ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) )
24 23 3adant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ◡ ◡ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) = ◡ ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) )
25 24 imaeq1d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ◡ ◡ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) “ 𝑌 ) = ( ◡ ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) “ 𝑌 ) )
26 imacnvcnv ⊢ ( ◡ ◡ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) “ 𝑌 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) “ 𝑌 )
27 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) )
28 27 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) “ 𝑌 ) = { 𝑥 ∈ 𝑋 ∣ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 }
29 df-rab ⊢ { 𝑥 ∈ 𝑋 ∣ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 } = { 𝑥 ∣ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) }
30 28 29 eqtri ⊢ ( ◡ ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) “ 𝑌 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) }
31 25 26 30 3eqtr3g ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) “ 𝑌 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ∈ 𝑌 ) } )
32 10 12 31 3eqtr4d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) “ 𝑌 ) )