Metamath Proof Explorer

Theorem prmidlprop

Description: Property of prime ideals. (Contributed by Thierry Arnoux, 6-Jun-2026)

Ref Expression
Hypotheses prmidlprop.1 
|- B = ( Base ` R )
prmidlprop.2 
|- .x. = ( .r ` R )
prmidlprop.3 
|- ( ph -> R e. CRing )
prmidlprop.4 
|- ( ph -> P e. ( PrmIdeal ` R ) )
prmidlprop.5 
|- ( ph -> X e. B )
prmidlprop.6 
|- ( ph -> Y e. B )
prmidlprop.7 
|- ( ph -> ( X .x. Y ) e. P )
Assertion prmidlprop 
|- ( ph -> ( X e. P \/ Y e. P ) )

Proof

Step Hyp Ref Expression
1 prmidlprop.1 
 |-  B = ( Base ` R )
2 prmidlprop.2 
 |-  .x. = ( .r ` R )
3 prmidlprop.3 
 |-  ( ph -> R e. CRing )
4 prmidlprop.4 
 |-  ( ph -> P e. ( PrmIdeal ` R ) )
5 prmidlprop.5 
 |-  ( ph -> X e. B )
6 prmidlprop.6 
 |-  ( ph -> Y e. B )
7 prmidlprop.7 
 |-  ( ph -> ( X .x. Y ) e. P )
8 oveq1 
 |-  ( a = X -> ( a .x. b ) = ( X .x. b ) )
9 8 eleq1d 
 |-  ( a = X -> ( ( a .x. b ) e. P <-> ( X .x. b ) e. P ) )
10 eleq1 
 |-  ( a = X -> ( a e. P <-> X e. P ) )
11 10 orbi1d 
 |-  ( a = X -> ( ( a e. P \/ b e. P ) <-> ( X e. P \/ b e. P ) ) )
12 9 11 imbi12d 
 |-  ( a = X -> ( ( ( a .x. b ) e. P -> ( a e. P \/ b e. P ) ) <-> ( ( X .x. b ) e. P -> ( X e. P \/ b e. P ) ) ) )
13 oveq2 
 |-  ( b = Y -> ( X .x. b ) = ( X .x. Y ) )
14 13 eleq1d 
 |-  ( b = Y -> ( ( X .x. b ) e. P <-> ( X .x. Y ) e. P ) )
15 eleq1 
 |-  ( b = Y -> ( b e. P <-> Y e. P ) )
16 15 orbi2d 
 |-  ( b = Y -> ( ( X e. P \/ b e. P ) <-> ( X e. P \/ Y e. P ) ) )
17 14 16 imbi12d 
 |-  ( b = Y -> ( ( ( X .x. b ) e. P -> ( X e. P \/ b e. P ) ) <-> ( ( X .x. Y ) e. P -> ( X e. P \/ Y e. P ) ) ) )
18 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 ) ) ) ) )
19 18 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 ) ) ) )
20 3 4 19 syl2anc 
 |-  ( ph -> ( 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 ) ) ) )
21 20 simp3d 
 |-  ( ph -> A. a e. B A. b e. B ( ( a .x. b ) e. P -> ( a e. P \/ b e. P ) ) )
22 12 17 21 5 6 rspc2dv 
 |-  ( ph -> ( ( X .x. Y ) e. P -> ( X e. P \/ Y e. P ) ) )
23 7 22 mpd 
 |-  ( ph -> ( X e. P \/ Y e. P ) )