eqgid

Description: The left coset containing the identity is the original subgroup. (Contributed by Mario Carneiro, 20-Sep-2015)

	Ref	Expression
Hypotheses	eqger.x	$⊢ X = {Base}_{G}$
	eqger.r	$⊢ \underset{˙}{\sim} = G ~_{QG} Y$
	eqgid.3	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	eqgid	$⊢ Y \in SubGrp (G) \to [\underset{˙}{0}] \underset{˙}{\sim} = Y$

Proof

Step	Hyp	Ref	Expression
1		eqger.x	$⊢ X = {Base}_{G}$
2		eqger.r	$⊢ \underset{˙}{\sim} = G ~_{QG} Y$
3		eqgid.3	$⊢ \underset{˙}{0} = 0_{G}$
4	2	releqg	$⊢ Rel \underset{˙}{\sim}$
5		relelec	$⊢ Rel \underset{˙}{\sim} \to (x \in [\underset{˙}{0}] \underset{˙}{\sim} \leftrightarrow \underset{˙}{0} \underset{˙}{\sim} x)$
6	4 5	ax-mp	$⊢ x \in [\underset{˙}{0}] \underset{˙}{\sim} \leftrightarrow \underset{˙}{0} \underset{˙}{\sim} x$
7		subgrcl	$⊢ Y \in SubGrp (G) \to G \in Grp$
8	7	adantr	$⊢ (Y \in SubGrp (G) \land x \in X) \to G \in Grp$
9		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
10	3 9	grpinvid	$⊢ G \in Grp \to {inv}_{g} (G) (\underset{˙}{0}) = \underset{˙}{0}$
11	8 10	syl	$⊢ (Y \in SubGrp (G) \land x \in X) \to {inv}_{g} (G) (\underset{˙}{0}) = \underset{˙}{0}$
12	11	oveq1d	$⊢ (Y \in SubGrp (G) \land x \in X) \to {inv}_{g} (G) (\underset{˙}{0}) +_{G} x = \underset{˙}{0} +_{G} x$
13		eqid	$⊢ +_{G} = +_{G}$
14	1 13 3	grplid	$⊢ (G \in Grp \land x \in X) \to \underset{˙}{0} +_{G} x = x$
15	7 14	sylan	$⊢ (Y \in SubGrp (G) \land x \in X) \to \underset{˙}{0} +_{G} x = x$
16	12 15	eqtrd	$⊢ (Y \in SubGrp (G) \land x \in X) \to {inv}_{g} (G) (\underset{˙}{0}) +_{G} x = x$
17	16	eleq1d	$⊢ (Y \in SubGrp (G) \land x \in X) \to ({inv}_{g} (G) (\underset{˙}{0}) +_{G} x \in Y \leftrightarrow x \in Y)$
18	17	pm5.32da	$⊢ Y \in SubGrp (G) \to ((x \in X \land {inv}_{g} (G) (\underset{˙}{0}) +_{G} x \in Y) \leftrightarrow (x \in X \land x \in Y))$
19	1	subgss	$⊢ Y \in SubGrp (G) \to Y \subseteq X$
20	1 3	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in X$
21	7 20	syl	$⊢ Y \in SubGrp (G) \to \underset{˙}{0} \in X$
22	1 9 13 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to (\underset{˙}{0} \underset{˙}{\sim} x \leftrightarrow (\underset{˙}{0} \in X \land x \in X \land {inv}_{g} (G) (\underset{˙}{0}) +_{G} x \in Y))$
23		3anass	$⊢ (\underset{˙}{0} \in X \land x \in X \land {inv}_{g} (G) (\underset{˙}{0}) +_{G} x \in Y) \leftrightarrow (\underset{˙}{0} \in X \land (x \in X \land {inv}_{g} (G) (\underset{˙}{0}) +_{G} x \in Y))$
24	22 23	bitrdi	$⊢ (G \in Grp \land Y \subseteq X) \to (\underset{˙}{0} \underset{˙}{\sim} x \leftrightarrow (\underset{˙}{0} \in X \land (x \in X \land {inv}_{g} (G) (\underset{˙}{0}) +_{G} x \in Y)))$
25	24	baibd	$⊢ ((G \in Grp \land Y \subseteq X) \land \underset{˙}{0} \in X) \to (\underset{˙}{0} \underset{˙}{\sim} x \leftrightarrow (x \in X \land {inv}_{g} (G) (\underset{˙}{0}) +_{G} x \in Y))$
26	7 19 21 25	syl21anc	$⊢ Y \in SubGrp (G) \to (\underset{˙}{0} \underset{˙}{\sim} x \leftrightarrow (x \in X \land {inv}_{g} (G) (\underset{˙}{0}) +_{G} x \in Y))$
27	19	sseld	$⊢ Y \in SubGrp (G) \to (x \in Y \to x \in X)$
28	27	pm4.71rd	$⊢ Y \in SubGrp (G) \to (x \in Y \leftrightarrow (x \in X \land x \in Y))$
29	18 26 28	3bitr4d	$⊢ Y \in SubGrp (G) \to (\underset{˙}{0} \underset{˙}{\sim} x \leftrightarrow x \in Y)$
30	6 29	bitrid	$⊢ Y \in SubGrp (G) \to (x \in [\underset{˙}{0}] \underset{˙}{\sim} \leftrightarrow x \in Y)$
31	30	eqrdv	$⊢ Y \in SubGrp (G) \to [\underset{˙}{0}] \underset{˙}{\sim} = Y$

Metamath Proof Explorer

Theorem eqgid

Proof