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 · ˙ = 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 = Base R
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 = I b = J a · ˙ b = I · ˙ J
11 10 eleq1d a = I b = J a · ˙ b P I · ˙ J P
12 simpl a = I b = J a = I
13 12 eleq1d a = I b = J a P I P
14 simpr a = I b = J b = J
15 14 eleq1d a = I b = J b P J P
16 13 15 orbi12d a = I b = J a P b P I P J P
17 11 16 imbi12d a = I b = J a · ˙ b P a P b P I · ˙ J P I P J P
18 17 rspc2gv I B J B a B b B a · ˙ b P a P b P I · ˙ J P I P J P
19 18 imp31 I B J B a B b B a · ˙ b P a P b P I · ˙ J P I P J P
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 |-