rhmqusspan

Description: Ring homomorphism out of a quotient given an ideal spanned by a singleton. (Contributed by metakunt, 7-Jun-2025)

	Ref	Expression
Hypotheses	rhmqusspan.1	$⊢ \underset{˙}{0} = 0_{H}$
	rhmqusspan.2	$⊢ φ \to F \in (G RingHom H)$
	rhmqusspan.3	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
	rhmqusspan.4	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
	rhmqusspan.5	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
	rhmqusspan.6	$⊢ φ \to G \in CRing$
	rhmqusspan.7	$⊢ N = RSpan (G) (\{X\})$
	rhmqusspan.8	$⊢ φ \to X \in {Base}_{G}$
	rhmqusspan.9	$⊢ φ \to F (X) = \underset{˙}{0}$
Assertion	rhmqusspan	$⊢ φ \to (J \in (Q RingHom H) \land \forall g \in {Base}_{G} J ([g] (G ~_{QG} N)) = F (g))$

Proof

Step	Hyp	Ref	Expression
1		rhmqusspan.1	$⊢ \underset{˙}{0} = 0_{H}$
2		rhmqusspan.2	$⊢ φ \to F \in (G RingHom H)$
3		rhmqusspan.3	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
4		rhmqusspan.4	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
5		rhmqusspan.5	$⊢ J = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
6		rhmqusspan.6	$⊢ φ \to G \in CRing$
7		rhmqusspan.7	$⊢ N = RSpan (G) (\{X\})$
8		rhmqusspan.8	$⊢ φ \to X \in {Base}_{G}$
9		rhmqusspan.9	$⊢ φ \to F (X) = \underset{˙}{0}$
10	6	crngringd	$⊢ φ \to G \in Ring$
11		eqid	$⊢ {Base}_{G} = {Base}_{G}$
12		eqid	$⊢ RSpan (G) = RSpan (G)$
13		eqid	$⊢ ∥_{r} (G) = ∥_{r} (G)$
14	11 12 13	rspsn	$⊢ (G \in Ring \land X \in {Base}_{G}) \to RSpan (G) (\{X\}) = \{y \| X ∥_{r} (G) y\}$
15	10 8 14	syl2anc	$⊢ φ \to RSpan (G) (\{X\}) = \{y \| X ∥_{r} (G) y\}$
16	15	eleq2d	$⊢ φ \to (x \in RSpan (G) (\{X\}) \leftrightarrow x \in \{y \| X ∥_{r} (G) y\})$
17	16	biimpd	$⊢ φ \to (x \in RSpan (G) (\{X\}) \to x \in \{y \| X ∥_{r} (G) y\})$
18	17	imp	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to x \in \{y \| X ∥_{r} (G) y\}$
19		vex	$⊢ x \in V$
20	19	a1i	$⊢ φ \to x \in V$
21		breq2	$⊢ y = x \to (X ∥_{r} (G) y \leftrightarrow X ∥_{r} (G) x)$
22	21	elabg	$⊢ x \in V \to (x \in \{y \| X ∥_{r} (G) y\} \leftrightarrow X ∥_{r} (G) x)$
23	22	biimpd	$⊢ x \in V \to (x \in \{y \| X ∥_{r} (G) y\} \to X ∥_{r} (G) x)$
24	20 23	syl	$⊢ φ \to (x \in \{y \| X ∥_{r} (G) y\} \to X ∥_{r} (G) x)$
25	24	imp	$⊢ (φ \land x \in \{y \| X ∥_{r} (G) y\}) \to X ∥_{r} (G) x$
26		eqid	$⊢ \cdot_{G} = \cdot_{G}$
27	11 13 26	dvdsr	$⊢ X ∥_{r} (G) x \leftrightarrow (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)$
28	27	biimpi	$⊢ X ∥_{r} (G) x \to (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)$
29	28	adantl	$⊢ (φ \land X ∥_{r} (G) x) \to (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)$
30		fveq2	$⊢ z \cdot_{G} X = x \to F (z \cdot_{G} X) = F (x)$
31	30	eqcomd	$⊢ z \cdot_{G} X = x \to F (x) = F (z \cdot_{G} X)$
32	31	adantl	$⊢ (((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \land z \cdot_{G} X = x) \to F (x) = F (z \cdot_{G} X)$
33	2	ad2antrr	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to F \in (G RingHom H)$
34		simpr	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to z \in {Base}_{G}$
35	8	ad2antrr	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to X \in {Base}_{G}$
36		eqid	$⊢ \cdot_{H} = \cdot_{H}$
37	11 26 36	rhmmul	$⊢ (F \in (G RingHom H) \land z \in {Base}_{G} \land X \in {Base}_{G}) \to F (z \cdot_{G} X) = F (z) \cdot_{H} F (X)$
38	33 34 35 37	syl3anc	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to F (z \cdot_{G} X) = F (z) \cdot_{H} F (X)$
39	9	ad2antrr	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to F (X) = \underset{˙}{0}$
40	39	oveq2d	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to F (z) \cdot_{H} F (X) = F (z) \cdot_{H} \underset{˙}{0}$
41		rhmrcl2	$⊢ F \in (G RingHom H) \to H \in Ring$
42		ringsrg	$⊢ H \in Ring \to H \in SRing$
43	33 41 42	3syl	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to H \in SRing$
44		eqid	$⊢ {Base}_{H} = {Base}_{H}$
45	11 44	rhmf	$⊢ F \in (G RingHom H) \to F : {Base}_{G} ⟶ {Base}_{H}$
46	2 45	syl	$⊢ φ \to F : {Base}_{G} ⟶ {Base}_{H}$
47	46	adantr	$⊢ (φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \to F : {Base}_{G} ⟶ {Base}_{H}$
48	47	ffvelcdmda	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to F (z) \in {Base}_{H}$
49	44 36 1	srgrz	$⊢ (H \in SRing \land F (z) \in {Base}_{H}) \to F (z) \cdot_{H} \underset{˙}{0} = \underset{˙}{0}$
50	43 48 49	syl2anc	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to F (z) \cdot_{H} \underset{˙}{0} = \underset{˙}{0}$
51	40 50	eqtrd	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to F (z) \cdot_{H} F (X) = \underset{˙}{0}$
52	38 51	eqtrd	$⊢ ((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \to F (z \cdot_{G} X) = \underset{˙}{0}$
53	52	adantr	$⊢ (((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \land z \cdot_{G} X = x) \to F (z \cdot_{G} X) = \underset{˙}{0}$
54	32 53	eqtrd	$⊢ (((φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \land z \in {Base}_{G}) \land z \cdot_{G} X = x) \to F (x) = \underset{˙}{0}$
55		nfv	$⊢ Ⅎ z y \cdot_{G} X = x$
56		nfv	$⊢ Ⅎ y z \cdot_{G} X = x$
57		oveq1	$⊢ y = z \to y \cdot_{G} X = z \cdot_{G} X$
58	57	eqeq1d	$⊢ y = z \to (y \cdot_{G} X = x \leftrightarrow z \cdot_{G} X = x)$
59	55 56 58	cbvrexw	$⊢ \exists y \in {Base}_{G} y \cdot_{G} X = x \leftrightarrow \exists z \in {Base}_{G} z \cdot_{G} X = x$
60	59	biimpi	$⊢ \exists y \in {Base}_{G} y \cdot_{G} X = x \to \exists z \in {Base}_{G} z \cdot_{G} X = x$
61	60	adantl	$⊢ (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x) \to \exists z \in {Base}_{G} z \cdot_{G} X = x$
62	61	adantl	$⊢ (φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \to \exists z \in {Base}_{G} z \cdot_{G} X = x$
63	54 62	r19.29a	$⊢ (φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \to F (x) = \underset{˙}{0}$
64	63	ex	$⊢ φ \to ((X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x) \to F (x) = \underset{˙}{0})$
65	64	adantr	$⊢ (φ \land X ∥_{r} (G) x) \to ((X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x) \to F (x) = \underset{˙}{0})$
66	29 65	mpd	$⊢ (φ \land X ∥_{r} (G) x) \to F (x) = \underset{˙}{0}$
67	66	ex	$⊢ φ \to (X ∥_{r} (G) x \to F (x) = \underset{˙}{0})$
68	67	adantr	$⊢ (φ \land x \in \{y \| X ∥_{r} (G) y\}) \to (X ∥_{r} (G) x \to F (x) = \underset{˙}{0})$
69	25 68	mpd	$⊢ (φ \land x \in \{y \| X ∥_{r} (G) y\}) \to F (x) = \underset{˙}{0}$
70	69	ex	$⊢ φ \to (x \in \{y \| X ∥_{r} (G) y\} \to F (x) = \underset{˙}{0})$
71	70	adantr	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to (x \in \{y \| X ∥_{r} (G) y\} \to F (x) = \underset{˙}{0})$
72	18 71	mpd	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to F (x) = \underset{˙}{0}$
73		fvexd	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to F (x) \in V$
74		elsng	$⊢ F (x) \in V \to (F (x) \in \{\underset{˙}{0}\} \leftrightarrow F (x) = \underset{˙}{0})$
75	73 74	syl	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to (F (x) \in \{\underset{˙}{0}\} \leftrightarrow F (x) = \underset{˙}{0})$
76	72 75	mpbird	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to F (x) \in \{\underset{˙}{0}\}$
77	46	ffund	$⊢ φ \to Fun F$
78	77	adantr	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to Fun F$
79		eqid	$⊢ LIdeal (G) = LIdeal (G)$
80	79 11	lidl1	$⊢ G \in Ring \to {Base}_{G} \in LIdeal (G)$
81	10 80	syl	$⊢ φ \to {Base}_{G} \in LIdeal (G)$
82	8	snssd	$⊢ φ \to \{X\} \subseteq {Base}_{G}$
83	12 79	rspssp	$⊢ (G \in Ring \land {Base}_{G} \in LIdeal (G) \land \{X\} \subseteq {Base}_{G}) \to RSpan (G) (\{X\}) \subseteq {Base}_{G}$
84	10 81 82 83	syl3anc	$⊢ φ \to RSpan (G) (\{X\}) \subseteq {Base}_{G}$
85	84	sselda	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to x \in {Base}_{G}$
86		fdm	$⊢ F : {Base}_{G} ⟶ {Base}_{H} \to dom F = {Base}_{G}$
87	46 86	syl	$⊢ φ \to dom F = {Base}_{G}$
88	87	adantr	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to dom F = {Base}_{G}$
89	85 88	eleqtrrd	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to x \in dom F$
90		fvimacnv	$⊢ (Fun F \land x \in dom F) \to (F (x) \in \{\underset{˙}{0}\} \leftrightarrow x \in F^{-1} [\{\underset{˙}{0}\}])$
91	78 89 90	syl2anc	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to (F (x) \in \{\underset{˙}{0}\} \leftrightarrow x \in F^{-1} [\{\underset{˙}{0}\}])$
92	76 91	mpbid	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to x \in F^{-1} [\{\underset{˙}{0}\}]$
93	92	ex	$⊢ φ \to (x \in RSpan (G) (\{X\}) \to x \in F^{-1} [\{\underset{˙}{0}\}])$
94	93	ssrdv	$⊢ φ \to RSpan (G) (\{X\}) \subseteq F^{-1} [\{\underset{˙}{0}\}]$
95	3	eqcomi	$⊢ F^{-1} [\{\underset{˙}{0}\}] = K$
96	94 95	sseqtrdi	$⊢ φ \to RSpan (G) (\{X\}) \subseteq K$
97	7 96	eqsstrid	$⊢ φ \to N \subseteq K$
98	12 11 79	rspcl	$⊢ (G \in Ring \land \{X\} \subseteq {Base}_{G}) \to RSpan (G) (\{X\}) \in LIdeal (G)$
99	10 82 98	syl2anc	$⊢ φ \to RSpan (G) (\{X\}) \in LIdeal (G)$
100	7 99	eqeltrid	$⊢ φ \to N \in LIdeal (G)$
101	1 2 3 4 5 6 97 100	rhmqusnsg	$⊢ φ \to J \in (Q RingHom H)$
102	2	adantr	$⊢ (φ \land g \in {Base}_{G}) \to F \in (G RingHom H)$
103		rhmghm	$⊢ F \in (G RingHom H) \to F \in (G GrpHom H)$
104	102 103	syl	$⊢ (φ \land g \in {Base}_{G}) \to F \in (G GrpHom H)$
105	97	adantr	$⊢ (φ \land g \in {Base}_{G}) \to N \subseteq K$
106		lidlnsg	$⊢ (G \in Ring \land N \in LIdeal (G)) \to N \in NrmSGrp (G)$
107	10 100 106	syl2anc	$⊢ φ \to N \in NrmSGrp (G)$
108	107	adantr	$⊢ (φ \land g \in {Base}_{G}) \to N \in NrmSGrp (G)$
109		simpr	$⊢ (φ \land g \in {Base}_{G}) \to g \in {Base}_{G}$
110	1 104 3 4 5 105 108 109	ghmqusnsglem1	$⊢ (φ \land g \in {Base}_{G}) \to J ([g] (G ~_{QG} N)) = F (g)$
111	110	ralrimiva	$⊢ φ \to \forall g \in {Base}_{G} J ([g] (G ~_{QG} N)) = F (g)$
112	101 111	jca	$⊢ φ \to (J \in (Q RingHom H) \land \forall g \in {Base}_{G} J ([g] (G ~_{QG} N)) = F (g))$

Metamath Proof Explorer

Theorem rhmqusspan

Proof