rhmqusnsg

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

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

Proof

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

Metamath Proof Explorer

Theorem rhmqusnsg

Proof