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 = 1 st ⁡ R
ispridl2.2 ⊢ H = 2 nd ⁡ R
ispridl2.3 ⊢ X = ran ⁡ G
Assertion ispridl2 ⊢ R ∈ RingOps ∧ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ X ∀ b ∈ X a H b ∈ P → a ∈ P ∨ b ∈ P → P ∈ PrIdl ⁡ R

Proof

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