pzriprnglem8

Description: Lemma 8 for pzriprng : I resp. J is a two-sided ideal of the non-unital ring R . (Contributed by AV, 21-Mar-2025)

	Ref	Expression
Hypotheses	pzriprng.r	$⊢ R = ℤ_{ring} \times_{𝑠} ℤ_{ring}$
	pzriprng.i	$⊢ I = ℤ \times \{0\}$
	pzriprng.j	$⊢ J = R ↾_{𝑠} I$
Assertion	pzriprnglem8	$⊢ I \in 2Ideal (R)$

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	$⊢ R = ℤ_{ring} \times_{𝑠} ℤ_{ring}$
2		pzriprng.i	$⊢ I = ℤ \times \{0\}$
3		pzriprng.j	$⊢ J = R ↾_{𝑠} I$
4	1	pzriprnglem2	$⊢ {Base}_{R} = ℤ \times ℤ$
5	4	eleq2i	$⊢ x \in {Base}_{R} \leftrightarrow x \in (ℤ \times ℤ)$
6		elxp2	$⊢ x \in (ℤ \times ℤ) \leftrightarrow \exists a \in ℤ \exists b \in ℤ x = ⟨a, b⟩$
7	5 6	bitri	$⊢ x \in {Base}_{R} \leftrightarrow \exists a \in ℤ \exists b \in ℤ x = ⟨a, b⟩$
8	1 2	pzriprnglem3	$⊢ y \in I \leftrightarrow \exists c \in ℤ y = ⟨c, 0⟩$
9		simpll	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to a \in ℤ$
10		simpr	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to c \in ℤ$
11	9 10	zmulcld	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to a c \in ℤ$
12		zcn	$⊢ b \in ℤ \to b \in ℂ$
13	12	adantl	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℂ$
14	13	adantr	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to b \in ℂ$
15	14	mul01d	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to b \cdot 0 = 0$
16		ovex	$⊢ b \cdot 0 \in V$
17	16	elsn	$⊢ b \cdot 0 \in \{0\} \leftrightarrow b \cdot 0 = 0$
18	15 17	sylibr	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to b \cdot 0 \in \{0\}$
19	11 18	opelxpd	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to ⟨a c, b \cdot 0⟩ \in (ℤ \times \{0\})$
20	10 9	zmulcld	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to c a \in ℤ$
21	14	mul02d	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to 0 \cdot b = 0$
22		ovex	$⊢ 0 \cdot b \in V$
23	22	elsn	$⊢ 0 \cdot b \in \{0\} \leftrightarrow 0 \cdot b = 0$
24	21 23	sylibr	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to 0 \cdot b \in \{0\}$
25	20 24	opelxpd	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to ⟨c a, 0 \cdot b⟩ \in (ℤ \times \{0\})$
26		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
27		zringring	$⊢ ℤ_{ring} \in Ring$
28	27	a1i	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to ℤ_{ring} \in Ring$
29		simplr	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to b \in ℤ$
30		0zd	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to 0 \in ℤ$
31	29 30	zmulcld	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to b \cdot 0 \in ℤ$
32		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
33		eqid	$⊢ \cdot_{R} = \cdot_{R}$
34	1 26 26 28 28 9 29 10 30 11 31 32 32 33	xpsmul	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to ⟨a, b⟩ \cdot_{R} ⟨c, 0⟩ = ⟨a c, b \cdot 0⟩$
35	34	eleq1d	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to (⟨a, b⟩ \cdot_{R} ⟨c, 0⟩ \in (ℤ \times \{0\}) \leftrightarrow ⟨a c, b \cdot 0⟩ \in (ℤ \times \{0\}))$
36		simpl	$⊢ (c \in ℤ \land (a \in ℤ \land b \in ℤ)) \to c \in ℤ$
37		simprl	$⊢ (c \in ℤ \land (a \in ℤ \land b \in ℤ)) \to a \in ℤ$
38	36 37	zmulcld	$⊢ (c \in ℤ \land (a \in ℤ \land b \in ℤ)) \to c a \in ℤ$
39	38	ancoms	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to c a \in ℤ$
40		0zd	$⊢ (c \in ℤ \land (a \in ℤ \land b \in ℤ)) \to 0 \in ℤ$
41		simprr	$⊢ (c \in ℤ \land (a \in ℤ \land b \in ℤ)) \to b \in ℤ$
42	40 41	zmulcld	$⊢ (c \in ℤ \land (a \in ℤ \land b \in ℤ)) \to 0 \cdot b \in ℤ$
43	42	ancoms	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to 0 \cdot b \in ℤ$
44	1 26 26 28 28 10 30 9 29 39 43 32 32 33	xpsmul	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to ⟨c, 0⟩ \cdot_{R} ⟨a, b⟩ = ⟨c a, 0 \cdot b⟩$
45	44	eleq1d	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to (⟨c, 0⟩ \cdot_{R} ⟨a, b⟩ \in (ℤ \times \{0\}) \leftrightarrow ⟨c a, 0 \cdot b⟩ \in (ℤ \times \{0\}))$
46	35 45	anbi12d	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to ((⟨a, b⟩ \cdot_{R} ⟨c, 0⟩ \in (ℤ \times \{0\}) \land ⟨c, 0⟩ \cdot_{R} ⟨a, b⟩ \in (ℤ \times \{0\})) \leftrightarrow (⟨a c, b \cdot 0⟩ \in (ℤ \times \{0\}) \land ⟨c a, 0 \cdot b⟩ \in (ℤ \times \{0\})))$
47	19 25 46	mpbir2and	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to (⟨a, b⟩ \cdot_{R} ⟨c, 0⟩ \in (ℤ \times \{0\}) \land ⟨c, 0⟩ \cdot_{R} ⟨a, b⟩ \in (ℤ \times \{0\}))$
48	47	adantr	$⊢ (((a \in ℤ \land b \in ℤ) \land c \in ℤ) \land (y = ⟨c, 0⟩ \land x = ⟨a, b⟩)) \to (⟨a, b⟩ \cdot_{R} ⟨c, 0⟩ \in (ℤ \times \{0\}) \land ⟨c, 0⟩ \cdot_{R} ⟨a, b⟩ \in (ℤ \times \{0\}))$
49		oveq12	$⊢ (x = ⟨a, b⟩ \land y = ⟨c, 0⟩) \to x \cdot_{R} y = ⟨a, b⟩ \cdot_{R} ⟨c, 0⟩$
50	49	ancoms	$⊢ (y = ⟨c, 0⟩ \land x = ⟨a, b⟩) \to x \cdot_{R} y = ⟨a, b⟩ \cdot_{R} ⟨c, 0⟩$
51	50	adantl	$⊢ (((a \in ℤ \land b \in ℤ) \land c \in ℤ) \land (y = ⟨c, 0⟩ \land x = ⟨a, b⟩)) \to x \cdot_{R} y = ⟨a, b⟩ \cdot_{R} ⟨c, 0⟩$
52	2	a1i	$⊢ (((a \in ℤ \land b \in ℤ) \land c \in ℤ) \land (y = ⟨c, 0⟩ \land x = ⟨a, b⟩)) \to I = ℤ \times \{0\}$
53	51 52	eleq12d	$⊢ (((a \in ℤ \land b \in ℤ) \land c \in ℤ) \land (y = ⟨c, 0⟩ \land x = ⟨a, b⟩)) \to (x \cdot_{R} y \in I \leftrightarrow ⟨a, b⟩ \cdot_{R} ⟨c, 0⟩ \in (ℤ \times \{0\}))$
54		oveq12	$⊢ (y = ⟨c, 0⟩ \land x = ⟨a, b⟩) \to y \cdot_{R} x = ⟨c, 0⟩ \cdot_{R} ⟨a, b⟩$
55	54	adantl	$⊢ (((a \in ℤ \land b \in ℤ) \land c \in ℤ) \land (y = ⟨c, 0⟩ \land x = ⟨a, b⟩)) \to y \cdot_{R} x = ⟨c, 0⟩ \cdot_{R} ⟨a, b⟩$
56	55 52	eleq12d	$⊢ (((a \in ℤ \land b \in ℤ) \land c \in ℤ) \land (y = ⟨c, 0⟩ \land x = ⟨a, b⟩)) \to (y \cdot_{R} x \in I \leftrightarrow ⟨c, 0⟩ \cdot_{R} ⟨a, b⟩ \in (ℤ \times \{0\}))$
57	53 56	anbi12d	$⊢ (((a \in ℤ \land b \in ℤ) \land c \in ℤ) \land (y = ⟨c, 0⟩ \land x = ⟨a, b⟩)) \to ((x \cdot_{R} y \in I \land y \cdot_{R} x \in I) \leftrightarrow (⟨a, b⟩ \cdot_{R} ⟨c, 0⟩ \in (ℤ \times \{0\}) \land ⟨c, 0⟩ \cdot_{R} ⟨a, b⟩ \in (ℤ \times \{0\})))$
58	48 57	mpbird	$⊢ (((a \in ℤ \land b \in ℤ) \land c \in ℤ) \land (y = ⟨c, 0⟩ \land x = ⟨a, b⟩)) \to (x \cdot_{R} y \in I \land y \cdot_{R} x \in I)$
59	58	exp32	$⊢ ((a \in ℤ \land b \in ℤ) \land c \in ℤ) \to (y = ⟨c, 0⟩ \to (x = ⟨a, b⟩ \to (x \cdot_{R} y \in I \land y \cdot_{R} x \in I)))$
60	59	rexlimdva	$⊢ (a \in ℤ \land b \in ℤ) \to (\exists c \in ℤ y = ⟨c, 0⟩ \to (x = ⟨a, b⟩ \to (x \cdot_{R} y \in I \land y \cdot_{R} x \in I)))$
61	60	com23	$⊢ (a \in ℤ \land b \in ℤ) \to (x = ⟨a, b⟩ \to (\exists c \in ℤ y = ⟨c, 0⟩ \to (x \cdot_{R} y \in I \land y \cdot_{R} x \in I)))$
62	61	rexlimivv	$⊢ \exists a \in ℤ \exists b \in ℤ x = ⟨a, b⟩ \to (\exists c \in ℤ y = ⟨c, 0⟩ \to (x \cdot_{R} y \in I \land y \cdot_{R} x \in I))$
63	62	imp	$⊢ (\exists a \in ℤ \exists b \in ℤ x = ⟨a, b⟩ \land \exists c \in ℤ y = ⟨c, 0⟩) \to (x \cdot_{R} y \in I \land y \cdot_{R} x \in I)$
64	7 8 63	syl2anb	$⊢ (x \in {Base}_{R} \land y \in I) \to (x \cdot_{R} y \in I \land y \cdot_{R} x \in I)$
65	64	rgen2	$⊢ \forall x \in {Base}_{R} \forall y \in I (x \cdot_{R} y \in I \land y \cdot_{R} x \in I)$
66	1	pzriprnglem1	$⊢ R \in Rng$
67	1 2	pzriprnglem4	$⊢ I \in SubGrp (R)$
68		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
69		eqid	$⊢ {Base}_{R} = {Base}_{R}$
70	68 69 33	df2idl2rng	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (I \in 2Ideal (R) \leftrightarrow \forall x \in {Base}_{R} \forall y \in I (x \cdot_{R} y \in I \land y \cdot_{R} x \in I))$
71	66 67 70	mp2an	$⊢ I \in 2Ideal (R) \leftrightarrow \forall x \in {Base}_{R} \forall y \in I (x \cdot_{R} y \in I \land y \cdot_{R} x \in I)$
72	65 71	mpbir	$⊢ I \in 2Ideal (R)$

Metamath Proof Explorer

Theorem pzriprnglem8

Proof