qusgrp

Description: If Y is a normal subgroup of G , then H = G / Y is a group, called the quotient of G by Y . (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 12-Aug-2015)

		Ref	Expression
	Hypothesis	qusgrp.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
	Assertion	qusgrp	$⊢ S \in NrmSGrp (G) \to H \in Grp$

Proof

Step	Hyp	Ref	Expression
1		qusgrp.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
2	1	a1i	$⊢ S \in NrmSGrp (G) \to H = G /_{𝑠} (G ~_{QG} S)$
3		eqidd	$⊢ S \in NrmSGrp (G) \to {Base}_{G} = {Base}_{G}$
4		eqidd	$⊢ S \in NrmSGrp (G) \to +_{G} = +_{G}$
5		nsgsubg	$⊢ S \in NrmSGrp (G) \to S \in SubGrp (G)$
6		eqid	$⊢ {Base}_{G} = {Base}_{G}$
7		eqid	$⊢ G ~_{QG} S = G ~_{QG} S$
8	6 7	eqger	$⊢ S \in SubGrp (G) \to (G ~_{QG} S) Er {Base}_{G}$
9	5 8	syl	$⊢ S \in NrmSGrp (G) \to (G ~_{QG} S) Er {Base}_{G}$
10		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
11	5 10	syl	$⊢ S \in NrmSGrp (G) \to G \in Grp$
12		eqid	$⊢ +_{G} = +_{G}$
13	6 7 12	eqgcpbl	$⊢ S \in NrmSGrp (G) \to ((a (G ~_{QG} S) c \land b (G ~_{QG} S) d) \to (a +_{G} b) (G ~_{QG} S) (c +_{G} d))$
14	6 12	grpcl	$⊢ (G \in Grp \land u \in {Base}_{G} \land v \in {Base}_{G}) \to u +_{G} v \in {Base}_{G}$
15	11 14	syl3an1	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G} \land v \in {Base}_{G}) \to u +_{G} v \in {Base}_{G}$
16	9	adantr	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to (G ~_{QG} S) Er {Base}_{G}$
17	11	adantr	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to G \in Grp$
18		simpr1	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to u \in {Base}_{G}$
19		simpr2	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to v \in {Base}_{G}$
20	17 18 19 14	syl3anc	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to u +_{G} v \in {Base}_{G}$
21		simpr3	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to w \in {Base}_{G}$
22	6 12	grpcl	$⊢ (G \in Grp \land u +_{G} v \in {Base}_{G} \land w \in {Base}_{G}) \to (u +_{G} v) +_{G} w \in {Base}_{G}$
23	17 20 21 22	syl3anc	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to (u +_{G} v) +_{G} w \in {Base}_{G}$
24	16 23	erref	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to ((u +_{G} v) +_{G} w) (G ~_{QG} S) ((u +_{G} v) +_{G} w)$
25	6 12	grpass	$⊢ (G \in Grp \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to (u +_{G} v) +_{G} w = u +_{G} (v +_{G} w)$
26	11 25	sylan	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to (u +_{G} v) +_{G} w = u +_{G} (v +_{G} w)$
27	24 26	breqtrd	$⊢ (S \in NrmSGrp (G) \land (u \in {Base}_{G} \land v \in {Base}_{G} \land w \in {Base}_{G})) \to ((u +_{G} v) +_{G} w) (G ~_{QG} S) (u +_{G} (v +_{G} w))$
28		eqid	$⊢ 0_{G} = 0_{G}$
29	6 28	grpidcl	$⊢ G \in Grp \to 0_{G} \in {Base}_{G}$
30	11 29	syl	$⊢ S \in NrmSGrp (G) \to 0_{G} \in {Base}_{G}$
31	6 12 28	grplid	$⊢ (G \in Grp \land u \in {Base}_{G}) \to 0_{G} +_{G} u = u$
32	11 31	sylan	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to 0_{G} +_{G} u = u$
33	9	adantr	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to (G ~_{QG} S) Er {Base}_{G}$
34		simpr	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to u \in {Base}_{G}$
35	33 34	erref	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to u (G ~_{QG} S) u$
36	32 35	eqbrtrd	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to (0_{G} +_{G} u) (G ~_{QG} S) u$
37		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
38	6 37	grpinvcl	$⊢ (G \in Grp \land u \in {Base}_{G}) \to {inv}_{g} (G) (u) \in {Base}_{G}$
39	11 38	sylan	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to {inv}_{g} (G) (u) \in {Base}_{G}$
40	6 12 28 37	grplinv	$⊢ (G \in Grp \land u \in {Base}_{G}) \to {inv}_{g} (G) (u) +_{G} u = 0_{G}$
41	11 40	sylan	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to {inv}_{g} (G) (u) +_{G} u = 0_{G}$
42	30	adantr	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to 0_{G} \in {Base}_{G}$
43	33 42	erref	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to 0_{G} (G ~_{QG} S) 0_{G}$
44	41 43	eqbrtrd	$⊢ (S \in NrmSGrp (G) \land u \in {Base}_{G}) \to ({inv}_{g} (G) (u) +_{G} u) (G ~_{QG} S) 0_{G}$
45	2 3 4 9 11 13 15 27 30 36 39 44	qusgrp2	$⊢ S \in NrmSGrp (G) \to (H \in Grp \land [0_{G}] (G ~_{QG} S) = 0_{H})$
46	45	simpld	$⊢ S \in NrmSGrp (G) \to H \in Grp$

Metamath Proof Explorer

Theorem qusgrp

Proof