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 ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) “ 𝑌 ) )