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	bilani	$⊢ (φ \land X ∥_{r} (G) x) \to (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)$
29		fveq2	$⊢ z \cdot_{G} X = x \to F (z \cdot_{G} X) = F (x)$
30	29	eqcomd	$⊢ z \cdot_{G} X = x \to F (x) = F (z \cdot_{G} X)$
31	30	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)$
32	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)$
33		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}$
34	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}$
35		eqid	$⊢ \cdot_{H} = \cdot_{H}$
36	11 26 35	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)$
37	32 33 34 36	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)$
38	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}$
39	38	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}$
40		rhmrcl2	$⊢ F \in (G RingHom H) \to H \in Ring$
41		ringsrg	$⊢ H \in Ring \to H \in SRing$
42	32 40 41	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$
43		eqid	$⊢ {Base}_{H} = {Base}_{H}$
44	11 43	rhmf	$⊢ F \in (G RingHom H) \to F : {Base}_{G} ⟶ {Base}_{H}$
45	2 44	syl	$⊢ φ \to F : {Base}_{G} ⟶ {Base}_{H}$
46	45	adantr	$⊢ (φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \to F : {Base}_{G} ⟶ {Base}_{H}$
47	46	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}$
48	43 35 1	srgrz	$⊢ (H \in SRing \land F (z) \in {Base}_{H}) \to F (z) \cdot_{H} \underset{˙}{0} = \underset{˙}{0}$
49	42 47 48	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}$
50	39 49	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}$
51	37 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_{G} X) = \underset{˙}{0}$
52	51	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}$
53	31 52	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}$
54		nfv	$⊢ Ⅎ z y \cdot_{G} X = x$
55		nfv	$⊢ Ⅎ y z \cdot_{G} X = x$
56		oveq1	$⊢ y = z \to y \cdot_{G} X = z \cdot_{G} X$
57	56	eqeq1d	$⊢ y = z \to (y \cdot_{G} X = x \leftrightarrow z \cdot_{G} X = x)$
58	54 55 57	cbvrexw	$⊢ \exists y \in {Base}_{G} y \cdot_{G} X = x \leftrightarrow \exists z \in {Base}_{G} z \cdot_{G} X = x$
59	58	bilani	$⊢ (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$
60	59	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$
61	53 60	r19.29a	$⊢ (φ \land (X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x)) \to F (x) = \underset{˙}{0}$
62	61	ex	$⊢ φ \to ((X \in {Base}_{G} \land \exists y \in {Base}_{G} y \cdot_{G} X = x) \to F (x) = \underset{˙}{0})$
63	62	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})$
64	28 63	mpd	$⊢ (φ \land X ∥_{r} (G) x) \to F (x) = \underset{˙}{0}$
65	64	ex	$⊢ φ \to (X ∥_{r} (G) x \to F (x) = \underset{˙}{0})$
66	65	adantr	$⊢ (φ \land x \in \{y \| X ∥_{r} (G) y\}) \to (X ∥_{r} (G) x \to F (x) = \underset{˙}{0})$
67	25 66	mpd	$⊢ (φ \land x \in \{y \| X ∥_{r} (G) y\}) \to F (x) = \underset{˙}{0}$
68	67	ex	$⊢ φ \to (x \in \{y \| X ∥_{r} (G) y\} \to F (x) = \underset{˙}{0})$
69	68	adantr	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to (x \in \{y \| X ∥_{r} (G) y\} \to F (x) = \underset{˙}{0})$
70	18 69	mpd	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to F (x) = \underset{˙}{0}$
71		fvexd	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to F (x) \in V$
72		elsng	$⊢ F (x) \in V \to (F (x) \in \{\underset{˙}{0}\} \leftrightarrow F (x) = \underset{˙}{0})$
73	71 72	syl	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to (F (x) \in \{\underset{˙}{0}\} \leftrightarrow F (x) = \underset{˙}{0})$
74	70 73	mpbird	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to F (x) \in \{\underset{˙}{0}\}$
75	45	ffund	$⊢ φ \to Fun F$
76	75	adantr	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to Fun F$
77		eqid	$⊢ LIdeal (G) = LIdeal (G)$
78	77 11	lidl1	$⊢ G \in Ring \to {Base}_{G} \in LIdeal (G)$
79	10 78	syl	$⊢ φ \to {Base}_{G} \in LIdeal (G)$
80	8	snssd	$⊢ φ \to \{X\} \subseteq {Base}_{G}$
81	12 77	rspssp	$⊢ (G \in Ring \land {Base}_{G} \in LIdeal (G) \land \{X\} \subseteq {Base}_{G}) \to RSpan (G) (\{X\}) \subseteq {Base}_{G}$
82	10 79 80 81	syl3anc	$⊢ φ \to RSpan (G) (\{X\}) \subseteq {Base}_{G}$
83	82	sselda	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to x \in {Base}_{G}$
84		fdm	$⊢ F : {Base}_{G} ⟶ {Base}_{H} \to dom F = {Base}_{G}$
85	45 84	syl	$⊢ φ \to dom F = {Base}_{G}$
86	85	adantr	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to dom F = {Base}_{G}$
87	83 86	eleqtrrd	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to x \in dom F$
88		fvimacnv	$⊢ (Fun F \land x \in dom F) \to (F (x) \in \{\underset{˙}{0}\} \leftrightarrow x \in F^{-1} [\{\underset{˙}{0}\}])$
89	76 87 88	syl2anc	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to (F (x) \in \{\underset{˙}{0}\} \leftrightarrow x \in F^{-1} [\{\underset{˙}{0}\}])$
90	74 89	mpbid	$⊢ (φ \land x \in RSpan (G) (\{X\})) \to x \in F^{-1} [\{\underset{˙}{0}\}]$
91	90	ex	$⊢ φ \to (x \in RSpan (G) (\{X\}) \to x \in F^{-1} [\{\underset{˙}{0}\}])$
92	91	ssrdv	$⊢ φ \to RSpan (G) (\{X\}) \subseteq F^{-1} [\{\underset{˙}{0}\}]$
93	3	eqcomi	$⊢ F^{-1} [\{\underset{˙}{0}\}] = K$
94	92 93	sseqtrdi	$⊢ φ \to RSpan (G) (\{X\}) \subseteq K$
95	7 94	eqsstrid	$⊢ φ \to N \subseteq K$
96	12 11 77	rspcl	$⊢ (G \in Ring \land \{X\} \subseteq {Base}_{G}) \to RSpan (G) (\{X\}) \in LIdeal (G)$
97	10 80 96	syl2anc	$⊢ φ \to RSpan (G) (\{X\}) \in LIdeal (G)$
98	7 97	eqeltrid	$⊢ φ \to N \in LIdeal (G)$
99	1 2 3 4 5 6 95 98	rhmqusnsg	$⊢ φ \to J \in (Q RingHom H)$
100	2	adantr	$⊢ (φ \land g \in {Base}_{G}) \to F \in (G RingHom H)$
101		rhmghm	$⊢ F \in (G RingHom H) \to F \in (G GrpHom H)$
102	100 101	syl	$⊢ (φ \land g \in {Base}_{G}) \to F \in (G GrpHom H)$
103	95	adantr	$⊢ (φ \land g \in {Base}_{G}) \to N \subseteq K$
104		lidlnsg	$⊢ (G \in Ring \land N \in LIdeal (G)) \to N \in NrmSGrp (G)$
105	10 98 104	syl2anc	$⊢ φ \to N \in NrmSGrp (G)$
106	105	adantr	$⊢ (φ \land g \in {Base}_{G}) \to N \in NrmSGrp (G)$
107		simpr	$⊢ (φ \land g \in {Base}_{G}) \to g \in {Base}_{G}$
108	1 102 3 4 5 103 106 107	ghmqusnsglem1	$⊢ (φ \land g \in {Base}_{G}) \to J ([g] (G ~_{QG} N)) = F (g)$
109	108	ralrimiva	$⊢ φ \to \forall g \in {Base}_{G} J ([g] (G ~_{QG} N)) = F (g)$
110	99 109	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