Theorem 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}\left(S\right)$$
	keridl.2	$$⊢Z=\mathrm{GId}\left(G\right)$$
Assertion	keridl	Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( `' F " { Z } ) e. ( Idl ` R ) ) with typecode |-

Proof

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