Metamath Proof Explorer

Theorem prmidlc

Description: Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses isprmidlc.1 
|- B = ( Base ` R )
isprmidlc.2 
|- .x. = ( .r ` R )
Assertion prmidlc 
|- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( I e. P \/ J e. P ) )

Proof

Step Hyp Ref Expression
1 isprmidlc.1 
 |-  B = ( Base ` R )
2 isprmidlc.2 
 |-  .x. = ( .r ` R )
3 simpr1 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> I e. B )
4 simpr2 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> J e. B )
5 1 2 isprmidlc 
 |-  ( R e. CRing -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. P -> ( a e. P \/ b e. P ) ) ) ) )
6 5 biimpa 
 |-  ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. B A. b e. B ( ( a .x. b ) e. P -> ( a e. P \/ b e. P ) ) ) )
7 6 simp3d 
 |-  ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> A. a e. B A. b e. B ( ( a .x. b ) e. P -> ( a e. P \/ b e. P ) ) )
8 7 adantr 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> A. a e. B A. b e. B ( ( a .x. b ) e. P -> ( a e. P \/ b e. P ) ) )
9 simpr3 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( I .x. J ) e. P )
10 oveq12 
 |-  ( ( a = I /\ b = J ) -> ( a .x. b ) = ( I .x. J ) )
11 10 eleq1d 
 |-  ( ( a = I /\ b = J ) -> ( ( a .x. b ) e. P <-> ( I .x. J ) e. P ) )
12 simpl 
 |-  ( ( a = I /\ b = J ) -> a = I )
13 12 eleq1d 
 |-  ( ( a = I /\ b = J ) -> ( a e. P <-> I e. P ) )
14 simpr 
 |-  ( ( a = I /\ b = J ) -> b = J )
15 14 eleq1d 
 |-  ( ( a = I /\ b = J ) -> ( b e. P <-> J e. P ) )
16 13 15 orbi12d 
 |-  ( ( a = I /\ b = J ) -> ( ( a e. P \/ b e. P ) <-> ( I e. P \/ J e. P ) ) )
17 11 16 imbi12d 
 |-  ( ( a = I /\ b = J ) -> ( ( ( a .x. b ) e. P -> ( a e. P \/ b e. P ) ) <-> ( ( I .x. J ) e. P -> ( I e. P \/ J e. P ) ) ) )
18 17 rspc2gv 
 |-  ( ( I e. B /\ J e. B ) -> ( A. a e. B A. b e. B ( ( a .x. b ) e. P -> ( a e. P \/ b e. P ) ) -> ( ( I .x. J ) e. P -> ( I e. P \/ J e. P ) ) ) )
19 18 imp31 
 |-  ( ( ( ( I e. B /\ J e. B ) /\ A. a e. B A. b e. B ( ( a .x. b ) e. P -> ( a e. P \/ b e. P ) ) ) /\ ( I .x. J ) e. P ) -> ( I e. P \/ J e. P ) )
20 3 4 8 9 19 syl1111anc 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( I e. P \/ J e. P ) )