eqger

Description: The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		eqger.x	$⊢ X = {Base}_{G}$
2		eqger.r	$⊢ \underset{˙}{\sim} = G ~_{QG} Y$
3	2	releqg	$⊢ Rel \underset{˙}{\sim}$
4	3	a1i	$⊢ Y \in SubGrp (G) \to Rel \underset{˙}{\sim}$
5		subgrcl	$⊢ Y \in SubGrp (G) \to G \in Grp$
6	1	subgss	$⊢ Y \in SubGrp (G) \to Y \subseteq X$
7		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
8		eqid	$⊢ +_{G} = +_{G}$
9	1 7 8 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to (x \underset{˙}{\sim} y \leftrightarrow (x \in X \land y \in X \land {inv}_{g} (G) (x) +_{G} y \in Y))$
10	5 6 9	syl2anc	$⊢ Y \in SubGrp (G) \to (x \underset{˙}{\sim} y \leftrightarrow (x \in X \land y \in X \land {inv}_{g} (G) (x) +_{G} y \in Y))$
11	10	biimpa	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to (x \in X \land y \in X \land {inv}_{g} (G) (x) +_{G} y \in Y)$
12	11	simp2d	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to y \in X$
13	11	simp1d	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to x \in X$
14	5	adantr	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to G \in Grp$
15	1 7 14 13	grpinvcld	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) (x) \in X$
16	1 8 7	grpinvadd	$⊢ (G \in Grp \land {inv}_{g} (G) (x) \in X \land y \in X) \to {inv}_{g} (G) ({inv}_{g} (G) (x) +_{G} y) = {inv}_{g} (G) (y) +_{G} {inv}_{g} (G) ({inv}_{g} (G) (x))$
17	14 15 12 16	syl3anc	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) ({inv}_{g} (G) (x) +_{G} y) = {inv}_{g} (G) (y) +_{G} {inv}_{g} (G) ({inv}_{g} (G) (x))$
18	1 7	grpinvinv	$⊢ (G \in Grp \land x \in X) \to {inv}_{g} (G) ({inv}_{g} (G) (x)) = x$
19	14 13 18	syl2anc	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) ({inv}_{g} (G) (x)) = x$
20	19	oveq2d	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) (y) +_{G} {inv}_{g} (G) ({inv}_{g} (G) (x)) = {inv}_{g} (G) (y) +_{G} x$
21	17 20	eqtrd	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) ({inv}_{g} (G) (x) +_{G} y) = {inv}_{g} (G) (y) +_{G} x$
22	11	simp3d	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) (x) +_{G} y \in Y$
23	7	subginvcl	$⊢ (Y \in SubGrp (G) \land {inv}_{g} (G) (x) +_{G} y \in Y) \to {inv}_{g} (G) ({inv}_{g} (G) (x) +_{G} y) \in Y$
24	22 23	syldan	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) ({inv}_{g} (G) (x) +_{G} y) \in Y$
25	21 24	eqeltrrd	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) (y) +_{G} x \in Y$
26	6	adantr	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to Y \subseteq X$
27	1 7 8 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in X \land x \in X \land {inv}_{g} (G) (y) +_{G} x \in Y))$
28	14 26 27	syl2anc	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in X \land x \in X \land {inv}_{g} (G) (y) +_{G} x \in Y))$
29	12 13 25 28	mpbir3and	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to y \underset{˙}{\sim} x$
30	13	adantrr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x \in X$
31	1 7 8 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to (y \underset{˙}{\sim} z \leftrightarrow (y \in X \land z \in X \land {inv}_{g} (G) (y) +_{G} z \in Y))$
32	5 6 31	syl2anc	$⊢ Y \in SubGrp (G) \to (y \underset{˙}{\sim} z \leftrightarrow (y \in X \land z \in X \land {inv}_{g} (G) (y) +_{G} z \in Y))$
33	32	biimpa	$⊢ (Y \in SubGrp (G) \land y \underset{˙}{\sim} z) \to (y \in X \land z \in X \land {inv}_{g} (G) (y) +_{G} z \in Y)$
34	33	adantrl	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to (y \in X \land z \in X \land {inv}_{g} (G) (y) +_{G} z \in Y)$
35	34	simp2d	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to z \in X$
36	5	adantr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to G \in Grp$
37	1 7 36 30	grpinvcld	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (x) \in X$
38	12	adantrr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to y \in X$
39	1 7 36 38	grpinvcld	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (y) \in X$
40	1 8 36 39 35	grpcld	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (y) +_{G} z \in X$
41	1 8 36 37 38 40	grpassd	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to ({inv}_{g} (G) (x) +_{G} y) +_{G} ({inv}_{g} (G) (y) +_{G} z) = {inv}_{g} (G) (x) +_{G} (y +_{G} ({inv}_{g} (G) (y) +_{G} z))$
42		eqid	$⊢ 0_{G} = 0_{G}$
43	1 8 42 7	grprinv	$⊢ (G \in Grp \land y \in X) \to y +_{G} {inv}_{g} (G) (y) = 0_{G}$
44	36 38 43	syl2anc	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to y +_{G} {inv}_{g} (G) (y) = 0_{G}$
45	44	oveq1d	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to (y +_{G} {inv}_{g} (G) (y)) +_{G} z = 0_{G} +_{G} z$
46	1 8 36 38 39 35	grpassd	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to (y +_{G} {inv}_{g} (G) (y)) +_{G} z = y +_{G} ({inv}_{g} (G) (y) +_{G} z)$
47	1 8 42 36 35	grplidd	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to 0_{G} +_{G} z = z$
48	45 46 47	3eqtr3d	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to y +_{G} ({inv}_{g} (G) (y) +_{G} z) = z$
49	48	oveq2d	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (x) +_{G} (y +_{G} ({inv}_{g} (G) (y) +_{G} z)) = {inv}_{g} (G) (x) +_{G} z$
50	41 49	eqtrd	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to ({inv}_{g} (G) (x) +_{G} y) +_{G} ({inv}_{g} (G) (y) +_{G} z) = {inv}_{g} (G) (x) +_{G} z$
51		simpl	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to Y \in SubGrp (G)$
52	22	adantrr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (x) +_{G} y \in Y$
53	34	simp3d	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (y) +_{G} z \in Y$
54	8	subgcl	$⊢ (Y \in SubGrp (G) \land {inv}_{g} (G) (x) +_{G} y \in Y \land {inv}_{g} (G) (y) +_{G} z \in Y) \to ({inv}_{g} (G) (x) +_{G} y) +_{G} ({inv}_{g} (G) (y) +_{G} z) \in Y$
55	51 52 53 54	syl3anc	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to ({inv}_{g} (G) (x) +_{G} y) +_{G} ({inv}_{g} (G) (y) +_{G} z) \in Y$
56	50 55	eqeltrrd	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (x) +_{G} z \in Y$
57	6	adantr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to Y \subseteq X$
58	1 7 8 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to (x \underset{˙}{\sim} z \leftrightarrow (x \in X \land z \in X \land {inv}_{g} (G) (x) +_{G} z \in Y))$
59	36 57 58	syl2anc	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to (x \underset{˙}{\sim} z \leftrightarrow (x \in X \land z \in X \land {inv}_{g} (G) (x) +_{G} z \in Y))$
60	30 35 56 59	mpbir3and	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x \underset{˙}{\sim} z$
61	1 8 42 7	grplinv	$⊢ (G \in Grp \land x \in X) \to {inv}_{g} (G) (x) +_{G} x = 0_{G}$
62	5 61	sylan	$⊢ (Y \in SubGrp (G) \land x \in X) \to {inv}_{g} (G) (x) +_{G} x = 0_{G}$
63	42	subg0cl	$⊢ Y \in SubGrp (G) \to 0_{G} \in Y$
64	63	adantr	$⊢ (Y \in SubGrp (G) \land x \in X) \to 0_{G} \in Y$
65	62 64	eqeltrd	$⊢ (Y \in SubGrp (G) \land x \in X) \to {inv}_{g} (G) (x) +_{G} x \in Y$
66	65	ex	$⊢ Y \in SubGrp (G) \to (x \in X \to {inv}_{g} (G) (x) +_{G} x \in Y)$
67	66	pm4.71rd	$⊢ Y \in SubGrp (G) \to (x \in X \leftrightarrow ({inv}_{g} (G) (x) +_{G} x \in Y \land x \in X))$
68	1 7 8 2	eqgval	$⊢ (G \in Grp \land Y \subseteq X) \to (x \underset{˙}{\sim} x \leftrightarrow (x \in X \land x \in X \land {inv}_{g} (G) (x) +_{G} x \in Y))$
69	5 6 68	syl2anc	$⊢ Y \in SubGrp (G) \to (x \underset{˙}{\sim} x \leftrightarrow (x \in X \land x \in X \land {inv}_{g} (G) (x) +_{G} x \in Y))$
70		df-3an	$⊢ (x \in X \land x \in X \land {inv}_{g} (G) (x) +_{G} x \in Y) \leftrightarrow ((x \in X \land x \in X) \land {inv}_{g} (G) (x) +_{G} x \in Y)$
71		anidm	$⊢ (x \in X \land x \in X) \leftrightarrow x \in X$
72	71	anbi2ci	$⊢ ((x \in X \land x \in X) \land {inv}_{g} (G) (x) +_{G} x \in Y) \leftrightarrow ({inv}_{g} (G) (x) +_{G} x \in Y \land x \in X)$
73	70 72	bitri	$⊢ (x \in X \land x \in X \land {inv}_{g} (G) (x) +_{G} x \in Y) \leftrightarrow ({inv}_{g} (G) (x) +_{G} x \in Y \land x \in X)$
74	69 73	bitrdi	$⊢ Y \in SubGrp (G) \to (x \underset{˙}{\sim} x \leftrightarrow ({inv}_{g} (G) (x) +_{G} x \in Y \land x \in X))$
75	67 74	bitr4d	$⊢ Y \in SubGrp (G) \to (x \in X \leftrightarrow x \underset{˙}{\sim} x)$
76	4 29 60 75	iserd	$⊢ Y \in SubGrp (G) \to \underset{˙}{\sim} Er X$

Metamath Proof Explorer

Theorem eqger

Proof