Theorem rhmpreimaprmidl

Description: The preimage of a prime ideal by a ring homomorphism is a prime ideal. (Contributed by Thierry Arnoux, 29-Jun-2024)

	Ref	Expression
Hypothesis	rhmpreimaprmidl.p	No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
Assertion	rhmpreimaprmidl	Could not format assertion : No typesetting found for |- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. P ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rhmpreimaprmidl.p	Could not format P = ( PrmIdeal ` R ) : No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
2		rhmrcl1	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to R\in \mathrm{Ring}$$
3	2	ad2antlr	Could not format ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> R e. Ring ) with typecode |-
4		rhmrcl2	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to S\in \mathrm{Ring}$$
5		prmidlidl	Could not format ( ( S e. Ring /\ J e. ( PrmIdeal ` S ) ) -> J e. ( LIdeal ` S ) ) : No typesetting found for |- ( ( S e. Ring /\ J e. ( PrmIdeal ` S ) ) -> J e. ( LIdeal ` S ) ) with typecode |-
6	4 5	sylan	Could not format ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> J e. ( LIdeal ` S ) ) : No typesetting found for |- ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> J e. ( LIdeal ` S ) ) with typecode |-
7		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
8	7	rhmpreimaidl	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge J\in \mathrm{LIdeal}\left(S\right)\right)\to F^{-1}\left[J\right]\in \mathrm{LIdeal}\left(R\right)$$
9	6 8	syldan	Could not format ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. ( LIdeal ` R ) ) with typecode |-
10	9	adantll	Could not format ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. ( LIdeal ` R ) ) with typecode |-
11	4	adantr	Could not format ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> S e. Ring ) : No typesetting found for |- ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> S e. Ring ) with typecode |-
12		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
13		eqid	$$⊢{\cdot }_S={\cdot }_S$$
14	12 13	prmidlnr	Could not format ( ( S e. Ring /\ J e. ( PrmIdeal ` S ) ) -> J =/= ( Base ` S ) ) : No typesetting found for |- ( ( S e. Ring /\ J e. ( PrmIdeal ` S ) ) -> J =/= ( Base ` S ) ) with typecode |-
15	4 14	sylan	Could not format ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> J =/= ( Base ` S ) ) : No typesetting found for |- ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> J =/= ( Base ` S ) ) with typecode |-
16		eqid	$$⊢1_S=1_S$$
17	12 16	pridln1	$$⊢\left(S\in \mathrm{Ring}\wedge J\in \mathrm{LIdeal}\left(S\right)\wedge J\ne {\mathrm{Base}}_S\right)\to \neg 1_S\in J$$
18	11 6 15 17	syl3anc	Could not format ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> -. ( 1r ` S ) e. J ) : No typesetting found for |- ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> -. ( 1r ` S ) e. J ) with typecode |-
19		eqid	$$⊢1_R=1_R$$
20	19 16	rhm1	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\left(1_R\right)=1_S$$
21	20	ad2antrr	Could not format ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) ) : No typesetting found for |- ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) ) with typecode |-
22		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
23	22 12	rhmf	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
24	23	ffnd	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to FFn{\mathrm{Base}}_R$$
25	24	ad2antrr	Could not format ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> F Fn ( Base ` R ) ) : No typesetting found for |- ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> F Fn ( Base ` R ) ) with typecode |-
26	22 19	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
27	2 26	syl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to 1_R\in {\mathrm{Base}}_R$$
28	27	ad2antrr	Could not format ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) ) with typecode |-
29		simpr	Could not format ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( `' F " J ) = ( Base ` R ) ) : No typesetting found for |- ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( `' F " J ) = ( Base ` R ) ) with typecode |-
30	28 29	eleqtrrd	Could not format ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( 1r ` R ) e. ( `' F " J ) ) : No typesetting found for |- ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( 1r ` R ) e. ( `' F " J ) ) with typecode |-
31		elpreima	$$⊢FFn{\mathrm{Base}}_R\to \left(1_R\in F^{-1}\left[J\right]\leftrightarrow \left(1_R\in {\mathrm{Base}}_R\wedge F\left(1_R\right)\in J\right)\right)$$
32	31	biimpa	$$⊢\left(FFn{\mathrm{Base}}_R\wedge 1_R\in F^{-1}\left[J\right]\right)\to \left(1_R\in {\mathrm{Base}}_R\wedge F\left(1_R\right)\in J\right)$$
33	25 30 32	syl2anc	Could not format ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( ( 1r ` R ) e. ( Base ` R ) /\ ( F ` ( 1r ` R ) ) e. J ) ) : No typesetting found for |- ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( ( 1r ` R ) e. ( Base ` R ) /\ ( F ` ( 1r ` R ) ) e. J ) ) with typecode |-
34	33	simprd	Could not format ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( F ` ( 1r ` R ) ) e. J ) : No typesetting found for |- ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( F ` ( 1r ` R ) ) e. J ) with typecode |-
35	21 34	eqeltrrd	Could not format ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( 1r ` S ) e. J ) : No typesetting found for |- ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( 1r ` S ) e. J ) with typecode |-
36	18 35	mtand	Could not format ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> -. ( `' F " J ) = ( Base ` R ) ) : No typesetting found for |- ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> -. ( `' F " J ) = ( Base ` R ) ) with typecode |-
37	36	neqned	Could not format ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) =/= ( Base ` R ) ) : No typesetting found for |- ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) =/= ( Base ` R ) ) with typecode |-
38	37	adantll	Could not format ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) =/= ( Base ` R ) ) : No typesetting found for |- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) =/= ( Base ` R ) ) with typecode |-
39		simp-5l	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> S e. CRing ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> S e. CRing ) with typecode |-
40		simp-4r	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> J e. ( PrmIdeal ` S ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> J e. ( PrmIdeal ` S ) ) with typecode |-
41		simp-5r	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> F e. ( R RingHom S ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> F e. ( R RingHom S ) ) with typecode |-
42	41 23	syl	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> F : ( Base ` R ) --> ( Base ` S ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> F : ( Base ` R ) --> ( Base ` S ) ) with typecode |-
43		simpllr	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> a e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> a e. ( Base ` R ) ) with typecode |-
44	42 43	ffvelrnd	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` a ) e. ( Base ` S ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` a ) e. ( Base ` S ) ) with typecode |-
45		simplr	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> b e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> b e. ( Base ` R ) ) with typecode |-
46	42 45	ffvelrnd	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` b ) e. ( Base ` S ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` b ) e. ( Base ` S ) ) with typecode |-
47		eqid	$$⊢{\cdot }_R={\cdot }_R$$
48	22 47 13	rhmmul	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_R\right)\to F\left(a{\cdot }_{R}b\right)=F\left(a\right){\cdot }_{S}F\left(b\right)$$
49	41 43 45 48	syl3anc	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` ( a ( .r ` R ) b ) ) = ( ( F ` a ) ( .r ` S ) ( F ` b ) ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` ( a ( .r ` R ) b ) ) = ( ( F ` a ) ( .r ` S ) ( F ` b ) ) ) with typecode |-
50	24	ad5antlr	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> F Fn ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> F Fn ( Base ` R ) ) with typecode |-
51		simpr	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( a ( .r ` R ) b ) e. ( `' F " J ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( a ( .r ` R ) b ) e. ( `' F " J ) ) with typecode |-
52		elpreima	$$⊢FFn{\mathrm{Base}}_R\to \left(a{\cdot }_{R}b\in F^{-1}\left[J\right]\leftrightarrow \left(a{\cdot }_{R}b\in {\mathrm{Base}}_R\wedge F\left(a{\cdot }_{R}b\right)\in J\right)\right)$$
53	52	simplbda	$$⊢\left(FFn{\mathrm{Base}}_R\wedge a{\cdot }_{R}b\in F^{-1}\left[J\right]\right)\to F\left(a{\cdot }_{R}b\right)\in J$$
54	50 51 53	syl2anc	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` ( a ( .r ` R ) b ) ) e. J ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` ( a ( .r ` R ) b ) ) e. J ) with typecode |-
55	49 54	eqeltrrd	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` a ) ( .r ` S ) ( F ` b ) ) e. J ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` a ) ( .r ` S ) ( F ` b ) ) e. J ) with typecode |-
56	12 13	prmidlc	Could not format ( ( ( S e. CRing /\ J e. ( PrmIdeal ` S ) ) /\ ( ( F ` a ) e. ( Base ` S ) /\ ( F ` b ) e. ( Base ` S ) /\ ( ( F ` a ) ( .r ` S ) ( F ` b ) ) e. J ) ) -> ( ( F ` a ) e. J \/ ( F ` b ) e. J ) ) : No typesetting found for |- ( ( ( S e. CRing /\ J e. ( PrmIdeal ` S ) ) /\ ( ( F ` a ) e. ( Base ` S ) /\ ( F ` b ) e. ( Base ` S ) /\ ( ( F ` a ) ( .r ` S ) ( F ` b ) ) e. J ) ) -> ( ( F ` a ) e. J \/ ( F ` b ) e. J ) ) with typecode |-
57	39 40 44 46 55 56	syl23anc	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` a ) e. J \/ ( F ` b ) e. J ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` a ) e. J \/ ( F ` b ) e. J ) ) with typecode |-
58	50	adantr	Could not format ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> F Fn ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> F Fn ( Base ` R ) ) with typecode |-
59	43	adantr	Could not format ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> a e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> a e. ( Base ` R ) ) with typecode |-
60		simpr	Could not format ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> ( F ` a ) e. J ) : No typesetting found for |- ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> ( F ` a ) e. J ) with typecode |-
61	58 59 60	elpreimad	Could not format ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> a e. ( `' F " J ) ) : No typesetting found for |- ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> a e. ( `' F " J ) ) with typecode |-
62	61	ex	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` a ) e. J -> a e. ( `' F " J ) ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` a ) e. J -> a e. ( `' F " J ) ) ) with typecode |-
63	50	adantr	Could not format ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> F Fn ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> F Fn ( Base ` R ) ) with typecode |-
64		simpllr	Could not format ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> b e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> b e. ( Base ` R ) ) with typecode |-
65		simpr	Could not format ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> ( F ` b ) e. J ) : No typesetting found for |- ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> ( F ` b ) e. J ) with typecode |-
66	63 64 65	elpreimad	Could not format ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> b e. ( `' F " J ) ) : No typesetting found for |- ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> b e. ( `' F " J ) ) with typecode |-
67	66	ex	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` b ) e. J -> b e. ( `' F " J ) ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` b ) e. J -> b e. ( `' F " J ) ) ) with typecode |-
68	62 67	orim12d	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( ( F ` a ) e. J \/ ( F ` b ) e. J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( ( F ` a ) e. J \/ ( F ` b ) e. J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) with typecode |-
69	57 68	mpd	Could not format ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) : No typesetting found for |- ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) with typecode |-
70	69	ex	Could not format ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) -> ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) : No typesetting found for |- ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) -> ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) with typecode |-
71	70	anasss	Could not format ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) : No typesetting found for |- ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) with typecode |-
72	71	ralrimivva	Could not format ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> A. a e. ( Base ` R ) A. b e. ( Base ` R ) ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) : No typesetting found for |- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> A. a e. ( Base ` R ) A. b e. ( Base ` R ) ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) with typecode |-
73	22 47	prmidl2	Could not format ( ( ( R e. Ring /\ ( `' F " J ) e. ( LIdeal ` R ) ) /\ ( ( `' F " J ) =/= ( Base ` R ) /\ A. a e. ( Base ` R ) A. b e. ( Base ` R ) ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) ) -> ( `' F " J ) e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. Ring /\ ( `' F " J ) e. ( LIdeal ` R ) ) /\ ( ( `' F " J ) =/= ( Base ` R ) /\ A. a e. ( Base ` R ) A. b e. ( Base ` R ) ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) ) -> ( `' F " J ) e. ( PrmIdeal ` R ) ) with typecode |-
74	3 10 38 72 73	syl22anc	Could not format ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. ( PrmIdeal ` R ) ) with typecode |-
75	74 1	eleqtrrdi	Could not format ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. P ) : No typesetting found for |- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. P ) with typecode |-