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=BaseR
isprmidlc.2 ·˙=R
Assertion prmidlc Could not format assertion : No typesetting found for |- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( I e. P \/ J e. P ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 isprmidlc.1 B=BaseR
2 isprmidlc.2 ·˙=R
3 simpr1 Could not format ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> I e. B ) : No typesetting found for |- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> I e. B ) with typecode |-
4 simpr2 Could not format ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> J e. B ) : No typesetting found for |- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> J e. B ) with typecode |-
5 1 2 isprmidlc Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
6 5 biimpa Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
7 6 simp3d Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
8 7 adantr Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
9 simpr3 Could not format ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( I .x. J ) e. P ) : No typesetting found for |- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( I .x. J ) e. P ) with typecode |-
10 oveq12 a=Ib=Ja·˙b=I·˙J
11 10 eleq1d a=Ib=Ja·˙bPI·˙JP
12 simpl a=Ib=Ja=I
13 12 eleq1d a=Ib=JaPIP
14 simpr a=Ib=Jb=J
15 14 eleq1d a=Ib=JbPJP
16 13 15 orbi12d a=Ib=JaPbPIPJP
17 11 16 imbi12d a=Ib=Ja·˙bPaPbPI·˙JPIPJP
18 17 rspc2gv IBJBaBbBa·˙bPaPbPI·˙JPIPJP
19 18 imp31 IBJBaBbBa·˙bPaPbPI·˙JPIPJP
20 3 4 8 9 19 syl1111anc Could not format ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( I e. P \/ J e. P ) ) : No typesetting found for |- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( I e. P \/ J e. P ) ) with typecode |-