Theorem 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={\mathrm{Base}}_G$$
	eqger.r	$$⊢\underset{\dot{}}{\sim }=G{~}_{\mathit{QG}}Y$$
	eqgid.3	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	eqgid	$$⊢Y\in \mathrm{SubGrp}\left(G\right)\to \left[\underset{\dot{}}{0}\right]\underset{\dot{}}{\sim }=Y$$

Proof

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