Step |
Hyp |
Ref |
Expression |
1 |
|
rhmpreimaprmidl.p |
⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 ) |
2 |
|
rhmrcl1 |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring ) |
3 |
2
|
ad2antlr |
⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝑅 ∈ Ring ) |
4 |
|
rhmrcl2 |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring ) |
5 |
|
prmidlidl |
⊢ ( ( 𝑆 ∈ Ring ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) |
6 |
4 5
|
sylan |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) |
7 |
|
eqid |
⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 ) |
8 |
7
|
rhmpreimaidl |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) ) |
9 |
6 8
|
syldan |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) ) |
10 |
9
|
adantll |
⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) ) |
11 |
4
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝑆 ∈ Ring ) |
12 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
13 |
|
eqid |
⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) |
14 |
12 13
|
prmidlnr |
⊢ ( ( 𝑆 ∈ Ring ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝐽 ≠ ( Base ‘ 𝑆 ) ) |
15 |
4 14
|
sylan |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → 𝐽 ≠ ( Base ‘ 𝑆 ) ) |
16 |
|
eqid |
⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 ) |
17 |
12 16
|
pridln1 |
⊢ ( ( 𝑆 ∈ Ring ∧ 𝐽 ∈ ( LIdeal ‘ 𝑆 ) ∧ 𝐽 ≠ ( Base ‘ 𝑆 ) ) → ¬ ( 1r ‘ 𝑆 ) ∈ 𝐽 ) |
18 |
11 6 15 17
|
syl3anc |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ¬ ( 1r ‘ 𝑆 ) ∈ 𝐽 ) |
19 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
20 |
19 16
|
rhm1 |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) ) |
21 |
20
|
ad2antrr |
⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) ) |
22 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
23 |
22 12
|
rhmf |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ) |
24 |
23
|
ffnd |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 Fn ( Base ‘ 𝑅 ) ) |
25 |
24
|
ad2antrr |
⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → 𝐹 Fn ( Base ‘ 𝑅 ) ) |
26 |
22 19
|
ringidcl |
⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
27 |
2 26
|
syl |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
28 |
27
|
ad2antrr |
⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
29 |
|
simpr |
⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) |
30 |
28 29
|
eleqtrrd |
⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) |
31 |
|
elpreima |
⊢ ( 𝐹 Fn ( Base ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ↔ ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐽 ) ) ) |
32 |
31
|
biimpa |
⊢ ( ( 𝐹 Fn ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐽 ) ) |
33 |
25 30 32
|
syl2anc |
⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐽 ) ) |
34 |
33
|
simprd |
⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐽 ) |
35 |
21 34
|
eqeltrrd |
⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝑆 ) ∈ 𝐽 ) |
36 |
18 35
|
mtand |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ¬ ( ◡ 𝐹 “ 𝐽 ) = ( Base ‘ 𝑅 ) ) |
37 |
36
|
neqned |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ≠ ( Base ‘ 𝑅 ) ) |
38 |
37
|
adantll |
⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ≠ ( Base ‘ 𝑅 ) ) |
39 |
|
simp-5l |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑆 ∈ CRing ) |
40 |
|
simp-4r |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) |
41 |
|
simp-5r |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) |
42 |
41 23
|
syl |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ) |
43 |
|
simpllr |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) |
44 |
42 43
|
ffvelrnd |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ( Base ‘ 𝑆 ) ) |
45 |
|
simplr |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) ) |
46 |
42 45
|
ffvelrnd |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ( Base ‘ 𝑆 ) ) |
47 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
48 |
22 47 13
|
rhmmul |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ) |
49 |
41 43 45 48
|
syl3anc |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ) |
50 |
24
|
ad5antlr |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → 𝐹 Fn ( Base ‘ 𝑅 ) ) |
51 |
|
simpr |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) |
52 |
|
elpreima |
⊢ ( 𝐹 Fn ( Base ‘ 𝑅 ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) ∈ 𝐽 ) ) ) |
53 |
52
|
simplbda |
⊢ ( ( 𝐹 Fn ( Base ‘ 𝑅 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) ∈ 𝐽 ) |
54 |
50 51 53
|
syl2anc |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) ∈ 𝐽 ) |
55 |
49 54
|
eqeltrrd |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ∈ 𝐽 ) |
56 |
12 13
|
prmidlc |
⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) ∈ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ∨ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) ) |
57 |
39 40 44 46 55 56
|
syl23anc |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ∨ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) ) |
58 |
50
|
adantr |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) → 𝐹 Fn ( Base ‘ 𝑅 ) ) |
59 |
43
|
adantr |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) |
60 |
|
simpr |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) |
61 |
58 59 60
|
elpreimad |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ) → 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) |
62 |
61
|
ex |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 → 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) |
63 |
50
|
adantr |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → 𝐹 Fn ( Base ‘ 𝑅 ) ) |
64 |
|
simpllr |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) ) |
65 |
|
simpr |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) |
66 |
63 64 65
|
elpreimad |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) |
67 |
66
|
ex |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 → 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) |
68 |
62 67
|
orim12d |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐽 ∨ ( 𝐹 ‘ 𝑏 ) ∈ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) ) |
69 |
57 68
|
mpd |
⊢ ( ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) |
70 |
69
|
ex |
⊢ ( ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) ) |
71 |
70
|
anasss |
⊢ ( ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) ) |
72 |
71
|
ralrimivva |
⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ∀ 𝑎 ∈ ( Base ‘ 𝑅 ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) ) |
73 |
22 47
|
prmidl2 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ◡ 𝐹 “ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( ◡ 𝐹 “ 𝐽 ) ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑅 ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝐽 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ 𝐽 ) ∨ 𝑏 ∈ ( ◡ 𝐹 “ 𝐽 ) ) ) ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( PrmIdeal ‘ 𝑅 ) ) |
74 |
3 10 38 72 73
|
syl22anc |
⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ ( PrmIdeal ‘ 𝑅 ) ) |
75 |
74 1
|
eleqtrrdi |
⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝐽 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝐽 ) ∈ 𝑃 ) |