rprmval

Description: The prime elements of a ring R . (Contributed by Thierry Arnoux, 1-Jul-2024)

	Ref	Expression
Hypotheses	rprmval.b	$⊢ B = {Base}_{R}$
	rprmval.u	$⊢ U = Unit (R)$
	rprmval.1	$⊢ \underset{˙}{0} = 0_{R}$
	rprmval.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rprmval.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
Assertion	rprmval	$⊢ R \in V \to RPrime (R) = \{p \in (B ∖ (U \cup \{\underset{˙}{0}\})) \| \forall x \in B \forall y \in B (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y))\}$

Proof

Step	Hyp	Ref	Expression
1		rprmval.b	$⊢ B = {Base}_{R}$
2		rprmval.u	$⊢ U = Unit (R)$
3		rprmval.1	$⊢ \underset{˙}{0} = 0_{R}$
4		rprmval.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		rprmval.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
6		df-rprm	$⊢ RPrime = (r \in V ⟼ ⦋ {Base}_{r} / b ⦌ \{p \in (b ∖ (Unit (r) \cup \{0_{r}\})) \| \forall x \in b \forall y \in b \underset{˙}{[} ∥_{r} (r) / d \underset{˙}{]} (p d (x \cdot_{r} y) \to (p d x \lor p d y))\})$
7		fvexd	$⊢ r = R \to {Base}_{r} \in V$
8		simpr	$⊢ (r = R \land b = {Base}_{r}) \to b = {Base}_{r}$
9		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
10	9	adantr	$⊢ (r = R \land b = {Base}_{r}) \to {Base}_{r} = {Base}_{R}$
11	8 10	eqtrd	$⊢ (r = R \land b = {Base}_{r}) \to b = {Base}_{R}$
12	11 1	eqtr4di	$⊢ (r = R \land b = {Base}_{r}) \to b = B$
13		fveq2	$⊢ r = R \to Unit (r) = Unit (R)$
14	13 2	eqtr4di	$⊢ r = R \to Unit (r) = U$
15		fveq2	$⊢ r = R \to 0_{r} = 0_{R}$
16	15 3	eqtr4di	$⊢ r = R \to 0_{r} = \underset{˙}{0}$
17	16	sneqd	$⊢ r = R \to \{0_{r}\} = \{\underset{˙}{0}\}$
18	14 17	uneq12d	$⊢ r = R \to Unit (r) \cup \{0_{r}\} = U \cup \{\underset{˙}{0}\}$
19	18	adantr	$⊢ (r = R \land b = {Base}_{r}) \to Unit (r) \cup \{0_{r}\} = U \cup \{\underset{˙}{0}\}$
20	12 19	difeq12d	$⊢ (r = R \land b = {Base}_{r}) \to b ∖ (Unit (r) \cup \{0_{r}\}) = B ∖ (U \cup \{\underset{˙}{0}\})$
21		fvexd	$⊢ (r = R \land b = {Base}_{r}) \to ∥_{r} (r) \in V$
22		eqidd	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to p = p$
23		simpr	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to d = ∥_{r} (r)$
24		fveq2	$⊢ r = R \to ∥_{r} (r) = ∥_{r} (R)$
25	24	ad2antrr	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to ∥_{r} (r) = ∥_{r} (R)$
26	23 25	eqtrd	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to d = ∥_{r} (R)$
27	26 5	eqtr4di	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to d = \underset{˙}{∥}$
28		fveq2	$⊢ r = R \to \cdot_{r} = \cdot_{R}$
29	28 4	eqtr4di	$⊢ r = R \to \cdot_{r} = \underset{˙}{\cdot}$
30	29	ad2antrr	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to \cdot_{r} = \underset{˙}{\cdot}$
31	30	oveqd	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to x \cdot_{r} y = x \underset{˙}{\cdot} y$
32	22 27 31	breq123d	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to (p d (x \cdot_{r} y) \leftrightarrow p \underset{˙}{∥} (x \underset{˙}{\cdot} y))$
33	27	breqd	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to (p d x \leftrightarrow p \underset{˙}{∥} x)$
34	27	breqd	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to (p d y \leftrightarrow p \underset{˙}{∥} y)$
35	33 34	orbi12d	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to ((p d x \lor p d y) \leftrightarrow (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y))$
36	32 35	imbi12d	$⊢ ((r = R \land b = {Base}_{r}) \land d = ∥_{r} (r)) \to ((p d (x \cdot_{r} y) \to (p d x \lor p d y)) \leftrightarrow (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y)))$
37	21 36	sbcied	$⊢ (r = R \land b = {Base}_{r}) \to (\underset{˙}{[} ∥_{r} (r) / d \underset{˙}{]} (p d (x \cdot_{r} y) \to (p d x \lor p d y)) \leftrightarrow (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y)))$
38	12 37	raleqbidv	$⊢ (r = R \land b = {Base}_{r}) \to (\forall y \in b \underset{˙}{[} ∥_{r} (r) / d \underset{˙}{]} (p d (x \cdot_{r} y) \to (p d x \lor p d y)) \leftrightarrow \forall y \in B (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y)))$
39	12 38	raleqbidv	$⊢ (r = R \land b = {Base}_{r}) \to (\forall x \in b \forall y \in b \underset{˙}{[} ∥_{r} (r) / d \underset{˙}{]} (p d (x \cdot_{r} y) \to (p d x \lor p d y)) \leftrightarrow \forall x \in B \forall y \in B (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y)))$
40	20 39	rabeqbidv	$⊢ (r = R \land b = {Base}_{r}) \to \{p \in (b ∖ (Unit (r) \cup \{0_{r}\})) \| \forall x \in b \forall y \in b \underset{˙}{[} ∥_{r} (r) / d \underset{˙}{]} (p d (x \cdot_{r} y) \to (p d x \lor p d y))\} = \{p \in (B ∖ (U \cup \{\underset{˙}{0}\})) \| \forall x \in B \forall y \in B (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y))\}$
41	7 40	csbied	$⊢ r = R \to ⦋ {Base}_{r} / b ⦌ \{p \in (b ∖ (Unit (r) \cup \{0_{r}\})) \| \forall x \in b \forall y \in b \underset{˙}{[} ∥_{r} (r) / d \underset{˙}{]} (p d (x \cdot_{r} y) \to (p d x \lor p d y))\} = \{p \in (B ∖ (U \cup \{\underset{˙}{0}\})) \| \forall x \in B \forall y \in B (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y))\}$
42		elex	$⊢ R \in V \to R \in V$
43	1	fvexi	$⊢ B \in V$
44	43	difexi	$⊢ B ∖ (U \cup \{\underset{˙}{0}\}) \in V$
45	44	rabex	$⊢ \{p \in (B ∖ (U \cup \{\underset{˙}{0}\})) \| \forall x \in B \forall y \in B (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y))\} \in V$
46	45	a1i	$⊢ R \in V \to \{p \in (B ∖ (U \cup \{\underset{˙}{0}\})) \| \forall x \in B \forall y \in B (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y))\} \in V$
47	6 41 42 46	fvmptd3	$⊢ R \in V \to RPrime (R) = \{p \in (B ∖ (U \cup \{\underset{˙}{0}\})) \| \forall x \in B \forall y \in B (p \underset{˙}{∥} (x \underset{˙}{\cdot} y) \to (p \underset{˙}{∥} x \lor p \underset{˙}{∥} y))\}$

Metamath Proof Explorer

Theorem rprmval

Proof