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	$⊢ X = {Base}_{G}$
	eqger.r	$⊢ \underset{˙}{\sim} = G ~_{QG} Y$
Assertion	eqgen	$⊢ (Y \in SubGrp (G) \land A \in (X / \underset{˙}{\sim})) \to Y \approx A$

Proof

Step	Hyp	Ref	Expression
1		eqger.x	$⊢ X = {Base}_{G}$
2		eqger.r	$⊢ \underset{˙}{\sim} = G ~_{QG} Y$
3		eqid	$⊢ X / \underset{˙}{\sim} = X / \underset{˙}{\sim}$
4		breq2	$⊢ [x] \underset{˙}{\sim} = A \to (Y \approx [x] \underset{˙}{\sim} \leftrightarrow Y \approx A)$
5		simpl	$⊢ (Y \in SubGrp (G) \land x \in X) \to Y \in SubGrp (G)$
6		subgrcl	$⊢ Y \in SubGrp (G) \to G \in Grp$
7	1	subgss	$⊢ Y \in SubGrp (G) \to Y \subseteq X$
8	6 7	jca	$⊢ Y \in SubGrp (G) \to (G \in Grp \land Y \subseteq X)$
9		eqid	$⊢ +_{G} = +_{G}$
10	1 2 9	eqglact	$⊢ (G \in Grp \land Y \subseteq X \land x \in X) \to [x] \underset{˙}{\sim} = (z \in X ⟼ x +_{G} z) [Y]$
11	10	3expa	$⊢ ((G \in Grp \land Y \subseteq X) \land x \in X) \to [x] \underset{˙}{\sim} = (z \in X ⟼ x +_{G} z) [Y]$
12	8 11	sylan	$⊢ (Y \in SubGrp (G) \land x \in X) \to [x] \underset{˙}{\sim} = (z \in X ⟼ x +_{G} z) [Y]$
13	2	ovexi	$⊢ \underset{˙}{\sim} \in V$
14		ecexg	$⊢ \underset{˙}{\sim} \in V \to [x] \underset{˙}{\sim} \in V$
15	13 14	ax-mp	$⊢ [x] \underset{˙}{\sim} \in V$
16	12 15	eqeltrrdi	$⊢ (Y \in SubGrp (G) \land x \in X) \to (z \in X ⟼ x +_{G} z) [Y] \in V$
17		eqid	$⊢ (y \in X ⟼ (z \in X ⟼ y +_{G} z)) = (y \in X ⟼ (z \in X ⟼ y +_{G} z))$
18	17 1 9	grplactf1o	$⊢ (G \in Grp \land x \in X) \to (y \in X ⟼ (z \in X ⟼ y +_{G} z)) (x) : X \underset{1-1 onto}{⟶} X$
19	17 1	grplactfval	$⊢ x \in X \to (y \in X ⟼ (z \in X ⟼ y +_{G} z)) (x) = (z \in X ⟼ x +_{G} z)$
20	19	adantl	$⊢ (G \in Grp \land x \in X) \to (y \in X ⟼ (z \in X ⟼ y +_{G} z)) (x) = (z \in X ⟼ x +_{G} z)$
21		f1oeq1	$⊢ (y \in X ⟼ (z \in X ⟼ y +_{G} z)) (x) = (z \in X ⟼ x +_{G} z) \to ((y \in X ⟼ (z \in X ⟼ y +_{G} z)) (x) : X \underset{1-1 onto}{⟶} X \leftrightarrow (z \in X ⟼ x +_{G} z) : X \underset{1-1 onto}{⟶} X)$
22	20 21	syl	$⊢ (G \in Grp \land x \in X) \to ((y \in X ⟼ (z \in X ⟼ y +_{G} z)) (x) : X \underset{1-1 onto}{⟶} X \leftrightarrow (z \in X ⟼ x +_{G} z) : X \underset{1-1 onto}{⟶} X)$
23	18 22	mpbid	$⊢ (G \in Grp \land x \in X) \to (z \in X ⟼ x +_{G} z) : X \underset{1-1 onto}{⟶} X$
24	6 23	sylan	$⊢ (Y \in SubGrp (G) \land x \in X) \to (z \in X ⟼ x +_{G} z) : X \underset{1-1 onto}{⟶} X$
25		f1of1	$⊢ (z \in X ⟼ x +_{G} z) : X \underset{1-1 onto}{⟶} X \to (z \in X ⟼ x +_{G} z) : X \underset{1-1}{⟶} X$
26	24 25	syl	$⊢ (Y \in SubGrp (G) \land x \in X) \to (z \in X ⟼ x +_{G} z) : X \underset{1-1}{⟶} X$
27	7	adantr	$⊢ (Y \in SubGrp (G) \land x \in X) \to Y \subseteq X$
28		f1ores	$⊢ ((z \in X ⟼ x +_{G} z) : X \underset{1-1}{⟶} X \land Y \subseteq X) \to ({(z \in X ⟼ x +_{G} z) ↾}_{Y}) : Y \underset{1-1 onto}{⟶} (z \in X ⟼ x +_{G} z) [Y]$
29	26 27 28	syl2anc	$⊢ (Y \in SubGrp (G) \land x \in X) \to ({(z \in X ⟼ x +_{G} z) ↾}_{Y}) : Y \underset{1-1 onto}{⟶} (z \in X ⟼ x +_{G} z) [Y]$
30		f1oen2g	$⊢ (Y \in SubGrp (G) \land (z \in X ⟼ x +_{G} z) [Y] \in V \land ({(z \in X ⟼ x +_{G} z) ↾}_{Y}) : Y \underset{1-1 onto}{⟶} (z \in X ⟼ x +_{G} z) [Y]) \to Y \approx (z \in X ⟼ x +_{G} z) [Y]$
31	5 16 29 30	syl3anc	$⊢ (Y \in SubGrp (G) \land x \in X) \to Y \approx (z \in X ⟼ x +_{G} z) [Y]$
32	31 12	breqtrrd	$⊢ (Y \in SubGrp (G) \land x \in X) \to Y \approx [x] \underset{˙}{\sim}$
33	3 4 32	ectocld	$⊢ (Y \in SubGrp (G) \land A \in (X / \underset{˙}{\sim})) \to Y \approx A$

Metamath Proof Explorer

Theorem eqgen

Proof