qusabl

Description: If Y is a subgroup of the abelian group G , then H = G / Y is an abelian group. (Contributed by Mario Carneiro, 26-Apr-2016)

		Ref	Expression
	Hypothesis	qusabl.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
	Assertion	qusabl	$⊢ (G \in Abel \land S \in SubGrp (G)) \to H \in Abel$

Proof

Step	Hyp	Ref	Expression
1		qusabl.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
2		ablnsg	$⊢ G \in Abel \to NrmSGrp (G) = SubGrp (G)$
3	2	eleq2d	$⊢ G \in Abel \to (S \in NrmSGrp (G) \leftrightarrow S \in SubGrp (G))$
4	3	biimpar	$⊢ (G \in Abel \land S \in SubGrp (G)) \to S \in NrmSGrp (G)$
5	1	qusgrp	$⊢ S \in NrmSGrp (G) \to H \in Grp$
6	4 5	syl	$⊢ (G \in Abel \land S \in SubGrp (G)) \to H \in Grp$
7		vex	$⊢ x \in V$
8	7	elqs	$⊢ x \in ({Base}_{G} / (G ~_{QG} S)) \leftrightarrow \exists a \in {Base}_{G} x = [a] (G ~_{QG} S)$
9	1	a1i	$⊢ (G \in Abel \land S \in SubGrp (G)) \to H = G /_{𝑠} (G ~_{QG} S)$
10		eqidd	$⊢ (G \in Abel \land S \in SubGrp (G)) \to {Base}_{G} = {Base}_{G}$
11		ovexd	$⊢ (G \in Abel \land S \in SubGrp (G)) \to G ~_{QG} S \in V$
12		simpl	$⊢ (G \in Abel \land S \in SubGrp (G)) \to G \in Abel$
13	9 10 11 12	qusbas	$⊢ (G \in Abel \land S \in SubGrp (G)) \to {Base}_{G} / (G ~_{QG} S) = {Base}_{H}$
14	13	eleq2d	$⊢ (G \in Abel \land S \in SubGrp (G)) \to (x \in ({Base}_{G} / (G ~_{QG} S)) \leftrightarrow x \in {Base}_{H})$
15	8 14	bitr3id	$⊢ (G \in Abel \land S \in SubGrp (G)) \to (\exists a \in {Base}_{G} x = [a] (G ~_{QG} S) \leftrightarrow x \in {Base}_{H})$
16		vex	$⊢ y \in V$
17	16	elqs	$⊢ y \in ({Base}_{G} / (G ~_{QG} S)) \leftrightarrow \exists b \in {Base}_{G} y = [b] (G ~_{QG} S)$
18	13	eleq2d	$⊢ (G \in Abel \land S \in SubGrp (G)) \to (y \in ({Base}_{G} / (G ~_{QG} S)) \leftrightarrow y \in {Base}_{H})$
19	17 18	bitr3id	$⊢ (G \in Abel \land S \in SubGrp (G)) \to (\exists b \in {Base}_{G} y = [b] (G ~_{QG} S) \leftrightarrow y \in {Base}_{H})$
20	15 19	anbi12d	$⊢ (G \in Abel \land S \in SubGrp (G)) \to ((\exists a \in {Base}_{G} x = [a] (G ~_{QG} S) \land \exists b \in {Base}_{G} y = [b] (G ~_{QG} S)) \leftrightarrow (x \in {Base}_{H} \land y \in {Base}_{H}))$
21		reeanv	$⊢ \exists a \in {Base}_{G} \exists b \in {Base}_{G} (x = [a] (G ~_{QG} S) \land y = [b] (G ~_{QG} S)) \leftrightarrow (\exists a \in {Base}_{G} x = [a] (G ~_{QG} S) \land \exists b \in {Base}_{G} y = [b] (G ~_{QG} S))$
22		eqid	$⊢ {Base}_{G} = {Base}_{G}$
23		eqid	$⊢ +_{G} = +_{G}$
24	22 23	ablcom	$⊢ (G \in Abel \land a \in {Base}_{G} \land b \in {Base}_{G}) \to a +_{G} b = b +_{G} a$
25	24	3expb	$⊢ (G \in Abel \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to a +_{G} b = b +_{G} a$
26	25	adantlr	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to a +_{G} b = b +_{G} a$
27	26	eceq1d	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to [(a +_{G} b)] (G ~_{QG} S) = [(b +_{G} a)] (G ~_{QG} S)$
28	4	adantr	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to S \in NrmSGrp (G)$
29		simprl	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to a \in {Base}_{G}$
30		simprr	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to b \in {Base}_{G}$
31		eqid	$⊢ +_{H} = +_{H}$
32	1 22 23 31	qusadd	$⊢ (S \in NrmSGrp (G) \land a \in {Base}_{G} \land b \in {Base}_{G}) \to [a] (G ~_{QG} S) +_{H} [b] (G ~_{QG} S) = [(a +_{G} b)] (G ~_{QG} S)$
33	28 29 30 32	syl3anc	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to [a] (G ~_{QG} S) +_{H} [b] (G ~_{QG} S) = [(a +_{G} b)] (G ~_{QG} S)$
34	1 22 23 31	qusadd	$⊢ (S \in NrmSGrp (G) \land b \in {Base}_{G} \land a \in {Base}_{G}) \to [b] (G ~_{QG} S) +_{H} [a] (G ~_{QG} S) = [(b +_{G} a)] (G ~_{QG} S)$
35	28 30 29 34	syl3anc	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to [b] (G ~_{QG} S) +_{H} [a] (G ~_{QG} S) = [(b +_{G} a)] (G ~_{QG} S)$
36	27 33 35	3eqtr4d	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to [a] (G ~_{QG} S) +_{H} [b] (G ~_{QG} S) = [b] (G ~_{QG} S) +_{H} [a] (G ~_{QG} S)$
37		oveq12	$⊢ (x = [a] (G ~_{QG} S) \land y = [b] (G ~_{QG} S)) \to x +_{H} y = [a] (G ~_{QG} S) +_{H} [b] (G ~_{QG} S)$
38		oveq12	$⊢ (y = [b] (G ~_{QG} S) \land x = [a] (G ~_{QG} S)) \to y +_{H} x = [b] (G ~_{QG} S) +_{H} [a] (G ~_{QG} S)$
39	38	ancoms	$⊢ (x = [a] (G ~_{QG} S) \land y = [b] (G ~_{QG} S)) \to y +_{H} x = [b] (G ~_{QG} S) +_{H} [a] (G ~_{QG} S)$
40	37 39	eqeq12d	$⊢ (x = [a] (G ~_{QG} S) \land y = [b] (G ~_{QG} S)) \to (x +_{H} y = y +_{H} x \leftrightarrow [a] (G ~_{QG} S) +_{H} [b] (G ~_{QG} S) = [b] (G ~_{QG} S) +_{H} [a] (G ~_{QG} S))$
41	36 40	syl5ibrcom	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land (a \in {Base}_{G} \land b \in {Base}_{G})) \to ((x = [a] (G ~_{QG} S) \land y = [b] (G ~_{QG} S)) \to x +_{H} y = y +_{H} x)$
42	41	rexlimdvva	$⊢ (G \in Abel \land S \in SubGrp (G)) \to (\exists a \in {Base}_{G} \exists b \in {Base}_{G} (x = [a] (G ~_{QG} S) \land y = [b] (G ~_{QG} S)) \to x +_{H} y = y +_{H} x)$
43	21 42	syl5bir	$⊢ (G \in Abel \land S \in SubGrp (G)) \to ((\exists a \in {Base}_{G} x = [a] (G ~_{QG} S) \land \exists b \in {Base}_{G} y = [b] (G ~_{QG} S)) \to x +_{H} y = y +_{H} x)$
44	20 43	sylbird	$⊢ (G \in Abel \land S \in SubGrp (G)) \to ((x \in {Base}_{H} \land y \in {Base}_{H}) \to x +_{H} y = y +_{H} x)$
45	44	ralrimivv	$⊢ (G \in Abel \land S \in SubGrp (G)) \to \forall x \in {Base}_{H} \forall y \in {Base}_{H} x +_{H} y = y +_{H} x$
46		eqid	$⊢ {Base}_{H} = {Base}_{H}$
47	46 31	isabl2	$⊢ H \in Abel \leftrightarrow (H \in Grp \land \forall x \in {Base}_{H} \forall y \in {Base}_{H} x +_{H} y = y +_{H} x)$
48	6 45 47	sylanbrc	$⊢ (G \in Abel \land S \in SubGrp (G)) \to H \in Abel$

Metamath Proof Explorer

Theorem qusabl

Proof