pzriprnglem5

Description: Lemma 5 for pzriprng : I is a subring of the non-unital ring R . (Contributed by AV, 18-Mar-2025)

	Ref	Expression
Hypotheses	pzriprng.r	$⊢ R = ℤ_{ring} \times_{𝑠} ℤ_{ring}$
	pzriprng.i	$⊢ I = ℤ \times \{0\}$
Assertion	pzriprnglem5	Could not format assertion : No typesetting found for \|- I e. ( SubRng ` R ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	$⊢ R = ℤ_{ring} \times_{𝑠} ℤ_{ring}$
2		pzriprng.i	$⊢ I = ℤ \times \{0\}$
3	1 2	pzriprnglem4	$⊢ I \in SubGrp (R)$
4	1 2	pzriprnglem3	$⊢ x \in I \leftrightarrow \exists a \in ℤ x = ⟨a, 0⟩$
5	1 2	pzriprnglem3	$⊢ y \in I \leftrightarrow \exists b \in ℤ y = ⟨b, 0⟩$
6		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
7		zringring	$⊢ ℤ_{ring} \in Ring$
8	7	a1i	$⊢ (a \in ℤ \land b \in ℤ) \to ℤ_{ring} \in Ring$
9		simpl	$⊢ (a \in ℤ \land b \in ℤ) \to a \in ℤ$
10		0zd	$⊢ (a \in ℤ \land b \in ℤ) \to 0 \in ℤ$
11		simpr	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℤ$
12		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
13	12	eqcomi	$⊢ \cdot_{ℤ_{ring}} = \times$
14	13	oveqi	$⊢ a \cdot_{ℤ_{ring}} b = a b$
15		zmulcl	$⊢ (a \in ℤ \land b \in ℤ) \to a b \in ℤ$
16	14 15	eqeltrid	$⊢ (a \in ℤ \land b \in ℤ) \to a \cdot_{ℤ_{ring}} b \in ℤ$
17	13	oveqi	$⊢ 0 \cdot_{ℤ_{ring}} 0 = 0 \cdot 0$
18		0cn	$⊢ 0 \in ℂ$
19	18	mul02i	$⊢ 0 \cdot 0 = 0$
20	17 19	eqtri	$⊢ 0 \cdot_{ℤ_{ring}} 0 = 0$
21		0z	$⊢ 0 \in ℤ$
22	20 21	eqeltri	$⊢ 0 \cdot_{ℤ_{ring}} 0 \in ℤ$
23	22	a1i	$⊢ (a \in ℤ \land b \in ℤ) \to 0 \cdot_{ℤ_{ring}} 0 \in ℤ$
24		eqid	$⊢ \cdot_{ℤ_{ring}} = \cdot_{ℤ_{ring}}$
25		eqid	$⊢ \cdot_{R} = \cdot_{R}$
26	1 6 6 8 8 9 10 11 10 16 23 24 24 25	xpsmul	$⊢ (a \in ℤ \land b \in ℤ) \to ⟨a, 0⟩ \cdot_{R} ⟨b, 0⟩ = ⟨a \cdot_{ℤ_{ring}} b, 0 \cdot_{ℤ_{ring}} 0⟩$
27		c0ex	$⊢ 0 \in V$
28	27	snid	$⊢ 0 \in \{0\}$
29	28	a1i	$⊢ (a \in ℤ \land b \in ℤ) \to 0 \in \{0\}$
30	20 29	eqeltrid	$⊢ (a \in ℤ \land b \in ℤ) \to 0 \cdot_{ℤ_{ring}} 0 \in \{0\}$
31	16 30	opelxpd	$⊢ (a \in ℤ \land b \in ℤ) \to ⟨a \cdot_{ℤ_{ring}} b, 0 \cdot_{ℤ_{ring}} 0⟩ \in (ℤ \times \{0\})$
32	26 31	eqeltrd	$⊢ (a \in ℤ \land b \in ℤ) \to ⟨a, 0⟩ \cdot_{R} ⟨b, 0⟩ \in (ℤ \times \{0\})$
33	32	adantr	$⊢ ((a \in ℤ \land b \in ℤ) \land (y = ⟨b, 0⟩ \land x = ⟨a, 0⟩)) \to ⟨a, 0⟩ \cdot_{R} ⟨b, 0⟩ \in (ℤ \times \{0\})$
34		oveq12	$⊢ (x = ⟨a, 0⟩ \land y = ⟨b, 0⟩) \to x \cdot_{R} y = ⟨a, 0⟩ \cdot_{R} ⟨b, 0⟩$
35	34	ancoms	$⊢ (y = ⟨b, 0⟩ \land x = ⟨a, 0⟩) \to x \cdot_{R} y = ⟨a, 0⟩ \cdot_{R} ⟨b, 0⟩$
36	35	adantl	$⊢ ((a \in ℤ \land b \in ℤ) \land (y = ⟨b, 0⟩ \land x = ⟨a, 0⟩)) \to x \cdot_{R} y = ⟨a, 0⟩ \cdot_{R} ⟨b, 0⟩$
37	2	a1i	$⊢ ((a \in ℤ \land b \in ℤ) \land (y = ⟨b, 0⟩ \land x = ⟨a, 0⟩)) \to I = ℤ \times \{0\}$
38	33 36 37	3eltr4d	$⊢ ((a \in ℤ \land b \in ℤ) \land (y = ⟨b, 0⟩ \land x = ⟨a, 0⟩)) \to x \cdot_{R} y \in I$
39	38	exp32	$⊢ (a \in ℤ \land b \in ℤ) \to (y = ⟨b, 0⟩ \to (x = ⟨a, 0⟩ \to x \cdot_{R} y \in I))$
40	39	rexlimdva	$⊢ a \in ℤ \to (\exists b \in ℤ y = ⟨b, 0⟩ \to (x = ⟨a, 0⟩ \to x \cdot_{R} y \in I))$
41	40	com23	$⊢ a \in ℤ \to (x = ⟨a, 0⟩ \to (\exists b \in ℤ y = ⟨b, 0⟩ \to x \cdot_{R} y \in I))$
42	41	rexlimiv	$⊢ \exists a \in ℤ x = ⟨a, 0⟩ \to (\exists b \in ℤ y = ⟨b, 0⟩ \to x \cdot_{R} y \in I)$
43	42	imp	$⊢ (\exists a \in ℤ x = ⟨a, 0⟩ \land \exists b \in ℤ y = ⟨b, 0⟩) \to x \cdot_{R} y \in I$
44	4 5 43	syl2anb	$⊢ (x \in I \land y \in I) \to x \cdot_{R} y \in I$
45	44	rgen2	$⊢ \forall x \in I \forall y \in I x \cdot_{R} y \in I$
46	1	pzriprnglem1	$⊢ R \in Rng$
47		eqid	$⊢ {Base}_{R} = {Base}_{R}$
48	47 25	issubrng2	Could not format ( R e. Rng -> ( I e. ( SubRng ` R ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. I A. y e. I ( x ( .r ` R ) y ) e. I ) ) ) : No typesetting found for \|- ( R e. Rng -> ( I e. ( SubRng ` R ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. I A. y e. I ( x ( .r ` R ) y ) e. I ) ) ) with typecode \|-
49	46 48	ax-mp	Could not format ( I e. ( SubRng ` R ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. I A. y e. I ( x ( .r ` R ) y ) e. I ) ) : No typesetting found for \|- ( I e. ( SubRng ` R ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. I A. y e. I ( x ( .r ` R ) y ) e. I ) ) with typecode \|-
50	3 45 49	mpbir2an	Could not format I e. ( SubRng ` R ) : No typesetting found for \|- I e. ( SubRng ` R ) with typecode \|-

Metamath Proof Explorer

Theorem pzriprnglem5

Proof