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

Metamath Proof Explorer

Theorem pridl

Description: The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypothesis pridl.1 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
Assertion pridl ( ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐵 ∈ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) ) → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 pridl.1 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
2 eqid ⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 )
3 eqid ⊢ ran ( 1st ‘ 𝑅 ) = ran ( 1st ‘ 𝑅 )
4 2 1 3 ispridl ⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ ran ( 1st ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) )
5 df-3an ⊢ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ ran ( 1st ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ↔ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ ran ( 1st ‘ 𝑅 ) ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) )
6 4 5 bitrdi ⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ ran ( 1st ‘ 𝑅 ) ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) )
7 6 simplbda ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) )
8 raleq ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
9 sseq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ⊆ 𝑃 ↔ 𝐴 ⊆ 𝑃 ) )
10 9 orbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ↔ ( 𝐴 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) )
11 8 10 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) )
12 raleq ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
13 12 ralbidv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
14 sseq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ⊆ 𝑃 ↔ 𝐵 ⊆ 𝑃 ) )
15 14 orbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ↔ ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) )
16 13 15 imbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) ) )
17 11 16 rspc2v ⊢ ( ( 𝐴 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐵 ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) ) )
18 7 17 syl5com ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → ( ( 𝐴 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐵 ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) ) )
19 18 expd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → ( 𝐴 ∈ ( Idl ‘ 𝑅 ) → ( 𝐵 ∈ ( Idl ‘ 𝑅 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) ) ) )
20 19 3imp2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐵 ∈ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) ) → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) )