rhmquskerlem

Description: The mapping J induced by a ring homomorphism F from the quotient group Q over F 's kernel K is a ring homomorphism. (Contributed by Thierry Arnoux, 22-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		rhmqusker.1	$⊢ \underset{˙}{0} = 0_{H}$
2		rhmqusker.f	$⊢ φ \to F \in (G RingHom H)$
3		rhmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
4		rhmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
5		rhmquskerlem.j	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
6		rhmquskerlem.2	$⊢ φ \to G \in CRing$
7		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
8		eqid	$⊢ 1_{Q} = 1_{Q}$
9		eqid	$⊢ 1_{H} = 1_{H}$
10		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
11		eqid	$⊢ \cdot_{H} = \cdot_{H}$
12		rhmrcl1	$⊢ F \in (G RingHom H) \to G \in Ring$
13	2 12	syl	$⊢ φ \to G \in Ring$
14		eqid	$⊢ LIdeal (G) = LIdeal (G)$
15	14 1	kerlidl	$⊢ F \in (G RingHom H) \to F^{-1} [\{\underset{˙}{0}\}] \in LIdeal (G)$
16	2 15	syl	$⊢ φ \to F^{-1} [\{\underset{˙}{0}\}] \in LIdeal (G)$
17	3 16	eqeltrid	$⊢ φ \to K \in LIdeal (G)$
18	14	crng2idl	$⊢ G \in CRing \to LIdeal (G) = 2Ideal (G)$
19	6 18	syl	$⊢ φ \to LIdeal (G) = 2Ideal (G)$
20	17 19	eleqtrd	$⊢ φ \to K \in 2Ideal (G)$
21		eqid	$⊢ 2Ideal (G) = 2Ideal (G)$
22		eqid	$⊢ 1_{G} = 1_{G}$
23	4 21 22	qus1	$⊢ (G \in Ring \land K \in 2Ideal (G)) \to (Q \in Ring \land [1_{G}] (G ~_{QG} K) = 1_{Q})$
24	13 20 23	syl2anc	$⊢ φ \to (Q \in Ring \land [1_{G}] (G ~_{QG} K) = 1_{Q})$
25	24	simpld	$⊢ φ \to Q \in Ring$
26		rhmrcl2	$⊢ F \in (G RingHom H) \to H \in Ring$
27	2 26	syl	$⊢ φ \to H \in Ring$
28		rhmghm	$⊢ F \in (G RingHom H) \to F \in (G GrpHom H)$
29	2 28	syl	$⊢ φ \to F \in (G GrpHom H)$
30		eqid	$⊢ {Base}_{G} = {Base}_{G}$
31	30 22	ringidcl	$⊢ G \in Ring \to 1_{G} \in {Base}_{G}$
32	13 31	syl	$⊢ φ \to 1_{G} \in {Base}_{G}$
33	1 29 3 4 5 32	ghmquskerlem1	$⊢ φ \to J ([1_{G}] (G ~_{QG} K)) = F (1_{G})$
34	24	simprd	$⊢ φ \to [1_{G}] (G ~_{QG} K) = 1_{Q}$
35	34	fveq2d	$⊢ φ \to J ([1_{G}] (G ~_{QG} K)) = J (1_{Q})$
36	22 9	rhm1	$⊢ F \in (G RingHom H) \to F (1_{G}) = 1_{H}$
37	2 36	syl	$⊢ φ \to F (1_{G}) = 1_{H}$
38	33 35 37	3eqtr3d	$⊢ φ \to J (1_{Q}) = 1_{H}$
39	2	ad6antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to F \in (G RingHom H)$
40	4	a1i	$⊢ φ \to Q = G /_{𝑠} (G ~_{QG} K)$
41		eqidd	$⊢ φ \to {Base}_{G} = {Base}_{G}$
42		ovexd	$⊢ φ \to G ~_{QG} K \in V$
43	40 41 42 6	qusbas	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
44	1	ghmker	$⊢ F \in (G GrpHom H) \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
45	29 44	syl	$⊢ φ \to F^{-1} [\{\underset{˙}{0}\}] \in NrmSGrp (G)$
46	3 45	eqeltrid	$⊢ φ \to K \in NrmSGrp (G)$
47		nsgsubg	$⊢ K \in NrmSGrp (G) \to K \in SubGrp (G)$
48		eqid	$⊢ G ~_{QG} K = G ~_{QG} K$
49	30 48	eqger	$⊢ K \in SubGrp (G) \to (G ~_{QG} K) Er {Base}_{G}$
50	46 47 49	3syl	$⊢ φ \to (G ~_{QG} K) Er {Base}_{G}$
51	50	qsss	$⊢ φ \to {Base}_{G} / (G ~_{QG} K) \subseteq 𝒫 {Base}_{G}$
52	43 51	eqsstrrd	$⊢ φ \to {Base}_{Q} \subseteq 𝒫 {Base}_{G}$
53	52	sselda	$⊢ (φ \land r \in {Base}_{Q}) \to r \in 𝒫 {Base}_{G}$
54	53	elpwid	$⊢ (φ \land r \in {Base}_{Q}) \to r \subseteq {Base}_{G}$
55	54	ad5antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r \subseteq {Base}_{G}$
56		simp-4r	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to x \in r$
57	55 56	sseldd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to x \in {Base}_{G}$
58	52	sselda	$⊢ (φ \land s \in {Base}_{Q}) \to s \in 𝒫 {Base}_{G}$
59	58	elpwid	$⊢ (φ \land s \in {Base}_{Q}) \to s \subseteq {Base}_{G}$
60	59	adantlr	$⊢ ((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \to s \subseteq {Base}_{G}$
61	60	ad4antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to s \subseteq {Base}_{G}$
62		simplr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to y \in s$
63	61 62	sseldd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to y \in {Base}_{G}$
64		eqid	$⊢ \cdot_{G} = \cdot_{G}$
65	30 64 11	rhmmul	$⊢ (F \in (G RingHom H) \land x \in {Base}_{G} \land y \in {Base}_{G}) \to F (x \cdot_{G} y) = F (x) \cdot_{H} F (y)$
66	39 57 63 65	syl3anc	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to F (x \cdot_{G} y) = F (x) \cdot_{H} F (y)$
67	50	ad6antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to (G ~_{QG} K) Er {Base}_{G}$
68		simp-6r	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r \in {Base}_{Q}$
69	43	ad6antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to {Base}_{G} / (G ~_{QG} K) = {Base}_{Q}$
70	68 69	eleqtrrd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r \in ({Base}_{G} / (G ~_{QG} K))$
71		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)$
72	67 70 56 71	syl3anc	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r = [x] (G ~_{QG} K)$
73		simp-5r	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to s \in {Base}_{Q}$
74	73 69	eleqtrrd	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to s \in ({Base}_{G} / (G ~_{QG} K))$
75		qsel	$⊢ ((G ~_{QG} K) Er {Base}_{G} \land s \in ({Base}_{G} / (G ~_{QG} K)) \land y \in s) \to s = [y] (G ~_{QG} K)$
76	67 74 62 75	syl3anc	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to s = [y] (G ~_{QG} K)$
77	72 76	oveq12d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to r \cdot_{Q} s = [x] (G ~_{QG} K) \cdot_{Q} [y] (G ~_{QG} K)$
78	6	ad6antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to G \in CRing$
79	17	ad6antr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to K \in LIdeal (G)$
80	4 30 64 10 78 79 57 63	qusmul	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to [x] (G ~_{QG} K) \cdot_{Q} [y] (G ~_{QG} K) = [(x \cdot_{G} y)] (G ~_{QG} K)$
81	77 80	eqtr2d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to [(x \cdot_{G} y)] (G ~_{QG} K) = r \cdot_{Q} s$
82	81	fveq2d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J ([(x \cdot_{G} y)] (G ~_{QG} K)) = J (r \cdot_{Q} s)$
83	39 28	syl	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to F \in (G GrpHom H)$
84	39 12	syl	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to G \in Ring$
85	30 64 84 57 63	ringcld	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to x \cdot_{G} y \in {Base}_{G}$
86	1 83 3 4 5 85	ghmquskerlem1	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J ([(x \cdot_{G} y)] (G ~_{QG} K)) = F (x \cdot_{G} y)$
87	82 86	eqtr3d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (r \cdot_{Q} s) = F (x \cdot_{G} y)$
88		simpllr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (r) = F (x)$
89		simpr	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (s) = F (y)$
90	88 89	oveq12d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (r) \cdot_{H} J (s) = F (x) \cdot_{H} F (y)$
91	66 87 90	3eqtr4d	$⊢ ((((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \land y \in s) \land J (s) = F (y)) \to J (r \cdot_{Q} s) = J (r) \cdot_{H} J (s)$
92	29	ad4antr	$⊢ ((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to F \in (G GrpHom H)$
93		simpllr	$⊢ ((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to s \in {Base}_{Q}$
94	1 92 3 4 5 93	ghmquskerlem2	$⊢ ((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to \exists y \in s J (s) = F (y)$
95	91 94	r19.29a	$⊢ ((((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \land x \in r) \land J (r) = F (x)) \to J (r \cdot_{Q} s) = J (r) \cdot_{H} J (s)$
96	29	ad2antrr	$⊢ ((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \to F \in (G GrpHom H)$
97		simplr	$⊢ ((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \to r \in {Base}_{Q}$
98	1 96 3 4 5 97	ghmquskerlem2	$⊢ ((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \to \exists x \in r J (r) = F (x)$
99	95 98	r19.29a	$⊢ ((φ \land r \in {Base}_{Q}) \land s \in {Base}_{Q}) \to J (r \cdot_{Q} s) = J (r) \cdot_{H} J (s)$
100	99	anasss	$⊢ (φ \land (r \in {Base}_{Q} \land s \in {Base}_{Q})) \to J (r \cdot_{Q} s) = J (r) \cdot_{H} J (s)$
101	1 29 3 4 5	ghmquskerlem3	$⊢ φ \to J \in (Q GrpHom H)$
102	7 8 9 10 11 25 27 38 100 101	isrhm2d	$⊢ φ \to J \in (Q RingHom H)$

Metamath Proof Explorer

Theorem rhmquskerlem

Proof