keridl

Description: The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011)

	Ref	Expression
Hypotheses	keridl.1	$⊢ G = 1^{st} (S)$
	keridl.2	$⊢ Z = GId (G)$
Assertion	keridl	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to F^{-1} [\{Z\}] \in Idl (R)$

Proof

Step	Hyp	Ref	Expression
1		keridl.1	$⊢ G = 1^{st} (S)$
2		keridl.2	$⊢ Z = GId (G)$
3		cnvimass	$⊢ F^{-1} [\{Z\}] \subseteq dom F$
4		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
5		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
6		eqid	$⊢ ran G = ran G$
7	4 5 1 6	rngohomf	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to F : ran 1^{st} (R) ⟶ ran G$
8	3 7	fssdm	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to F^{-1} [\{Z\}] \subseteq ran 1^{st} (R)$
9		eqid	$⊢ GId (1^{st} (R)) = GId (1^{st} (R))$
10	4 5 9	rngo0cl	$⊢ R \in RingOps \to GId (1^{st} (R)) \in ran 1^{st} (R)$
11	10	3ad2ant1	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to GId (1^{st} (R)) \in ran 1^{st} (R)$
12	4 9 1 2	rngohom0	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to F (GId (1^{st} (R))) = Z$
13		fvex	$⊢ F (GId (1^{st} (R))) \in V$
14	13	elsn	$⊢ F (GId (1^{st} (R))) \in \{Z\} \leftrightarrow F (GId (1^{st} (R))) = Z$
15	12 14	sylibr	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to F (GId (1^{st} (R))) \in \{Z\}$
16		ffn	$⊢ F : ran 1^{st} (R) ⟶ ran G \to F Fn ran 1^{st} (R)$
17		elpreima	$⊢ F Fn ran 1^{st} (R) \to (GId (1^{st} (R)) \in F^{-1} [\{Z\}] \leftrightarrow (GId (1^{st} (R)) \in ran 1^{st} (R) \land F (GId (1^{st} (R))) \in \{Z\}))$
18	7 16 17	3syl	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (GId (1^{st} (R)) \in F^{-1} [\{Z\}] \leftrightarrow (GId (1^{st} (R)) \in ran 1^{st} (R) \land F (GId (1^{st} (R))) \in \{Z\}))$
19	11 15 18	mpbir2and	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to GId (1^{st} (R)) \in F^{-1} [\{Z\}]$
20		an4	$⊢ ((x \in ran 1^{st} (R) \land F (x) \in \{Z\}) \land (y \in ran 1^{st} (R) \land F (y) \in \{Z\})) \leftrightarrow ((x \in ran 1^{st} (R) \land y \in ran 1^{st} (R)) \land (F (x) \in \{Z\} \land F (y) \in \{Z\}))$
21	4 5 1	rngohomadd	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land y \in ran 1^{st} (R))) \to F (x 1^{st} (R) y) = F (x) G F (y)$
22	21	adantr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land y \in ran 1^{st} (R))) \land (F (x) = Z \land F (y) = Z)) \to F (x 1^{st} (R) y) = F (x) G F (y)$
23		oveq12	$⊢ (F (x) = Z \land F (y) = Z) \to F (x) G F (y) = Z G Z$
24	23	adantl	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land y \in ran 1^{st} (R))) \land (F (x) = Z \land F (y) = Z)) \to F (x) G F (y) = Z G Z$
25	1	rngogrpo	$⊢ S \in RingOps \to G \in GrpOp$
26	6 2	grpoidcl	$⊢ G \in GrpOp \to Z \in ran G$
27	6 2	grpolid	$⊢ (G \in GrpOp \land Z \in ran G) \to Z G Z = Z$
28	25 26 27	syl2anc2	$⊢ S \in RingOps \to Z G Z = Z$
29	28	3ad2ant2	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to Z G Z = Z$
30	29	ad2antrr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land y \in ran 1^{st} (R))) \land (F (x) = Z \land F (y) = Z)) \to Z G Z = Z$
31	22 24 30	3eqtrd	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land y \in ran 1^{st} (R))) \land (F (x) = Z \land F (y) = Z)) \to F (x 1^{st} (R) y) = Z$
32	31	ex	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land y \in ran 1^{st} (R))) \to ((F (x) = Z \land F (y) = Z) \to F (x 1^{st} (R) y) = Z)$
33		fvex	$⊢ F (x) \in V$
34	33	elsn	$⊢ F (x) \in \{Z\} \leftrightarrow F (x) = Z$
35		fvex	$⊢ F (y) \in V$
36	35	elsn	$⊢ F (y) \in \{Z\} \leftrightarrow F (y) = Z$
37	34 36	anbi12i	$⊢ (F (x) \in \{Z\} \land F (y) \in \{Z\}) \leftrightarrow (F (x) = Z \land F (y) = Z)$
38		fvex	$⊢ F (x 1^{st} (R) y) \in V$
39	38	elsn	$⊢ F (x 1^{st} (R) y) \in \{Z\} \leftrightarrow F (x 1^{st} (R) y) = Z$
40	32 37 39	3imtr4g	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land y \in ran 1^{st} (R))) \to ((F (x) \in \{Z\} \land F (y) \in \{Z\}) \to F (x 1^{st} (R) y) \in \{Z\})$
41	40	imdistanda	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (((x \in ran 1^{st} (R) \land y \in ran 1^{st} (R)) \land (F (x) \in \{Z\} \land F (y) \in \{Z\})) \to ((x \in ran 1^{st} (R) \land y \in ran 1^{st} (R)) \land F (x 1^{st} (R) y) \in \{Z\}))$
42	4 5	rngogcl	$⊢ (R \in RingOps \land x \in ran 1^{st} (R) \land y \in ran 1^{st} (R)) \to x 1^{st} (R) y \in ran 1^{st} (R)$
43	42	3expib	$⊢ R \in RingOps \to ((x \in ran 1^{st} (R) \land y \in ran 1^{st} (R)) \to x 1^{st} (R) y \in ran 1^{st} (R))$
44	43	3ad2ant1	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to ((x \in ran 1^{st} (R) \land y \in ran 1^{st} (R)) \to x 1^{st} (R) y \in ran 1^{st} (R))$
45	44	anim1d	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (((x \in ran 1^{st} (R) \land y \in ran 1^{st} (R)) \land F (x 1^{st} (R) y) \in \{Z\}) \to (x 1^{st} (R) y \in ran 1^{st} (R) \land F (x 1^{st} (R) y) \in \{Z\}))$
46	41 45	syld	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (((x \in ran 1^{st} (R) \land y \in ran 1^{st} (R)) \land (F (x) \in \{Z\} \land F (y) \in \{Z\})) \to (x 1^{st} (R) y \in ran 1^{st} (R) \land F (x 1^{st} (R) y) \in \{Z\}))$
47	20 46	syl5bi	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (((x \in ran 1^{st} (R) \land F (x) \in \{Z\}) \land (y \in ran 1^{st} (R) \land F (y) \in \{Z\})) \to (x 1^{st} (R) y \in ran 1^{st} (R) \land F (x 1^{st} (R) y) \in \{Z\}))$
48		elpreima	$⊢ F Fn ran 1^{st} (R) \to (x \in F^{-1} [\{Z\}] \leftrightarrow (x \in ran 1^{st} (R) \land F (x) \in \{Z\}))$
49	7 16 48	3syl	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (x \in F^{-1} [\{Z\}] \leftrightarrow (x \in ran 1^{st} (R) \land F (x) \in \{Z\}))$
50		elpreima	$⊢ F Fn ran 1^{st} (R) \to (y \in F^{-1} [\{Z\}] \leftrightarrow (y \in ran 1^{st} (R) \land F (y) \in \{Z\}))$
51	7 16 50	3syl	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (y \in F^{-1} [\{Z\}] \leftrightarrow (y \in ran 1^{st} (R) \land F (y) \in \{Z\}))$
52	49 51	anbi12d	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to ((x \in F^{-1} [\{Z\}] \land y \in F^{-1} [\{Z\}]) \leftrightarrow ((x \in ran 1^{st} (R) \land F (x) \in \{Z\}) \land (y \in ran 1^{st} (R) \land F (y) \in \{Z\})))$
53		elpreima	$⊢ F Fn ran 1^{st} (R) \to (x 1^{st} (R) y \in F^{-1} [\{Z\}] \leftrightarrow (x 1^{st} (R) y \in ran 1^{st} (R) \land F (x 1^{st} (R) y) \in \{Z\}))$
54	7 16 53	3syl	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (x 1^{st} (R) y \in F^{-1} [\{Z\}] \leftrightarrow (x 1^{st} (R) y \in ran 1^{st} (R) \land F (x 1^{st} (R) y) \in \{Z\}))$
55	47 52 54	3imtr4d	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to ((x \in F^{-1} [\{Z\}] \land y \in F^{-1} [\{Z\}]) \to x 1^{st} (R) y \in F^{-1} [\{Z\}])$
56	55	impl	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land x \in F^{-1} [\{Z\}]) \land y \in F^{-1} [\{Z\}]) \to x 1^{st} (R) y \in F^{-1} [\{Z\}]$
57	56	ralrimiva	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land x \in F^{-1} [\{Z\}]) \to \forall y \in F^{-1} [\{Z\}] x 1^{st} (R) y \in F^{-1} [\{Z\}]$
58	34	anbi2i	$⊢ (x \in ran 1^{st} (R) \land F (x) \in \{Z\}) \leftrightarrow (x \in ran 1^{st} (R) \land F (x) = Z)$
59		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
60	4 59 5	rngocl	$⊢ (R \in RingOps \land z \in ran 1^{st} (R) \land x \in ran 1^{st} (R)) \to z 2^{nd} (R) x \in ran 1^{st} (R)$
61	60	3expb	$⊢ (R \in RingOps \land (z \in ran 1^{st} (R) \land x \in ran 1^{st} (R))) \to z 2^{nd} (R) x \in ran 1^{st} (R)$
62	61	3ad2antl1	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (z \in ran 1^{st} (R) \land x \in ran 1^{st} (R))) \to z 2^{nd} (R) x \in ran 1^{st} (R)$
63	62	anass1rs	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land x \in ran 1^{st} (R)) \land z \in ran 1^{st} (R)) \to z 2^{nd} (R) x \in ran 1^{st} (R)$
64	63	adantlrr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to z 2^{nd} (R) x \in ran 1^{st} (R)$
65		eqid	$⊢ 2^{nd} (S) = 2^{nd} (S)$
66	4 5 59 65	rngohommul	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (z \in ran 1^{st} (R) \land x \in ran 1^{st} (R))) \to F (z 2^{nd} (R) x) = F (z) 2^{nd} (S) F (x)$
67	66	anass1rs	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land x \in ran 1^{st} (R)) \land z \in ran 1^{st} (R)) \to F (z 2^{nd} (R) x) = F (z) 2^{nd} (S) F (x)$
68	67	adantlrr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to F (z 2^{nd} (R) x) = F (z) 2^{nd} (S) F (x)$
69		oveq2	$⊢ F (x) = Z \to F (z) 2^{nd} (S) F (x) = F (z) 2^{nd} (S) Z$
70	69	adantl	$⊢ (x \in ran 1^{st} (R) \land F (x) = Z) \to F (z) 2^{nd} (S) F (x) = F (z) 2^{nd} (S) Z$
71	70	ad2antlr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to F (z) 2^{nd} (S) F (x) = F (z) 2^{nd} (S) Z$
72	4 5 1 6	rngohomcl	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land z \in ran 1^{st} (R)) \to F (z) \in ran G$
73	2 6 1 65	rngorz	$⊢ (S \in RingOps \land F (z) \in ran G) \to F (z) 2^{nd} (S) Z = Z$
74	73	3ad2antl2	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land F (z) \in ran G) \to F (z) 2^{nd} (S) Z = Z$
75	72 74	syldan	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land z \in ran 1^{st} (R)) \to F (z) 2^{nd} (S) Z = Z$
76	75	adantlr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to F (z) 2^{nd} (S) Z = Z$
77	68 71 76	3eqtrd	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to F (z 2^{nd} (R) x) = Z$
78		fvex	$⊢ F (z 2^{nd} (R) x) \in V$
79	78	elsn	$⊢ F (z 2^{nd} (R) x) \in \{Z\} \leftrightarrow F (z 2^{nd} (R) x) = Z$
80	77 79	sylibr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to F (z 2^{nd} (R) x) \in \{Z\}$
81		elpreima	$⊢ F Fn ran 1^{st} (R) \to (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \leftrightarrow (z 2^{nd} (R) x \in ran 1^{st} (R) \land F (z 2^{nd} (R) x) \in \{Z\}))$
82	7 16 81	3syl	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \leftrightarrow (z 2^{nd} (R) x \in ran 1^{st} (R) \land F (z 2^{nd} (R) x) \in \{Z\}))$
83	82	ad2antrr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \leftrightarrow (z 2^{nd} (R) x \in ran 1^{st} (R) \land F (z 2^{nd} (R) x) \in \{Z\}))$
84	64 80 83	mpbir2and	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to z 2^{nd} (R) x \in F^{-1} [\{Z\}]$
85	4 59 5	rngocl	$⊢ (R \in RingOps \land x \in ran 1^{st} (R) \land z \in ran 1^{st} (R)) \to x 2^{nd} (R) z \in ran 1^{st} (R)$
86	85	3expb	$⊢ (R \in RingOps \land (x \in ran 1^{st} (R) \land z \in ran 1^{st} (R))) \to x 2^{nd} (R) z \in ran 1^{st} (R)$
87	86	3ad2antl1	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land z \in ran 1^{st} (R))) \to x 2^{nd} (R) z \in ran 1^{st} (R)$
88	87	anassrs	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land x \in ran 1^{st} (R)) \land z \in ran 1^{st} (R)) \to x 2^{nd} (R) z \in ran 1^{st} (R)$
89	88	adantlrr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to x 2^{nd} (R) z \in ran 1^{st} (R)$
90	4 5 59 65	rngohommul	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land z \in ran 1^{st} (R))) \to F (x 2^{nd} (R) z) = F (x) 2^{nd} (S) F (z)$
91	90	anassrs	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land x \in ran 1^{st} (R)) \land z \in ran 1^{st} (R)) \to F (x 2^{nd} (R) z) = F (x) 2^{nd} (S) F (z)$
92	91	adantlrr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to F (x 2^{nd} (R) z) = F (x) 2^{nd} (S) F (z)$
93		oveq1	$⊢ F (x) = Z \to F (x) 2^{nd} (S) F (z) = Z 2^{nd} (S) F (z)$
94	93	adantl	$⊢ (x \in ran 1^{st} (R) \land F (x) = Z) \to F (x) 2^{nd} (S) F (z) = Z 2^{nd} (S) F (z)$
95	94	ad2antlr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to F (x) 2^{nd} (S) F (z) = Z 2^{nd} (S) F (z)$
96	2 6 1 65	rngolz	$⊢ (S \in RingOps \land F (z) \in ran G) \to Z 2^{nd} (S) F (z) = Z$
97	96	3ad2antl2	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land F (z) \in ran G) \to Z 2^{nd} (S) F (z) = Z$
98	72 97	syldan	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land z \in ran 1^{st} (R)) \to Z 2^{nd} (S) F (z) = Z$
99	98	adantlr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to Z 2^{nd} (S) F (z) = Z$
100	92 95 99	3eqtrd	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to F (x 2^{nd} (R) z) = Z$
101		fvex	$⊢ F (x 2^{nd} (R) z) \in V$
102	101	elsn	$⊢ F (x 2^{nd} (R) z) \in \{Z\} \leftrightarrow F (x 2^{nd} (R) z) = Z$
103	100 102	sylibr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to F (x 2^{nd} (R) z) \in \{Z\}$
104		elpreima	$⊢ F Fn ran 1^{st} (R) \to (x 2^{nd} (R) z \in F^{-1} [\{Z\}] \leftrightarrow (x 2^{nd} (R) z \in ran 1^{st} (R) \land F (x 2^{nd} (R) z) \in \{Z\}))$
105	7 16 104	3syl	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (x 2^{nd} (R) z \in F^{-1} [\{Z\}] \leftrightarrow (x 2^{nd} (R) z \in ran 1^{st} (R) \land F (x 2^{nd} (R) z) \in \{Z\}))$
106	105	ad2antrr	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to (x 2^{nd} (R) z \in F^{-1} [\{Z\}] \leftrightarrow (x 2^{nd} (R) z \in ran 1^{st} (R) \land F (x 2^{nd} (R) z) \in \{Z\}))$
107	89 103 106	mpbir2and	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to x 2^{nd} (R) z \in F^{-1} [\{Z\}]$
108	84 107	jca	$⊢ (((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \land z \in ran 1^{st} (R)) \to (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}])$
109	108	ralrimiva	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land (x \in ran 1^{st} (R) \land F (x) = Z)) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}])$
110	109	ex	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to ((x \in ran 1^{st} (R) \land F (x) = Z) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}]))$
111	58 110	syl5bi	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to ((x \in ran 1^{st} (R) \land F (x) \in \{Z\}) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}]))$
112	49 111	sylbid	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (x \in F^{-1} [\{Z\}] \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}]))$
113	112	imp	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land x \in F^{-1} [\{Z\}]) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}])$
114	57 113	jca	$⊢ ((R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \land x \in F^{-1} [\{Z\}]) \to (\forall y \in F^{-1} [\{Z\}] x 1^{st} (R) y \in F^{-1} [\{Z\}] \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}]))$
115	114	ralrimiva	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to \forall x \in F^{-1} [\{Z\}] (\forall y \in F^{-1} [\{Z\}] x 1^{st} (R) y \in F^{-1} [\{Z\}] \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}]))$
116	4 59 5 9	isidl	$⊢ R \in RingOps \to (F^{-1} [\{Z\}] \in Idl (R) \leftrightarrow (F^{-1} [\{Z\}] \subseteq ran 1^{st} (R) \land GId (1^{st} (R)) \in F^{-1} [\{Z\}] \land \forall x \in F^{-1} [\{Z\}] (\forall y \in F^{-1} [\{Z\}] x 1^{st} (R) y \in F^{-1} [\{Z\}] \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}]))))$
117	116	3ad2ant1	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (F^{-1} [\{Z\}] \in Idl (R) \leftrightarrow (F^{-1} [\{Z\}] \subseteq ran 1^{st} (R) \land GId (1^{st} (R)) \in F^{-1} [\{Z\}] \land \forall x \in F^{-1} [\{Z\}] (\forall y \in F^{-1} [\{Z\}] x 1^{st} (R) y \in F^{-1} [\{Z\}] \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in F^{-1} [\{Z\}] \land x 2^{nd} (R) z \in F^{-1} [\{Z\}]))))$
118	8 19 115 117	mpbir3and	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to F^{-1} [\{Z\}] \in Idl (R)$

Metamath Proof Explorer

Theorem keridl

Proof