qusinv

Description: Value of the group inverse operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	qusgrp.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
	qusinv.v	$⊢ V = {Base}_{G}$
	qusinv.i	$⊢ I = {inv}_{g} (G)$
	qusinv.n	$⊢ N = {inv}_{g} (H)$
Assertion	qusinv	$⊢ (S \in NrmSGrp (G) \land X \in V) \to N ([X] (G ~_{QG} S)) = [I (X)] (G ~_{QG} S)$

Proof

Step	Hyp	Ref	Expression
1		qusgrp.h	$⊢ H = G /_{𝑠} (G ~_{QG} S)$
2		qusinv.v	$⊢ V = {Base}_{G}$
3		qusinv.i	$⊢ I = {inv}_{g} (G)$
4		qusinv.n	$⊢ N = {inv}_{g} (H)$
5		nsgsubg	$⊢ S \in NrmSGrp (G) \to S \in SubGrp (G)$
6		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
7	5 6	syl	$⊢ S \in NrmSGrp (G) \to G \in Grp$
8	2 3	grpinvcl	$⊢ (G \in Grp \land X \in V) \to I (X) \in V$
9	7 8	sylan	$⊢ (S \in NrmSGrp (G) \land X \in V) \to I (X) \in V$
10		eqid	$⊢ +_{G} = +_{G}$
11		eqid	$⊢ +_{H} = +_{H}$
12	1 2 10 11	qusadd	$⊢ (S \in NrmSGrp (G) \land X \in V \land I (X) \in V) \to [X] (G ~_{QG} S) +_{H} [I (X)] (G ~_{QG} S) = [(X +_{G} I (X))] (G ~_{QG} S)$
13	9 12	mpd3an3	$⊢ (S \in NrmSGrp (G) \land X \in V) \to [X] (G ~_{QG} S) +_{H} [I (X)] (G ~_{QG} S) = [(X +_{G} I (X))] (G ~_{QG} S)$
14		eqid	$⊢ 0_{G} = 0_{G}$
15	2 10 14 3	grprinv	$⊢ (G \in Grp \land X \in V) \to X +_{G} I (X) = 0_{G}$
16	7 15	sylan	$⊢ (S \in NrmSGrp (G) \land X \in V) \to X +_{G} I (X) = 0_{G}$
17	16	eceq1d	$⊢ (S \in NrmSGrp (G) \land X \in V) \to [(X +_{G} I (X))] (G ~_{QG} S) = [0_{G}] (G ~_{QG} S)$
18	1 14	qus0	$⊢ S \in NrmSGrp (G) \to [0_{G}] (G ~_{QG} S) = 0_{H}$
19	18	adantr	$⊢ (S \in NrmSGrp (G) \land X \in V) \to [0_{G}] (G ~_{QG} S) = 0_{H}$
20	13 17 19	3eqtrd	$⊢ (S \in NrmSGrp (G) \land X \in V) \to [X] (G ~_{QG} S) +_{H} [I (X)] (G ~_{QG} S) = 0_{H}$
21	1	qusgrp	$⊢ S \in NrmSGrp (G) \to H \in Grp$
22	21	adantr	$⊢ (S \in NrmSGrp (G) \land X \in V) \to H \in Grp$
23		eqid	$⊢ {Base}_{H} = {Base}_{H}$
24	1 2 23	quseccl	$⊢ (S \in NrmSGrp (G) \land X \in V) \to [X] (G ~_{QG} S) \in {Base}_{H}$
25	1 2 23	quseccl	$⊢ (S \in NrmSGrp (G) \land I (X) \in V) \to [I (X)] (G ~_{QG} S) \in {Base}_{H}$
26	9 25	syldan	$⊢ (S \in NrmSGrp (G) \land X \in V) \to [I (X)] (G ~_{QG} S) \in {Base}_{H}$
27		eqid	$⊢ 0_{H} = 0_{H}$
28	23 11 27 4	grpinvid1	$⊢ (H \in Grp \land [X] (G ~_{QG} S) \in {Base}_{H} \land [I (X)] (G ~_{QG} S) \in {Base}_{H}) \to (N ([X] (G ~_{QG} S)) = [I (X)] (G ~_{QG} S) \leftrightarrow [X] (G ~_{QG} S) +_{H} [I (X)] (G ~_{QG} S) = 0_{H})$
29	22 24 26 28	syl3anc	$⊢ (S \in NrmSGrp (G) \land X \in V) \to (N ([X] (G ~_{QG} S)) = [I (X)] (G ~_{QG} S) \leftrightarrow [X] (G ~_{QG} S) +_{H} [I (X)] (G ~_{QG} S) = 0_{H})$
30	20 29	mpbird	$⊢ (S \in NrmSGrp (G) \land X \in V) \to N ([X] (G ~_{QG} S)) = [I (X)] (G ~_{QG} S)$

Metamath Proof Explorer

Theorem qusinv

Proof