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	grpinvcl	$⊢ (G \in Grp \land x \in X) \to {inv}_{g} (G) (x) \in X$
16	14 13 15	syl2anc	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) (x) \in X$
17	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))$
18	14 16 12 17	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))$
19	1 7	grpinvinv	$⊢ (G \in Grp \land x \in X) \to {inv}_{g} (G) ({inv}_{g} (G) (x)) = x$
20	14 13 19	syl2anc	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) ({inv}_{g} (G) (x)) = x$
21	20	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$
22	18 21	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$
23	11	simp3d	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) (x) +_{G} y \in Y$
24	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$
25	23 24	syldan	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) ({inv}_{g} (G) (x) +_{G} y) \in Y$
26	22 25	eqeltrrd	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to {inv}_{g} (G) (y) +_{G} x \in Y$
27	6	adantr	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to Y \subseteq X$
28	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))$
29	14 27 28	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))$
30	12 13 26 29	mpbir3and	$⊢ (Y \in SubGrp (G) \land x \underset{˙}{\sim} y) \to y \underset{˙}{\sim} x$
31	13	adantrr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x \in X$
32	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))$
33	5 6 32	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))$
34	33	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)$
35	34	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)$
36	35	simp2d	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to z \in X$
37	5	adantr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to G \in Grp$
38	37 31 15	syl2anc	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (x) \in X$
39	12	adantrr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to y \in X$
40	1 7	grpinvcl	$⊢ (G \in Grp \land y \in X) \to {inv}_{g} (G) (y) \in X$
41	37 39 40	syl2anc	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (y) \in X$
42	1 8	grpcl	$⊢ (G \in Grp \land {inv}_{g} (G) (y) \in X \land z \in X) \to {inv}_{g} (G) (y) +_{G} z \in X$
43	37 41 36 42	syl3anc	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (y) +_{G} z \in X$
44	1 8	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (x) \in X \land y \in X \land {inv}_{g} (G) (y) +_{G} z \in X)) \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))$
45	37 38 39 43 44	syl13anc	$⊢ (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))$
46		eqid	$⊢ 0_{G} = 0_{G}$
47	1 8 46 7	grprinv	$⊢ (G \in Grp \land y \in X) \to y +_{G} {inv}_{g} (G) (y) = 0_{G}$
48	37 39 47	syl2anc	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to y +_{G} {inv}_{g} (G) (y) = 0_{G}$
49	48	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$
50	1 8	grpass	$⊢ (G \in Grp \land (y \in X \land {inv}_{g} (G) (y) \in X \land z \in X)) \to (y +_{G} {inv}_{g} (G) (y)) +_{G} z = y +_{G} ({inv}_{g} (G) (y) +_{G} z)$
51	37 39 41 36 50	syl13anc	$⊢ (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)$
52	1 8 46	grplid	$⊢ (G \in Grp \land z \in X) \to 0_{G} +_{G} z = z$
53	37 36 52	syl2anc	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to 0_{G} +_{G} z = z$
54	49 51 53	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$
55	54	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$
56	45 55	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$
57		simpl	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to Y \in SubGrp (G)$
58	23	adantrr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (x) +_{G} y \in Y$
59	35	simp3d	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (y) +_{G} z \in Y$
60	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$
61	57 58 59 60	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$
62	56 61	eqeltrrd	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to {inv}_{g} (G) (x) +_{G} z \in Y$
63	6	adantr	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to Y \subseteq X$
64	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))$
65	37 63 64	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))$
66	31 36 62 65	mpbir3and	$⊢ (Y \in SubGrp (G) \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x \underset{˙}{\sim} z$
67	1 8 46 7	grplinv	$⊢ (G \in Grp \land x \in X) \to {inv}_{g} (G) (x) +_{G} x = 0_{G}$
68	5 67	sylan	$⊢ (Y \in SubGrp (G) \land x \in X) \to {inv}_{g} (G) (x) +_{G} x = 0_{G}$
69	46	subg0cl	$⊢ Y \in SubGrp (G) \to 0_{G} \in Y$
70	69	adantr	$⊢ (Y \in SubGrp (G) \land x \in X) \to 0_{G} \in Y$
71	68 70	eqeltrd	$⊢ (Y \in SubGrp (G) \land x \in X) \to {inv}_{g} (G) (x) +_{G} x \in Y$
72	71	ex	$⊢ Y \in SubGrp (G) \to (x \in X \to {inv}_{g} (G) (x) +_{G} x \in Y)$
73	72	pm4.71rd	$⊢ Y \in SubGrp (G) \to (x \in X \leftrightarrow ({inv}_{g} (G) (x) +_{G} x \in Y \land x \in X))$
74	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))$
75	5 6 74	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))$
76		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)$
77		anidm	$⊢ (x \in X \land x \in X) \leftrightarrow x \in X$
78	77	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)$
79	76 78	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)$
80	75 79	syl6bb	$⊢ Y \in SubGrp (G) \to (x \underset{˙}{\sim} x \leftrightarrow ({inv}_{g} (G) (x) +_{G} x \in Y \land x \in X))$
81	73 80	bitr4d	$⊢ Y \in SubGrp (G) \to (x \in X \leftrightarrow x \underset{˙}{\sim} x)$
82	4 30 66 81	iserd	$⊢ Y \in SubGrp (G) \to \underset{˙}{\sim} Er X$

Metamath Proof Explorer

Theorem eqger

Proof