This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ispridl2.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
ispridl2.3 ⊢ 𝑋 = ran 𝐺
Assertion ispridl2 ( ( 𝑅 ∈ RingOps ∧ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) → 𝑃 ∈ ( PrIdl ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 ispridl2.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ispridl2.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ispridl2.3 ⊢ 𝑋 = ran 𝐺
4 1 3 idlss ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑟 ∈ ( Idl ‘ 𝑅 ) ) → 𝑟 ⊆ 𝑋 )
5 ssralv ⊢ ( 𝑟 ⊆ 𝑋 → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
6 4 5 syl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑟 ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
7 6 adantrr ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑠 ∈ ( Idl ‘ 𝑅 ) ) ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
8 1 3 idlss ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑠 ∈ ( Idl ‘ 𝑅 ) ) → 𝑠 ⊆ 𝑋 )
9 ssralv ⊢ ( 𝑠 ⊆ 𝑋 → ( ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
10 9 ralimdv ⊢ ( 𝑠 ⊆ 𝑋 → ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
11 8 10 syl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑠 ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
12 11 adantrl ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑠 ∈ ( Idl ‘ 𝑅 ) ) ) → ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
13 7 12 syld ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑠 ∈ ( Idl ‘ 𝑅 ) ) ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
14 13 adantlr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑟 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑠 ∈ ( Idl ‘ 𝑅 ) ) ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
15 r19.26-2 ⊢ ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ∧ ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ↔ ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ∧ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
16 pm3.35 ⊢ ( ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ∧ ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) )
17 16 2ralimi ⊢ ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ∧ ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) → ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) )
18 2ralor ⊢ ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ↔ ( ∀ 𝑎 ∈ 𝑟 𝑎 ∈ 𝑃 ∨ ∀ 𝑏 ∈ 𝑠 𝑏 ∈ 𝑃 ) )
19 dfss3 ⊢ ( 𝑟 ⊆ 𝑃 ↔ ∀ 𝑎 ∈ 𝑟 𝑎 ∈ 𝑃 )
20 dfss3 ⊢ ( 𝑠 ⊆ 𝑃 ↔ ∀ 𝑏 ∈ 𝑠 𝑏 ∈ 𝑃 )
21 19 20 orbi12i ⊢ ( ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ↔ ( ∀ 𝑎 ∈ 𝑟 𝑎 ∈ 𝑃 ∨ ∀ 𝑏 ∈ 𝑠 𝑏 ∈ 𝑃 ) )
22 18 21 sylbb2 ⊢ ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) )
23 17 22 syl ⊢ ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ∧ ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) )
24 15 23 sylbir ⊢ ( ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ∧ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) )
25 24 expcom ⊢ ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) )
26 14 25 syl6 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑟 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑠 ∈ ( Idl ‘ 𝑅 ) ) ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) )
27 26 ralrimdvva ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) )
28 27 ex ⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( Idl ‘ 𝑅 ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) ) )
29 28 adantrd ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) → ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) ) )
30 29 imdistand ⊢ ( 𝑅 ∈ RingOps → ( ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) → ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) ) )
31 df-3an ⊢ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ↔ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
32 df-3an ⊢ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) ↔ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) )
33 30 31 32 3imtr4g ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) → ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) ) )
34 1 2 3 ispridl ⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) ) )
35 33 34 sylibrd ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) → 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) )
36 35 imp ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) → 𝑃 ∈ ( PrIdl ‘ 𝑅 ) )