lmhmqusker

Description: A surjective module homomorphism F from G to H induces an isomorphism J from Q to H , where Q is the factor group of G by F 's kernel K . (Contributed by Thierry Arnoux, 25-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		lmhmqusker.1	$⊢ \underset{˙}{0} = 0_{H}$
2		lmhmqusker.f	$⊢ φ \to F \in (G LMHom H)$
3		lmhmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
4		lmhmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
5		lmhmqusker.s	$⊢ φ \to ran F = {Base}_{H}$
6		lmhmqusker.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
7		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
8		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
9		eqid	$⊢ \cdot_{H} = \cdot_{H}$
10		eqid	$⊢ Scalar (Q) = Scalar (Q)$
11		eqid	$⊢ Scalar (H) = Scalar (H)$
12		eqid	$⊢ {Base}_{Scalar (Q)} = {Base}_{Scalar (Q)}$
13		eqid	$⊢ {Base}_{G} = {Base}_{G}$
14		lmhmlmod1	$⊢ F \in (G LMHom H) \to G \in LMod$
15	2 14	syl	$⊢ φ \to G \in LMod$
16		eqid	$⊢ LSubSp (G) = LSubSp (G)$
17	3 1 16	lmhmkerlss	$⊢ F \in (G LMHom H) \to K \in LSubSp (G)$
18	2 17	syl	$⊢ φ \to K \in LSubSp (G)$
19	4 13 15 18	quslmod	$⊢ φ \to Q \in LMod$
20		lmhmlmod2	$⊢ F \in (G LMHom H) \to H \in LMod$
21	2 20	syl	$⊢ φ \to H \in LMod$
22		eqid	$⊢ Scalar (G) = Scalar (G)$
23	22 11	lmhmsca	$⊢ F \in (G LMHom H) \to Scalar (H) = Scalar (G)$
24	2 23	syl	$⊢ φ \to Scalar (H) = Scalar (G)$
25	4	a1i	$⊢ φ \to Q = G /_{𝑠} (G ~_{QG} K)$
26	13	a1i	$⊢ φ \to {Base}_{G} = {Base}_{G}$
27		ovexd	$⊢ φ \to G ~_{QG} K \in V$
28	25 26 27 15 22	quss	$⊢ φ \to Scalar (G) = Scalar (Q)$
29	24 28	eqtrd	$⊢ φ \to Scalar (H) = Scalar (Q)$
30		lmghm	$⊢ F \in (G LMHom H) \to F \in (G GrpHom H)$
31	2 30	syl	$⊢ φ \to F \in (G GrpHom H)$
32	1 31 3 4 6 5	ghmqusker	$⊢ φ \to J \in (Q GrpIso H)$
33		gimghm	$⊢ J \in (Q GrpIso H) \to J \in (Q GrpHom H)$
34	32 33	syl	$⊢ φ \to J \in (Q GrpHom H)$
35	1	ghmker	$⊢ F \in (G GrpHom H) \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
36	31 35	syl	$⊢ φ \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
37	3 36	eqeltrid	$⊢ φ \to K \in NrmSGrp (G)$
38		nsgsubg	$⊢ K \in NrmSGrp (G) \to K \in SubGrp (G)$
39		eqid	$⊢ G ~_{QG} K = G ~_{QG} K$
40	13 39	eqger	$⊢ K \in SubGrp (G) \to (G ~_{QG} K) Er {Base}_{G}$
41	37 38 40	3syl	$⊢ φ \to (G ~_{QG} K) Er {Base}_{G}$
42	41	ad4antr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to (G ~_{QG} K) Er {Base}_{G}$
43		simpllr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to r \in {Base}_{Q}$
44	25 26 27 15	qusbas	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
45	44	ad4antr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
46	43 45	eleqtrrd	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to r \in ({Base}_{G} / (G ~_{QG} K))$
47		simplr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to x \in r$
48		qsel	$⊢ ((G ~_{QG} K) Er {Base}_{G} \land r \in ({Base}_{G} / (G ~_{QG} K)) \land x \in r) \to r = [x] (G ~_{QG} K)$
49	42 46 47 48	syl3anc	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to r = [x] (G ~_{QG} K)$
50	49	oveq2d	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to k \cdot_{Q} r = k \cdot_{Q} [x] (G ~_{QG} K)$
51		eqid	$⊢ {Base}_{Scalar (G)} = {Base}_{Scalar (G)}$
52		eqid	$⊢ \cdot_{G} = \cdot_{G}$
53	15	ad4antr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to G \in LMod$
54	18	ad4antr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to K \in LSubSp (G)$
55		simp-4r	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to k \in {Base}_{Scalar (Q)}$
56	28	fveq2d	$⊢ φ \to {Base}_{Scalar (G)} = {Base}_{Scalar (Q)}$
57	56	ad4antr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to {Base}_{Scalar (G)} = {Base}_{Scalar (Q)}$
58	55 57	eleqtrrd	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to k \in {Base}_{Scalar (G)}$
59	41	qsss	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) \subseteq 𝒫 {Base}_{G}$
60	44 59	eqsstrrd	$⊢ φ \to {Base}_{Q} \subseteq 𝒫 {Base}_{G}$
61	60	sselda	$⊢ (φ \land r \in {Base}_{Q}) \to r \in 𝒫 {Base}_{G}$
62	61	elpwid	$⊢ (φ \land r \in {Base}_{Q}) \to r \subseteq {Base}_{G}$
63	62	ad5ant13	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to r \subseteq {Base}_{G}$
64	63 47	sseldd	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to x \in {Base}_{G}$
65	13 39 51 52 53 54 58 4 8 64	qusvsval	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to k \cdot_{Q} [x] (G ~_{QG} K) = [(k \cdot_{G} x)] (G ~_{QG} K)$
66	50 65	eqtrd	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to k \cdot_{Q} r = [(k \cdot_{G} x)] (G ~_{QG} K)$
67	66	fveq2d	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (k \cdot_{Q} r) = J ([(k \cdot_{G} x)] (G ~_{QG} K))$
68	31	ad4antr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F \in (G GrpHom H)$
69	13 22 52 51	lmodvscl	$⊢ (G \in LMod \land k \in {Base}_{Scalar (G)} \land x \in {Base}_{G}) \to k \cdot_{G} x \in {Base}_{G}$
70	53 58 64 69	syl3anc	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to k \cdot_{G} x \in {Base}_{G}$
71	1 68 3 4 6 70	ghmquskerlem1	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J ([(k \cdot_{G} x)] (G ~_{QG} K)) = F (k \cdot_{G} x)$
72	2	ad4antr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F \in (G LMHom H)$
73	22 51 13 52 9	lmhmlin	$⊢ (F \in (G LMHom H) \land k \in {Base}_{Scalar (G)} \land x \in {Base}_{G}) \to F (k \cdot_{G} x) = k \cdot_{H} F (x)$
74	72 58 64 73	syl3anc	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F (k \cdot_{G} x) = k \cdot_{H} F (x)$
75	67 71 74	3eqtrd	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (k \cdot_{Q} r) = k \cdot_{H} F (x)$
76		simpr	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (r) = F (x)$
77	76	oveq2d	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to k \cdot_{H} J (r) = k \cdot_{H} F (x)$
78	75 77	eqtr4d	$⊢ ((((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (k \cdot_{Q} r) = k \cdot_{H} J (r)$
79	31	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \to F \in (G GrpHom H)$
80		simpr	$⊢ ((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \to r \in {Base}_{Q}$
81	1 79 3 4 6 80	ghmquskerlem2	$⊢ ((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \to \exists x \in r J (r) = F (x)$
82	78 81	r19.29a	$⊢ ((φ \land k \in {Base}_{Scalar (Q)}) \land r \in {Base}_{Q}) \to J (k \cdot_{Q} r) = k \cdot_{H} J (r)$
83	82	anasss	$⊢ (φ \land (k \in {Base}_{Scalar (Q)} \land r \in {Base}_{Q})) \to J (k \cdot_{Q} r) = k \cdot_{H} J (r)$
84	7 8 9 10 11 12 19 21 29 34 83	islmhmd	$⊢ φ \to J \in (Q LMHom H)$
85		eqid	$⊢ {Base}_{H} = {Base}_{H}$
86	7 85	gimf1o	$⊢ J \in (Q GrpIso H) \to J : {Base}_{Q} \underset{1-1 onto}{⟶} {Base}_{H}$
87	32 86	syl	$⊢ φ \to J : {Base}_{Q} \underset{1-1 onto}{⟶} {Base}_{H}$
88	7 85	islmim	$⊢ J \in (Q LMIso H) \leftrightarrow (J \in (Q LMHom H) \land J : {Base}_{Q} \underset{1-1 onto}{⟶} {Base}_{H})$
89	84 87 88	sylanbrc	$⊢ φ \to J \in (Q LMIso H)$

Metamath Proof Explorer

Theorem lmhmqusker

Proof