nsgmgc

Description: There is a monotone Galois connection between the lattice of subgroups of a group G containing a normal subgroup N and the lattice of subgroups of the quotient group G / N . This is sometimes called the lattice theorem. (Contributed by Thierry Arnoux, 27-Jul-2024)

	Ref	Expression
Hypotheses	nsgmgc.b	$⊢ B = {Base}_{G}$
	nsgmgc.s	$⊢ S = \{h \in SubGrp (G) \| N \subseteq h\}$
	nsgmgc.t	$⊢ T = SubGrp (Q)$
	nsgmgc.j	No typesetting found for \|- J = ( V MGalConn W ) with typecode \|-
	nsgmgc.v	$⊢ V = toInc (S)$
	nsgmgc.w	$⊢ W = toInc (T)$
	nsgmgc.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
	nsgmgc.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	nsgmgc.e	$⊢ E = (h \in S ⟼ ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
	nsgmgc.f	$⊢ F = (f \in T ⟼ \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
	nsgmgc.n	$⊢ φ \to N \in NrmSGrp (G)$
Assertion	nsgmgc	$⊢ φ \to E J F$

Proof

Step	Hyp	Ref	Expression
1		nsgmgc.b	$⊢ B = {Base}_{G}$
2		nsgmgc.s	$⊢ S = \{h \in SubGrp (G) \| N \subseteq h\}$
3		nsgmgc.t	$⊢ T = SubGrp (Q)$
4		nsgmgc.j	Could not format J = ( V MGalConn W ) : No typesetting found for \|- J = ( V MGalConn W ) with typecode \|-
5		nsgmgc.v	$⊢ V = toInc (S)$
6		nsgmgc.w	$⊢ W = toInc (T)$
7		nsgmgc.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
8		nsgmgc.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
9		nsgmgc.e	$⊢ E = (h \in S ⟼ ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
10		nsgmgc.f	$⊢ F = (f \in T ⟼ \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
11		nsgmgc.n	$⊢ φ \to N \in NrmSGrp (G)$
12		nfv	$⊢ Ⅎ h φ$
13		vex	$⊢ h \in V$
14	13	mptex	$⊢ (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in V$
15	14	rnex	$⊢ ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in V$
16	15	a1i	$⊢ (φ \land h \in S) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in V$
17	12 16 9	fnmptd	$⊢ φ \to E Fn S$
18		mpteq1	$⊢ h = k \to (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) = (x \in k ⟼ \{x\} \underset{˙}{\oplus} N)$
19	18	rneqd	$⊢ h = k \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) = ran (x \in k ⟼ \{x\} \underset{˙}{\oplus} N)$
20	19	cbvmptv	$⊢ (h \in S ⟼ ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) = (k \in S ⟼ ran (x \in k ⟼ \{x\} \underset{˙}{\oplus} N))$
21	9 20	eqtri	$⊢ E = (k \in S ⟼ ran (x \in k ⟼ \{x\} \underset{˙}{\oplus} N))$
22		eqid	$⊢ (x \in B ⟼ [x] (G ~_{QG} N)) = (x \in B ⟼ [x] (G ~_{QG} N))$
23	11	adantr	$⊢ (φ \land h \in S) \to N \in NrmSGrp (G)$
24		simpr	$⊢ (φ \land h \in S) \to h \in S$
25	2	ssrab3	$⊢ S \subseteq SubGrp (G)$
26	25	a1i	$⊢ (φ \land h \in S) \to S \subseteq SubGrp (G)$
27	1 7 8 21 22 23 24 26	qusima	$⊢ (φ \land h \in S) \to E (h) = (x \in B ⟼ [x] (G ~_{QG} N)) [h]$
28	1 7 22	qusghm	$⊢ N \in NrmSGrp (G) \to (x \in B ⟼ [x] (G ~_{QG} N)) \in (G GrpHom Q)$
29	23 28	syl	$⊢ (φ \land h \in S) \to (x \in B ⟼ [x] (G ~_{QG} N)) \in (G GrpHom Q)$
30	25	a1i	$⊢ φ \to S \subseteq SubGrp (G)$
31	30	sselda	$⊢ (φ \land h \in S) \to h \in SubGrp (G)$
32		ghmima	$⊢ ((x \in B ⟼ [x] (G ~_{QG} N)) \in (G GrpHom Q) \land h \in SubGrp (G)) \to (x \in B ⟼ [x] (G ~_{QG} N)) [h] \in SubGrp (Q)$
33	29 31 32	syl2anc	$⊢ (φ \land h \in S) \to (x \in B ⟼ [x] (G ~_{QG} N)) [h] \in SubGrp (Q)$
34	27 33	eqeltrd	$⊢ (φ \land h \in S) \to E (h) \in SubGrp (Q)$
35	34 3	eleqtrrdi	$⊢ (φ \land h \in S) \to E (h) \in T$
36	35	ralrimiva	$⊢ φ \to \forall h \in S E (h) \in T$
37		ffnfv	$⊢ E : S ⟶ T \leftrightarrow (E Fn S \land \forall h \in S E (h) \in T)$
38	17 36 37	sylanbrc	$⊢ φ \to E : S ⟶ T$
39		sseq2	$⊢ h = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \to (N \subseteq h \leftrightarrow N \subseteq \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
40	11	adantr	$⊢ (φ \land f \in T) \to N \in NrmSGrp (G)$
41		simpr	$⊢ (φ \land f \in T) \to f \in T$
42	41 3	eleqtrdi	$⊢ (φ \land f \in T) \to f \in SubGrp (Q)$
43	1 7 8 40 42	nsgmgclem	$⊢ (φ \land f \in T) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in SubGrp (G)$
44		nsgsubg	$⊢ N \in NrmSGrp (G) \to N \in SubGrp (G)$
45	11 44	syl	$⊢ φ \to N \in SubGrp (G)$
46	1	subgss	$⊢ N \in SubGrp (G) \to N \subseteq B$
47	45 46	syl	$⊢ φ \to N \subseteq B$
48	47	adantr	$⊢ (φ \land f \in T) \to N \subseteq B$
49	45	ad2antrr	$⊢ ((φ \land f \in T) \land a \in N) \to N \in SubGrp (G)$
50		simpr	$⊢ ((φ \land f \in T) \land a \in N) \to a \in N$
51	8	grplsmid	$⊢ (N \in SubGrp (G) \land a \in N) \to \{a\} \underset{˙}{\oplus} N = N$
52	49 50 51	syl2anc	$⊢ ((φ \land f \in T) \land a \in N) \to \{a\} \underset{˙}{\oplus} N = N$
53	11	ad2antrr	$⊢ ((φ \land f \in T) \land a \in N) \to N \in NrmSGrp (G)$
54	42	adantr	$⊢ ((φ \land f \in T) \land a \in N) \to f \in SubGrp (Q)$
55	7	nsgqus0	$⊢ (N \in NrmSGrp (G) \land f \in SubGrp (Q)) \to N \in f$
56	53 54 55	syl2anc	$⊢ ((φ \land f \in T) \land a \in N) \to N \in f$
57	52 56	eqeltrd	$⊢ ((φ \land f \in T) \land a \in N) \to \{a\} \underset{˙}{\oplus} N \in f$
58	48 57	ssrabdv	$⊢ (φ \land f \in T) \to N \subseteq \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
59	39 43 58	elrabd	$⊢ (φ \land f \in T) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in \{h \in SubGrp (G) \| N \subseteq h\}$
60	59 2	eleqtrrdi	$⊢ (φ \land f \in T) \to \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in S$
61	60 10	fmptd	$⊢ φ \to F : T ⟶ S$
62	38 61	jca	$⊢ φ \to (E : S ⟶ T \land F : T ⟶ S)$
63	1	subgss	$⊢ h \in SubGrp (G) \to h \subseteq B$
64	31 63	syl	$⊢ (φ \land h \in S) \to h \subseteq B$
65	64	ad2antrr	$⊢ (((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \to h \subseteq B$
66	9	fvmpt2	$⊢ (h \in S \land ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in V) \to E (h) = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
67	24 15 66	sylancl	$⊢ (φ \land h \in S) \to E (h) = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
68	67	ad5ant12	$⊢ ((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \to E (h) = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
69		simplr	$⊢ ((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \to E (h) \subseteq f$
70	68 69	eqsstrrd	$⊢ ((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \subseteq f$
71		eqid	$⊢ (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) = (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
72		simpr	$⊢ ((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \to a \in h$
73		sneq	$⊢ x = a \to \{x\} = \{a\}$
74	73	oveq1d	$⊢ x = a \to \{x\} \underset{˙}{\oplus} N = \{a\} \underset{˙}{\oplus} N$
75	74	eqeq2d	$⊢ x = a \to (\{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N \leftrightarrow \{a\} \underset{˙}{\oplus} N = \{a\} \underset{˙}{\oplus} N)$
76	75	adantl	$⊢ (((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \land x = a) \to (\{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N \leftrightarrow \{a\} \underset{˙}{\oplus} N = \{a\} \underset{˙}{\oplus} N)$
77		eqidd	$⊢ ((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \to \{a\} \underset{˙}{\oplus} N = \{a\} \underset{˙}{\oplus} N$
78	72 76 77	rspcedvd	$⊢ ((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \to \exists x \in h \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N$
79		ovexd	$⊢ ((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \to \{a\} \underset{˙}{\oplus} N \in V$
80	71 78 79	elrnmptd	$⊢ ((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \to \{a\} \underset{˙}{\oplus} N \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
81	70 80	sseldd	$⊢ ((((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \land a \in h) \to \{a\} \underset{˙}{\oplus} N \in f$
82	65 81	ssrabdv	$⊢ (((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \to h \subseteq \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
83		simpr	$⊢ ((φ \land h \in S) \land f \in T) \to f \in T$
84	1	fvexi	$⊢ B \in V$
85	84	rabex	$⊢ \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in V$
86	10	fvmpt2	$⊢ (f \in T \land \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \in V) \to F (f) = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
87	83 85 86	sylancl	$⊢ ((φ \land h \in S) \land f \in T) \to F (f) = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
88	87	adantr	$⊢ (((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \to F (f) = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
89	82 88	sseqtrrd	$⊢ (((φ \land h \in S) \land f \in T) \land E (h) \subseteq f) \to h \subseteq F (f)$
90	67	ad2antrr	$⊢ (((φ \land h \in S) \land f \in T) \land h \subseteq F (f)) \to E (h) = ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
91		simpr	$⊢ (((φ \land h \in S) \land f \in T) \land h \subseteq F (f)) \to h \subseteq F (f)$
92	91	sselda	$⊢ ((((φ \land h \in S) \land f \in T) \land h \subseteq F (f)) \land x \in h) \to x \in F (f)$
93	87	ad2antrr	$⊢ ((((φ \land h \in S) \land f \in T) \land h \subseteq F (f)) \land x \in h) \to F (f) = \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
94	92 93	eleqtrd	$⊢ ((((φ \land h \in S) \land f \in T) \land h \subseteq F (f)) \land x \in h) \to x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\}$
95		sneq	$⊢ a = x \to \{a\} = \{x\}$
96	95	oveq1d	$⊢ a = x \to \{a\} \underset{˙}{\oplus} N = \{x\} \underset{˙}{\oplus} N$
97	96	eleq1d	$⊢ a = x \to (\{a\} \underset{˙}{\oplus} N \in f \leftrightarrow \{x\} \underset{˙}{\oplus} N \in f)$
98	97	elrab	$⊢ x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \leftrightarrow (x \in B \land \{x\} \underset{˙}{\oplus} N \in f)$
99	98	simprbi	$⊢ x \in \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\} \to \{x\} \underset{˙}{\oplus} N \in f$
100	94 99	syl	$⊢ ((((φ \land h \in S) \land f \in T) \land h \subseteq F (f)) \land x \in h) \to \{x\} \underset{˙}{\oplus} N \in f$
101	100	ralrimiva	$⊢ (((φ \land h \in S) \land f \in T) \land h \subseteq F (f)) \to \forall x \in h \{x\} \underset{˙}{\oplus} N \in f$
102	71	rnmptss	$⊢ \forall x \in h \{x\} \underset{˙}{\oplus} N \in f \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \subseteq f$
103	101 102	syl	$⊢ (((φ \land h \in S) \land f \in T) \land h \subseteq F (f)) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \subseteq f$
104	90 103	eqsstrd	$⊢ (((φ \land h \in S) \land f \in T) \land h \subseteq F (f)) \to E (h) \subseteq f$
105	89 104	impbida	$⊢ ((φ \land h \in S) \land f \in T) \to (E (h) \subseteq f \leftrightarrow h \subseteq F (f))$
106	3	fvexi	$⊢ T \in V$
107		eqid	$⊢ \leq_{W} = \leq_{W}$
108	6 107	ipole	$⊢ (T \in V \land E (h) \in T \land f \in T) \to (E (h) \leq_{W} f \leftrightarrow E (h) \subseteq f)$
109	106 35 83 108	mp3an2ani	$⊢ ((φ \land h \in S) \land f \in T) \to (E (h) \leq_{W} f \leftrightarrow E (h) \subseteq f)$
110		fvex	$⊢ SubGrp (G) \in V$
111	2 110	rabex2	$⊢ S \in V$
112	61	ffvelrnda	$⊢ (φ \land f \in T) \to F (f) \in S$
113	112	adantlr	$⊢ ((φ \land h \in S) \land f \in T) \to F (f) \in S$
114		eqid	$⊢ \leq_{V} = \leq_{V}$
115	5 114	ipole	$⊢ (S \in V \land h \in S \land F (f) \in S) \to (h \leq_{V} F (f) \leftrightarrow h \subseteq F (f))$
116	111 24 113 115	mp3an2ani	$⊢ ((φ \land h \in S) \land f \in T) \to (h \leq_{V} F (f) \leftrightarrow h \subseteq F (f))$
117	105 109 116	3bitr4d	$⊢ ((φ \land h \in S) \land f \in T) \to (E (h) \leq_{W} f \leftrightarrow h \leq_{V} F (f))$
118	117	anasss	$⊢ (φ \land (h \in S \land f \in T)) \to (E (h) \leq_{W} f \leftrightarrow h \leq_{V} F (f))$
119	118	ralrimivva	$⊢ φ \to \forall h \in S \forall f \in T (E (h) \leq_{W} f \leftrightarrow h \leq_{V} F (f))$
120	5	ipobas	$⊢ S \in V \to S = {Base}_{V}$
121	111 120	ax-mp	$⊢ S = {Base}_{V}$
122	6	ipobas	$⊢ T \in V \to T = {Base}_{W}$
123	106 122	ax-mp	$⊢ T = {Base}_{W}$
124	5	ipopos	$⊢ V \in Poset$
125		posprs	$⊢ V \in Poset \to V \in Proset$
126	124 125	mp1i	$⊢ φ \to V \in Proset$
127	6	ipopos	$⊢ W \in Poset$
128		posprs	$⊢ W \in Poset \to W \in Proset$
129	127 128	mp1i	$⊢ φ \to W \in Proset$
130	121 123 114 107 4 126 129	mgcval	$⊢ φ \to (E J F \leftrightarrow ((E : S ⟶ T \land F : T ⟶ S) \land \forall h \in S \forall f \in T (E (h) \leq_{W} f \leftrightarrow h \leq_{V} F (f))))$
131	62 119 130	mpbir2and	$⊢ φ \to E J F$

Metamath Proof Explorer

Theorem nsgmgc

Proof