keridl

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

	Ref	Expression
Hypotheses	keridl.1	⊢ 𝐺 = ( 1^st ‘ 𝑆 )
	keridl.2	⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion	keridl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( ^◡ 𝐹 “ { 𝑍 } ) ∈ ( Idl ‘ 𝑅 ) )

Proof

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

Metamath Proof Explorer

Theorem keridl

Proof