Theorem 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	⊢ 𝑅 = ( ℤring ×s ℤring )
	pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
Assertion	pzriprnglem5	⊢ 𝐼 ∈ ( SubRng ‘ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	⊢ 𝑅 = ( ℤring ×s ℤring )
2		pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
3	1 2	pzriprnglem4	⊢ 𝐼 ∈ ( SubGrp ‘ 𝑅 )
4	1 2	pzriprnglem3	⊢ ( 𝑥 ∈ 𝐼 ↔ ∃ 𝑎 ∈ ℤ 𝑥 = ⟨ 𝑎 , 0 ⟩ )
5	1 2	pzriprnglem3	⊢ ( 𝑦 ∈ 𝐼 ↔ ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 0 ⟩ )
6		zringbas	⊢ ℤ = ( Base ‘ ℤring )
7		zringring	⊢ ℤring ∈ Ring
8	7	a1i	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ℤring ∈ Ring )
9		simpl	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑎 ∈ ℤ )
10		0zd	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 0 ∈ ℤ )
11		simpr	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℤ )
12		zringmulr	⊢ · = ( .r ‘ ℤring )
13	12	eqcomi	⊢ ( .r ‘ ℤring ) = ·
14	13	oveqi	⊢ ( 𝑎 ( .r ‘ ℤring ) 𝑏 ) = ( 𝑎 · 𝑏 )
15		zmulcl	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
16	14 15	eqeltrid	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 ( .r ‘ ℤring ) 𝑏 ) ∈ ℤ )
17	13	oveqi	⊢ ( 0 ( .r ‘ ℤring ) 0 ) = ( 0 · 0 )
18		0cn	⊢ 0 ∈ ℂ
19	18	mul02i	⊢ ( 0 · 0 ) = 0
20	17 19	eqtri	⊢ ( 0 ( .r ‘ ℤring ) 0 ) = 0
21		0z	⊢ 0 ∈ ℤ
22	20 21	eqeltri	⊢ ( 0 ( .r ‘ ℤring ) 0 ) ∈ ℤ
23	22	a1i	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 0 ( .r ‘ ℤring ) 0 ) ∈ ℤ )
24		eqid	⊢ ( .r ‘ ℤring ) = ( .r ‘ ℤring )
25		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
26	1 6 6 8 8 9 10 11 10 16 23 24 24 25	xpsmul	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) = ⟨ ( 𝑎 ( .r ‘ ℤring ) 𝑏 ) , ( 0 ( .r ‘ ℤring ) 0 ) ⟩ )
27		c0ex	⊢ 0 ∈ V
28	27	snid	⊢ 0 ∈ { 0 }
29	28	a1i	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 0 ∈ { 0 } )
30	20 29	eqeltrid	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 0 ( .r ‘ ℤring ) 0 ) ∈ { 0 } )
31	16 30	opelxpd	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ⟨ ( 𝑎 ( .r ‘ ℤring ) 𝑏 ) , ( 0 ( .r ‘ ℤring ) 0 ) ⟩ ∈ ( ℤ × { 0 } ) )
32	26 31	eqeltrd	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) )
33	32	adantr	⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑏 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) ) → ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) )
34		oveq12	⊢ ( ( 𝑥 = ⟨ 𝑎 , 0 ⟩ ∧ 𝑦 = ⟨ 𝑏 , 0 ⟩ ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) )
35	34	ancoms	⊢ ( ( 𝑦 = ⟨ 𝑏 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) )
36	35	adantl	⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑏 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) )
37	2	a1i	⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑏 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) ) → 𝐼 = ( ℤ × { 0 } ) )
38	33 36 37	3eltr4d	⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑏 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
39	38	exp32	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑦 = ⟨ 𝑏 , 0 ⟩ → ( 𝑥 = ⟨ 𝑎 , 0 ⟩ → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) ) )
40	39	rexlimdva	⊢ ( 𝑎 ∈ ℤ → ( ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 0 ⟩ → ( 𝑥 = ⟨ 𝑎 , 0 ⟩ → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) ) )
41	40	com23	⊢ ( 𝑎 ∈ ℤ → ( 𝑥 = ⟨ 𝑎 , 0 ⟩ → ( ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 0 ⟩ → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) ) )
42	41	rexlimiv	⊢ ( ∃ 𝑎 ∈ ℤ 𝑥 = ⟨ 𝑎 , 0 ⟩ → ( ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 0 ⟩ → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) )
43	42	imp	⊢ ( ( ∃ 𝑎 ∈ ℤ 𝑥 = ⟨ 𝑎 , 0 ⟩ ∧ ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 0 ⟩ ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
44	4 5 43	syl2anb	⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
45	44	rgen2	⊢ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼
46	1	pzriprnglem1	⊢ 𝑅 ∈ Rng
47		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
48	47 25	issubrng2	⊢ ( 𝑅 ∈ Rng → ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) ) )
49	46 48	ax-mp	⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) )
50	3 45 49	mpbir2an	⊢ 𝐼 ∈ ( SubRng ‘ 𝑅 )