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	$⊢ X = {Base}_{G}$
	eqger.r	$⊢ \underset{˙}{\sim} = G ~_{QG} Y$
	eqglact.3	$⊢ \underset{˙}{+} = +_{G}$
Assertion	eqglact	$⊢ (G \in Grp \land Y \subseteq X \land A \in X) \to [A] \underset{˙}{\sim} = (x \in X ⟼ A \underset{˙}{+} x) [Y]$

Proof

Step	Hyp	Ref	Expression
1		eqger.x	$⊢ X = {Base}_{G}$
2		eqger.r	$⊢ \underset{˙}{\sim} = G ~_{QG} Y$
3		eqglact.3	$⊢ \underset{˙}{+} = +_{G}$
4		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
5	1 4 3 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to (A \underset{˙}{\sim} x \leftrightarrow (A \in X \land x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y))$
6		3anass	$⊢ (A \in X \land x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y) \leftrightarrow (A \in X \land (x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y))$
7	5 6	bitrdi	$⊢ (G \in Grp \land Y \subseteq X) \to (A \underset{˙}{\sim} x \leftrightarrow (A \in X \land (x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y)))$
8	7	baibd	$⊢ ((G \in Grp \land Y \subseteq X) \land A \in X) \to (A \underset{˙}{\sim} x \leftrightarrow (x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y))$
9	8	3impa	$⊢ (G \in Grp \land Y \subseteq X \land A \in X) \to (A \underset{˙}{\sim} x \leftrightarrow (x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y))$
10	9	abbidv	$⊢ (G \in Grp \land Y \subseteq X \land A \in X) \to \{x \| A \underset{˙}{\sim} x\} = \{x \| (x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y)\}$
11		dfec2	$⊢ A \in X \to [A] \underset{˙}{\sim} = \{x \| A \underset{˙}{\sim} x\}$
12	11	3ad2ant3	$⊢ (G \in Grp \land Y \subseteq X \land A \in X) \to [A] \underset{˙}{\sim} = \{x \| A \underset{˙}{\sim} x\}$
13		eqid	$⊢ (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) = (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x))$
14	13 1 3 4	grplactcnv	$⊢ (G \in Grp \land A \in X) \to ((g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A) : X \underset{1-1 onto}{⟶} X \land {(g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A)}^{-1} = (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) ({inv}_{g} (G) (A)))$
15	14	simprd	$⊢ (G \in Grp \land A \in X) \to {(g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A)}^{-1} = (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) ({inv}_{g} (G) (A))$
16	13 1	grplactfval	$⊢ A \in X \to (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A) = (x \in X ⟼ A \underset{˙}{+} x)$
17	16	adantl	$⊢ (G \in Grp \land A \in X) \to (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A) = (x \in X ⟼ A \underset{˙}{+} x)$
18	17	cnveqd	$⊢ (G \in Grp \land A \in X) \to {(g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A)}^{-1} = {(x \in X ⟼ A \underset{˙}{+} x)}^{-1}$
19	1 4	grpinvcl	$⊢ (G \in Grp \land A \in X) \to {inv}_{g} (G) (A) \in X$
20	13 1	grplactfval	$⊢ {inv}_{g} (G) (A) \in X \to (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) ({inv}_{g} (G) (A)) = (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)$
21	19 20	syl	$⊢ (G \in Grp \land A \in X) \to (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) ({inv}_{g} (G) (A)) = (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)$
22	15 18 21	3eqtr3d	$⊢ (G \in Grp \land A \in X) \to {(x \in X ⟼ A \underset{˙}{+} x)}^{-1} = (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)$
23	22	cnveqd	$⊢ (G \in Grp \land A \in X) \to {(x \in X ⟼ A \underset{˙}{+} x)}^{-1}^{-1} = {(x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)}^{-1}$
24	23	3adant2	$⊢ (G \in Grp \land Y \subseteq X \land A \in X) \to {(x \in X ⟼ A \underset{˙}{+} x)}^{-1}^{-1} = {(x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)}^{-1}$
25	24	imaeq1d	$⊢ (G \in Grp \land Y \subseteq X \land A \in X) \to {(x \in X ⟼ A \underset{˙}{+} x)}^{-1}^{-1} [Y] = {(x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)}^{-1} [Y]$
26		imacnvcnv	$⊢ {(x \in X ⟼ A \underset{˙}{+} x)}^{-1}^{-1} [Y] = (x \in X ⟼ A \underset{˙}{+} x) [Y]$
27		eqid	$⊢ (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x) = (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)$
28	27	mptpreima	$⊢ {(x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)}^{-1} [Y] = \{x \in X \| {inv}_{g} (G) (A) \underset{˙}{+} x \in Y\}$
29		df-rab	$⊢ \{x \in X \| {inv}_{g} (G) (A) \underset{˙}{+} x \in Y\} = \{x \| (x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y)\}$
30	28 29	eqtri	$⊢ {(x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)}^{-1} [Y] = \{x \| (x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y)\}$
31	25 26 30	3eqtr3g	$⊢ (G \in Grp \land Y \subseteq X \land A \in X) \to (x \in X ⟼ A \underset{˙}{+} x) [Y] = \{x \| (x \in X \land {inv}_{g} (G) (A) \underset{˙}{+} x \in Y)\}$
32	10 12 31	3eqtr4d	$⊢ (G \in Grp \land Y \subseteq X \land A \in X) \to [A] \underset{˙}{\sim} = (x \in X ⟼ A \underset{˙}{+} x) [Y]$

Metamath Proof Explorer

Theorem eqglact

Proof