Metamath Proof Explorer

Theorem ispridl2

Description: A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses ispridl2.1 ⊢G=1st⁡R
ispridl2.2 ⊢H=2nd⁡R
ispridl2.3 ⊢X=ran⁡G
Assertion ispridl2 ⊢R∈RingOps∧P∈Idl⁡R∧P≠X∧∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→P∈PrIdl⁡R

Proof

Step Hyp Ref Expression
1 ispridl2.1 ⊢G=1st⁡R
2 ispridl2.2 ⊢H=2nd⁡R
3 ispridl2.3 ⊢X=ran⁡G
4 1 3 idlss ⊢R∈RingOps∧r∈Idl⁡R→r⊆X
5 ssralv ⊢r⊆X→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→∀a∈r∀b∈XaHb∈P→a∈P∨b∈P
6 4 5 syl ⊢R∈RingOps∧r∈Idl⁡R→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→∀a∈r∀b∈XaHb∈P→a∈P∨b∈P
7 6 adantrr ⊢R∈RingOps∧r∈Idl⁡R∧s∈Idl⁡R→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→∀a∈r∀b∈XaHb∈P→a∈P∨b∈P
8 1 3 idlss ⊢R∈RingOps∧s∈Idl⁡R→s⊆X
9 ssralv ⊢s⊆X→∀b∈XaHb∈P→a∈P∨b∈P→∀b∈saHb∈P→a∈P∨b∈P
10 9 ralimdv ⊢s⊆X→∀a∈r∀b∈XaHb∈P→a∈P∨b∈P→∀a∈r∀b∈saHb∈P→a∈P∨b∈P
11 8 10 syl ⊢R∈RingOps∧s∈Idl⁡R→∀a∈r∀b∈XaHb∈P→a∈P∨b∈P→∀a∈r∀b∈saHb∈P→a∈P∨b∈P
12 11 adantrl ⊢R∈RingOps∧r∈Idl⁡R∧s∈Idl⁡R→∀a∈r∀b∈XaHb∈P→a∈P∨b∈P→∀a∈r∀b∈saHb∈P→a∈P∨b∈P
13 7 12 syld ⊢R∈RingOps∧r∈Idl⁡R∧s∈Idl⁡R→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→∀a∈r∀b∈saHb∈P→a∈P∨b∈P
14 13 adantlr ⊢R∈RingOps∧P∈Idl⁡R∧r∈Idl⁡R∧s∈Idl⁡R→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→∀a∈r∀b∈saHb∈P→a∈P∨b∈P
15 r19.26-2 ⊢∀a∈r∀b∈saHb∈P∧aHb∈P→a∈P∨b∈P↔∀a∈r∀b∈saHb∈P∧∀a∈r∀b∈saHb∈P→a∈P∨b∈P
16 pm3.35 ⊢aHb∈P∧aHb∈P→a∈P∨b∈P→a∈P∨b∈P
17 16 2ralimi ⊢∀a∈r∀b∈saHb∈P∧aHb∈P→a∈P∨b∈P→∀a∈r∀b∈sa∈P∨b∈P
18 2ralor ⊢∀a∈r∀b∈sa∈P∨b∈P↔∀a∈ra∈P∨∀b∈sb∈P
19 dfss3 ⊢r⊆P↔∀a∈ra∈P
20 dfss3 ⊢s⊆P↔∀b∈sb∈P
21 19 20 orbi12i ⊢r⊆P∨s⊆P↔∀a∈ra∈P∨∀b∈sb∈P
22 18 21 sylbb2 ⊢∀a∈r∀b∈sa∈P∨b∈P→r⊆P∨s⊆P
23 17 22 syl ⊢∀a∈r∀b∈saHb∈P∧aHb∈P→a∈P∨b∈P→r⊆P∨s⊆P
24 15 23 sylbir ⊢∀a∈r∀b∈saHb∈P∧∀a∈r∀b∈saHb∈P→a∈P∨b∈P→r⊆P∨s⊆P
25 24 expcom ⊢∀a∈r∀b∈saHb∈P→a∈P∨b∈P→∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P
26 14 25 syl6 ⊢R∈RingOps∧P∈Idl⁡R∧r∈Idl⁡R∧s∈Idl⁡R→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P
27 26 ralrimdvva ⊢R∈RingOps∧P∈Idl⁡R→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→∀r∈Idl⁡R∀s∈Idl⁡R∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P
28 27 ex ⊢R∈RingOps→P∈Idl⁡R→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→∀r∈Idl⁡R∀s∈Idl⁡R∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P
29 28 adantrd ⊢R∈RingOps→P∈Idl⁡R∧P≠X→∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→∀r∈Idl⁡R∀s∈Idl⁡R∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P
30 29 imdistand ⊢R∈RingOps→P∈Idl⁡R∧P≠X∧∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→P∈Idl⁡R∧P≠X∧∀r∈Idl⁡R∀s∈Idl⁡R∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P
31 df-3an ⊢P∈Idl⁡R∧P≠X∧∀a∈X∀b∈XaHb∈P→a∈P∨b∈P↔P∈Idl⁡R∧P≠X∧∀a∈X∀b∈XaHb∈P→a∈P∨b∈P
32 df-3an ⊢P∈Idl⁡R∧P≠X∧∀r∈Idl⁡R∀s∈Idl⁡R∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P↔P∈Idl⁡R∧P≠X∧∀r∈Idl⁡R∀s∈Idl⁡R∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P
33 30 31 32 3imtr4g ⊢R∈RingOps→P∈Idl⁡R∧P≠X∧∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→P∈Idl⁡R∧P≠X∧∀r∈Idl⁡R∀s∈Idl⁡R∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P
34 1 2 3 ispridl ⊢R∈RingOps→P∈PrIdl⁡R↔P∈Idl⁡R∧P≠X∧∀r∈Idl⁡R∀s∈Idl⁡R∀a∈r∀b∈saHb∈P→r⊆P∨s⊆P
35 33 34 sylibrd ⊢R∈RingOps→P∈Idl⁡R∧P≠X∧∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→P∈PrIdl⁡R
36 35 imp ⊢R∈RingOps∧P∈Idl⁡R∧P≠X∧∀a∈X∀b∈XaHb∈P→a∈P∨b∈P→P∈PrIdl⁡R