ghmquskerlem1

	Ref	Expression
Hypotheses	ghmqusker.1	$⊢ \underset{˙}{0} = 0_{H}$
	ghmqusker.f	$⊢ φ \to F \in (G GrpHom H)$
	ghmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
	ghmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
	ghmqusker.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
	ghmquskerlem1.x	$⊢ φ \to X \in {Base}_{G}$
Assertion	ghmquskerlem1	$⊢ φ \to J ([X] (G ~_{QG} K)) = F (X)$

Proof

Step	Hyp	Ref	Expression
1		ghmqusker.1	$⊢ \underset{˙}{0} = 0_{H}$
2		ghmqusker.f	$⊢ φ \to F \in (G GrpHom H)$
3		ghmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
4		ghmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
5		ghmqusker.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
6		ghmquskerlem1.x	$⊢ φ \to X \in {Base}_{G}$
7		imaeq2	$⊢ q = [X] (G ~_{QG} K) \to F [q] = F [[X] (G ~_{QG} K)]$
8	7	unieqd	$⊢ q = [X] (G ~_{QG} K) \to ⋃ F [q] = ⋃ F [[X] (G ~_{QG} K)]$
9		ovex	$⊢ G ~_{QG} K \in V$
10	9	ecelqsi	$⊢ X \in {Base}_{G} \to [X] (G ~_{QG} K) \in ({Base}_{G} / (G ~_{QG} K))$
11	6 10	syl	$⊢ φ \to [X] (G ~_{QG} K) \in ({Base}_{G} / (G ~_{QG} K))$
12	4	a1i	$⊢ φ \to Q = G /_{𝑠} (G ~_{QG} K)$
13		eqidd	$⊢ φ \to {Base}_{G} = {Base}_{G}$
14		ovexd	$⊢ φ \to G ~_{QG} K \in V$
15		ghmgrp1	$⊢ F \in (G GrpHom H) \to G \in Grp$
16	2 15	syl	$⊢ φ \to G \in Grp$
17	12 13 14 16	qusbas	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
18	11 17	eleqtrd	$⊢ φ \to [X] (G ~_{QG} K) \in {Base}_{Q}$
19	2	imaexd	$⊢ φ \to F [[X] (G ~_{QG} K)] \in V$
20	19	uniexd	$⊢ φ \to ⋃ F [[X] (G ~_{QG} K)] \in V$
21	5 8 18 20	fvmptd3	$⊢ φ \to J ([X] (G ~_{QG} K)) = ⋃ F [[X] (G ~_{QG} K)]$
22		eqid	$⊢ {Base}_{G} = {Base}_{G}$
23		eqid	$⊢ {Base}_{H} = {Base}_{H}$
24	22 23	ghmf	$⊢ F \in (G GrpHom H) \to F : {Base}_{G} ⟶ {Base}_{H}$
25	2 24	syl	$⊢ φ \to F : {Base}_{G} ⟶ {Base}_{H}$
26	25	ffnd	$⊢ φ \to F Fn {Base}_{G}$
27	1	ghmker	$⊢ F \in (G GrpHom H) \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
28	2 27	syl	$⊢ φ \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
29	3 28	eqeltrid	$⊢ φ \to K \in NrmSGrp (G)$
30		nsgsubg	$⊢ K \in NrmSGrp (G) \to K \in SubGrp (G)$
31		eqid	$⊢ G ~_{QG} K = G ~_{QG} K$
32	22 31	eqger	$⊢ K \in SubGrp (G) \to (G ~_{QG} K) Er {Base}_{G}$
33	29 30 32	3syl	$⊢ φ \to (G ~_{QG} K) Er {Base}_{G}$
34	33	ecss	$⊢ φ \to [X] (G ~_{QG} K) \subseteq {Base}_{G}$
35	26 34	fvelimabd	$⊢ φ \to (y \in F [[X] (G ~_{QG} K)] \leftrightarrow \exists z \in [X] (G ~_{QG} K) F (z) = y)$
36		simpr	$⊢ ((φ \land z \in [X] (G ~_{QG} K)) \land F (z) = y) \to F (z) = y$
37	2	adantr	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F \in (G GrpHom H)$
38		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
39	37 15	syl	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to G \in Grp$
40	6	adantr	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to X \in {Base}_{G}$
41	22 38 39 40	grpinvcld	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to {inv}_{g} (G) (X) \in {Base}_{G}$
42	34	sselda	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to z \in {Base}_{G}$
43		eqid	$⊢ +_{G} = +_{G}$
44		eqid	$⊢ +_{H} = +_{H}$
45	22 43 44	ghmlin	$⊢ (F \in (G GrpHom H) \land {inv}_{g} (G) (X) \in {Base}_{G} \land z \in {Base}_{G}) \to F ({inv}_{g} (G) (X) +_{G} z) = F ({inv}_{g} (G) (X)) +_{H} F (z)$
46	37 41 42 45	syl3anc	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F ({inv}_{g} (G) (X) +_{G} z) = F ({inv}_{g} (G) (X)) +_{H} F (z)$
47	26	adantr	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F Fn {Base}_{G}$
48	22	subgss	$⊢ K \in SubGrp (G) \to K \subseteq {Base}_{G}$
49	29 30 48	3syl	$⊢ φ \to K \subseteq {Base}_{G}$
50	49	adantr	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to K \subseteq {Base}_{G}$
51		vex	$⊢ z \in V$
52		elecg	$⊢ (z \in V \land X \in {Base}_{G}) \to (z \in [X] (G ~_{QG} K) \leftrightarrow X (G ~_{QG} K) z)$
53	51 52	mpan	$⊢ X \in {Base}_{G} \to (z \in [X] (G ~_{QG} K) \leftrightarrow X (G ~_{QG} K) z)$
54	53	biimpa	$⊢ (X \in {Base}_{G} \land z \in [X] (G ~_{QG} K)) \to X (G ~_{QG} K) z$
55	6 54	sylan	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to X (G ~_{QG} K) z$
56	22 38 43 31	eqgval	$⊢ (G \in Grp \land K \subseteq {Base}_{G}) \to (X (G ~_{QG} K) z \leftrightarrow (X \in {Base}_{G} \land z \in {Base}_{G} \land {inv}_{g} (G) (X) +_{G} z \in K))$
57	56	biimpa	$⊢ ((G \in Grp \land K \subseteq {Base}_{G}) \land X (G ~_{QG} K) z) \to (X \in {Base}_{G} \land z \in {Base}_{G} \land {inv}_{g} (G) (X) +_{G} z \in K)$
58	57	simp3d	$⊢ ((G \in Grp \land K \subseteq {Base}_{G}) \land X (G ~_{QG} K) z) \to {inv}_{g} (G) (X) +_{G} z \in K$
59	39 50 55 58	syl21anc	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to {inv}_{g} (G) (X) +_{G} z \in K$
60	59 3	eleqtrdi	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to {inv}_{g} (G) (X) +_{G} z \in F^{-1} [\{\underset{˙}{0}\}]$
61		fniniseg	$⊢ F Fn {Base}_{G} \to ({inv}_{g} (G) (X) +_{G} z \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow ({inv}_{g} (G) (X) +_{G} z \in {Base}_{G} \land F ({inv}_{g} (G) (X) +_{G} z) = \underset{˙}{0}))$
62	61	biimpa	$⊢ (F Fn {Base}_{G} \land {inv}_{g} (G) (X) +_{G} z \in F^{-1} [\{\underset{˙}{0}\}]) \to ({inv}_{g} (G) (X) +_{G} z \in {Base}_{G} \land F ({inv}_{g} (G) (X) +_{G} z) = \underset{˙}{0})$
63	47 60 62	syl2anc	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to ({inv}_{g} (G) (X) +_{G} z \in {Base}_{G} \land F ({inv}_{g} (G) (X) +_{G} z) = \underset{˙}{0})$
64	63	simprd	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F ({inv}_{g} (G) (X) +_{G} z) = \underset{˙}{0}$
65	46 64	eqtr3d	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F ({inv}_{g} (G) (X)) +_{H} F (z) = \underset{˙}{0}$
66	65	oveq2d	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F (X) +_{H} (F ({inv}_{g} (G) (X)) +_{H} F (z)) = F (X) +_{H} \underset{˙}{0}$
67		eqid	$⊢ {inv}_{g} (H) = {inv}_{g} (H)$
68	22 38 67	ghminv	$⊢ (F \in (G GrpHom H) \land X \in {Base}_{G}) \to F ({inv}_{g} (G) (X)) = {inv}_{g} (H) (F (X))$
69	37 40 68	syl2anc	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F ({inv}_{g} (G) (X)) = {inv}_{g} (H) (F (X))$
70	69	oveq1d	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F ({inv}_{g} (G) (X)) +_{H} F (z) = {inv}_{g} (H) (F (X)) +_{H} F (z)$
71	70	oveq2d	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F (X) +_{H} (F ({inv}_{g} (G) (X)) +_{H} F (z)) = F (X) +_{H} ({inv}_{g} (H) (F (X)) +_{H} F (z))$
72		ghmgrp2	$⊢ F \in (G GrpHom H) \to H \in Grp$
73	37 72	syl	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to H \in Grp$
74	37 24	syl	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F : {Base}_{G} ⟶ {Base}_{H}$
75	74 40	ffvelcdmd	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F (X) \in {Base}_{H}$
76	74 42	ffvelcdmd	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F (z) \in {Base}_{H}$
77	23 44 67	grpasscan1	$⊢ (H \in Grp \land F (X) \in {Base}_{H} \land F (z) \in {Base}_{H}) \to F (X) +_{H} ({inv}_{g} (H) (F (X)) +_{H} F (z)) = F (z)$
78	73 75 76 77	syl3anc	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F (X) +_{H} ({inv}_{g} (H) (F (X)) +_{H} F (z)) = F (z)$
79	71 78	eqtrd	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F (X) +_{H} (F ({inv}_{g} (G) (X)) +_{H} F (z)) = F (z)$
80	23 44 1	grprid	$⊢ (H \in Grp \land F (X) \in {Base}_{H}) \to F (X) +_{H} \underset{˙}{0} = F (X)$
81	73 75 80	syl2anc	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F (X) +_{H} \underset{˙}{0} = F (X)$
82	66 79 81	3eqtr3d	$⊢ (φ \land z \in [X] (G ~_{QG} K)) \to F (z) = F (X)$
83	82	adantr	$⊢ ((φ \land z \in [X] (G ~_{QG} K)) \land F (z) = y) \to F (z) = F (X)$
84	36 83	eqtr3d	$⊢ ((φ \land z \in [X] (G ~_{QG} K)) \land F (z) = y) \to y = F (X)$
85	84	r19.29an	$⊢ (φ \land \exists z \in [X] (G ~_{QG} K) F (z) = y) \to y = F (X)$
86		ecref	$⊢ ((G ~_{QG} K) Er {Base}_{G} \land X \in {Base}_{G}) \to X \in [X] (G ~_{QG} K)$
87	33 6 86	syl2anc	$⊢ φ \to X \in [X] (G ~_{QG} K)$
88	87	adantr	$⊢ (φ \land y = F (X)) \to X \in [X] (G ~_{QG} K)$
89		fveqeq2	$⊢ z = X \to (F (z) = y \leftrightarrow F (X) = y)$
90	89	adantl	$⊢ ((φ \land y = F (X)) \land z = X) \to (F (z) = y \leftrightarrow F (X) = y)$
91		simpr	$⊢ (φ \land y = F (X)) \to y = F (X)$
92	91	eqcomd	$⊢ (φ \land y = F (X)) \to F (X) = y$
93	88 90 92	rspcedvd	$⊢ (φ \land y = F (X)) \to \exists z \in [X] (G ~_{QG} K) F (z) = y$
94	85 93	impbida	$⊢ φ \to (\exists z \in [X] (G ~_{QG} K) F (z) = y \leftrightarrow y = F (X))$
95		velsn	$⊢ y \in \{F (X)\} \leftrightarrow y = F (X)$
96	94 95	bitr4di	$⊢ φ \to (\exists z \in [X] (G ~_{QG} K) F (z) = y \leftrightarrow y \in \{F (X)\})$
97	35 96	bitrd	$⊢ φ \to (y \in F [[X] (G ~_{QG} K)] \leftrightarrow y \in \{F (X)\})$
98	97	eqrdv	$⊢ φ \to F [[X] (G ~_{QG} K)] = \{F (X)\}$
99	98	unieqd	$⊢ φ \to ⋃ F [[X] (G ~_{QG} K)] = ⋃ \{F (X)\}$
100		fvex	$⊢ F (X) \in V$
101	100	unisn	$⊢ ⋃ \{F (X)\} = F (X)$
102	99 101	eqtrdi	$⊢ φ \to ⋃ F [[X] (G ~_{QG} K)] = F (X)$
103	21 102	eqtrd	$⊢ φ \to J ([X] (G ~_{QG} K)) = F (X)$

Metamath Proof Explorer

Theorem ghmquskerlem1

Proof