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={\mathrm{Base}}_R$$
	isprmidlc.2	$$⊢\underset{\dot{}}{·}={\cdot }_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={\mathrm{Base}}_R$$
2		isprmidlc.2	$$⊢\underset{\dot{}}{·}={\cdot }_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	$$⊢\left(a=I\wedge b=J\right)\to a\underset{\dot{}}{·}b=I\underset{\dot{}}{·}J$$
11	10	eleq1d	$$⊢\left(a=I\wedge b=J\right)\to \left(a\underset{\dot{}}{·}b\in P\leftrightarrow I\underset{\dot{}}{·}J\in P\right)$$
12		simpl	$$⊢\left(a=I\wedge b=J\right)\to a=I$$
13	12	eleq1d	$$⊢\left(a=I\wedge b=J\right)\to \left(a\in P\leftrightarrow I\in P\right)$$
14		simpr	$$⊢\left(a=I\wedge b=J\right)\to b=J$$
15	14	eleq1d	$$⊢\left(a=I\wedge b=J\right)\to \left(b\in P\leftrightarrow J\in P\right)$$
16	13 15	orbi12d	$$⊢\left(a=I\wedge b=J\right)\to \left(\left(a\in P\vee b\in P\right)\leftrightarrow \left(I\in P\vee J\in P\right)\right)$$
17	11 16	imbi12d	$$⊢\left(a=I\wedge b=J\right)\to \left(\left(a\underset{\dot{}}{·}b\in P\to \left(a\in P\vee b\in P\right)\right)\leftrightarrow \left(I\underset{\dot{}}{·}J\in P\to \left(I\in P\vee J\in P\right)\right)\right)$$
18	17	rspc2gv	$$⊢\left(I\in B\wedge J\in B\right)\to \left(\forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in P\to \left(a\in P\vee b\in P\right)\right)\to \left(I\underset{\dot{}}{·}J\in P\to \left(I\in P\vee J\in P\right)\right)\right)$$
19	18	imp31	$$⊢\left(\left(\left(I\in B\wedge J\in B\right)\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in P\to \left(a\in P\vee b\in P\right)\right)\right)\wedge I\underset{\dot{}}{·}J\in P\right)\to \left(I\in P\vee J\in P\right)$$
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 |-