Step |
Hyp |
Ref |
Expression |
1 |
|
isprmidlc.1 |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
isprmidlc.2 |
⊢ · = ( .r ‘ 𝑅 ) |
3 |
|
crngring |
⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring ) |
4 |
|
prmidlidl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) |
5 |
3 4
|
sylan |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) |
6 |
1 2
|
prmidlnr |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑃 ≠ 𝐵 ) |
7 |
3 6
|
sylan |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑃 ≠ 𝐵 ) |
8 |
3
|
ad4antr |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑅 ∈ Ring ) |
9 |
|
simp-4r |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) |
10 |
|
simpllr |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑥 ∈ 𝐵 ) |
11 |
10
|
snssd |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → { 𝑥 } ⊆ 𝐵 ) |
12 |
|
eqid |
⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 ) |
13 |
|
eqid |
⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 ) |
14 |
12 1 13
|
rspcl |
⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑥 } ⊆ 𝐵 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ ( LIdeal ‘ 𝑅 ) ) |
15 |
8 11 14
|
syl2anc |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ ( LIdeal ‘ 𝑅 ) ) |
16 |
|
simplr |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → 𝑦 ∈ 𝐵 ) |
17 |
16
|
snssd |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → { 𝑦 } ⊆ 𝐵 ) |
18 |
12 1 13
|
rspcl |
⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑦 } ⊆ 𝐵 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ∈ ( LIdeal ‘ 𝑅 ) ) |
19 |
8 17 18
|
syl2anc |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ∈ ( LIdeal ‘ 𝑅 ) ) |
20 |
15 19
|
jca |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ∈ ( LIdeal ‘ 𝑅 ) ) ) |
21 |
|
simpllr |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → 𝑟 = ( 𝑚 · 𝑥 ) ) |
22 |
|
simpr |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → 𝑠 = ( 𝑛 · 𝑦 ) ) |
23 |
21 22
|
oveq12d |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → ( 𝑟 · 𝑠 ) = ( ( 𝑚 · 𝑥 ) · ( 𝑛 · 𝑦 ) ) ) |
24 |
|
simp-10l |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → 𝑅 ∈ CRing ) |
25 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → 𝑚 ∈ 𝐵 ) |
26 |
10
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) → 𝑥 ∈ 𝐵 ) |
27 |
26
|
ad4antr |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → 𝑥 ∈ 𝐵 ) |
28 |
|
simplr |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → 𝑛 ∈ 𝐵 ) |
29 |
16
|
ad4antr |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) → 𝑦 ∈ 𝐵 ) |
30 |
29
|
ad2antrr |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → 𝑦 ∈ 𝐵 ) |
31 |
1 2
|
cringm4 |
⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑚 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑛 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑚 · 𝑥 ) · ( 𝑛 · 𝑦 ) ) = ( ( 𝑚 · 𝑛 ) · ( 𝑥 · 𝑦 ) ) ) |
32 |
24 25 27 28 30 31
|
syl122anc |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → ( ( 𝑚 · 𝑥 ) · ( 𝑛 · 𝑦 ) ) = ( ( 𝑚 · 𝑛 ) · ( 𝑥 · 𝑦 ) ) ) |
33 |
24 3
|
syl |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → 𝑅 ∈ Ring ) |
34 |
5
|
ad9antr |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) |
35 |
1 2
|
ringcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( 𝑚 · 𝑛 ) ∈ 𝐵 ) |
36 |
33 25 28 35
|
syl3anc |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → ( 𝑚 · 𝑛 ) ∈ 𝐵 ) |
37 |
|
simp-7r |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑃 ) |
38 |
13 1 2
|
lidlmcl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑚 · 𝑛 ) ∈ 𝐵 ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ) → ( ( 𝑚 · 𝑛 ) · ( 𝑥 · 𝑦 ) ) ∈ 𝑃 ) |
39 |
33 34 36 37 38
|
syl22anc |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → ( ( 𝑚 · 𝑛 ) · ( 𝑥 · 𝑦 ) ) ∈ 𝑃 ) |
40 |
32 39
|
eqeltrd |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → ( ( 𝑚 · 𝑥 ) · ( 𝑛 · 𝑦 ) ) ∈ 𝑃 ) |
41 |
23 40
|
eqeltrd |
⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑠 = ( 𝑛 · 𝑦 ) ) → ( 𝑟 · 𝑠 ) ∈ 𝑃 ) |
42 |
8
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) → 𝑅 ∈ Ring ) |
43 |
42
|
ad2antrr |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) → 𝑅 ∈ Ring ) |
44 |
|
simpllr |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) → 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) |
45 |
1 2 12
|
rspsnel |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ↔ ∃ 𝑛 ∈ 𝐵 𝑠 = ( 𝑛 · 𝑦 ) ) ) |
46 |
45
|
biimpa |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) → ∃ 𝑛 ∈ 𝐵 𝑠 = ( 𝑛 · 𝑦 ) ) |
47 |
43 29 44 46
|
syl21anc |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) → ∃ 𝑛 ∈ 𝐵 𝑠 = ( 𝑛 · 𝑦 ) ) |
48 |
41 47
|
r19.29a |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑟 = ( 𝑚 · 𝑥 ) ) → ( 𝑟 · 𝑠 ) ∈ 𝑃 ) |
49 |
|
simplr |
⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) → 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) |
50 |
1 2 12
|
rspsnel |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ↔ ∃ 𝑚 ∈ 𝐵 𝑟 = ( 𝑚 · 𝑥 ) ) ) |
51 |
50
|
biimpa |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ∃ 𝑚 ∈ 𝐵 𝑟 = ( 𝑚 · 𝑥 ) ) |
52 |
42 26 49 51
|
syl21anc |
⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) → ∃ 𝑚 ∈ 𝐵 𝑟 = ( 𝑚 · 𝑥 ) ) |
53 |
48 52
|
r19.29a |
⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) → ( 𝑟 · 𝑠 ) ∈ 𝑃 ) |
54 |
53
|
anasss |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∧ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) ) → ( 𝑟 · 𝑠 ) ∈ 𝑃 ) |
55 |
54
|
ralrimivva |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ∀ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∀ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ( 𝑟 · 𝑠 ) ∈ 𝑃 ) |
56 |
1 2
|
prmidl |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑟 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∀ 𝑠 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ( 𝑟 · 𝑠 ) ∈ 𝑃 ) → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ⊆ 𝑃 ∨ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ⊆ 𝑃 ) ) |
57 |
8 9 20 55 56
|
syl1111anc |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ⊆ 𝑃 ∨ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ⊆ 𝑃 ) ) |
58 |
1 12
|
rspsnid |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) |
59 |
3 58
|
sylan |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) |
60 |
59
|
adantr |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) |
61 |
|
ssel |
⊢ ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ⊆ 𝑃 → ( 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) → 𝑥 ∈ 𝑃 ) ) |
62 |
60 61
|
syl5com |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ⊆ 𝑃 → 𝑥 ∈ 𝑃 ) ) |
63 |
1 12
|
rspsnid |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) |
64 |
3 63
|
sylan |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) |
65 |
64
|
adantlr |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) |
66 |
|
ssel |
⊢ ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ⊆ 𝑃 → ( 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) → 𝑦 ∈ 𝑃 ) ) |
67 |
65 66
|
syl5com |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ⊆ 𝑃 → 𝑦 ∈ 𝑃 ) ) |
68 |
62 67
|
orim12d |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ⊆ 𝑃 ∨ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ⊆ 𝑃 ) → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) |
69 |
68
|
adantllr |
⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ⊆ 𝑃 ∨ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ⊆ 𝑃 ) → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) |
70 |
69
|
adantr |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ⊆ 𝑃 ∨ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ⊆ 𝑃 ) → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) |
71 |
57 70
|
mpd |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝑃 ) → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) |
72 |
71
|
ex |
⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) |
73 |
72
|
anasss |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) |
74 |
73
|
ralrimivva |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) |
75 |
5 7 74
|
3jca |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) |
76 |
|
3anass |
⊢ ( ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ↔ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) ) |
77 |
1 2
|
prmidl2 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) |
78 |
77
|
anasss |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) |
79 |
76 78
|
sylan2b |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) |
80 |
3 79
|
sylan |
⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) |
81 |
75 80
|
impbida |
⊢ ( 𝑅 ∈ CRing → ( 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑃 ≠ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃 ) ) ) ) ) |