pzriprnglem8 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pzriprnglem8		Structured version Visualization version GIF version

Theorem pzriprnglem8 21467

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

**Hypotheses**
Ref	Expression
pzriprng.r	⊢ 𝑅 = (ℤ_ring ×_s ℤ_ring)
pzriprng.i	⊢ 𝐼 = (ℤ × {0})
pzriprng.j	⊢ 𝐽 = (𝑅 ↾_s 𝐼)

**Assertion**
Ref	Expression
pzriprnglem8	⊢ 𝐼 ∈ (2Ideal‘𝑅)

Proof of Theorem pzriprnglem8 Dummy variables 𝑥 𝑦 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pzriprng.r	. . . . . . 7 ⊢ 𝑅 = (ℤ_ring ×_s ℤ_ring)
2	1	pzriprnglem2 21461	. . . . . 6 ⊢ (Base‘𝑅) = (ℤ × ℤ)
3	2	eleq2i 2833	. . . . 5 ⊢ (𝑥 ∈ (Base‘𝑅) ↔ 𝑥 ∈ (ℤ × ℤ))
4		elxp2 5645	. . . . 5 ⊢ (𝑥 ∈ (ℤ × ℤ) ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = ⟨𝑎, 𝑏⟩)
5	3, 4	bitri 277	. . . 4 ⊢ (𝑥 ∈ (Base‘𝑅) ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = ⟨𝑎, 𝑏⟩)
6		pzriprng.i	. . . . 5 ⊢ 𝐼 = (ℤ × {0})
7	1, 6	pzriprnglem3 21462	. . . 4 ⊢ (𝑦 ∈ 𝐼 ↔ ∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩)
8		simpll 773	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 𝑎 ∈ ℤ)
9		simpr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 𝑐 ∈ ℤ)
10	8, 9	zmulcld 12634	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑎 · 𝑐) ∈ ℤ)
11		zcn 12524	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ ℤ → 𝑏 ∈ ℂ)
12	11	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℂ)
13	12	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 𝑏 ∈ ℂ)
14	13	mul01d 11340	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑏 · 0) = 0)
15		ovex 7393	. . . . . . . . . . . . . . 15 ⊢ (𝑏 · 0) ∈ V
16	15	elsn 4573	. . . . . . . . . . . . . 14 ⊢ ((𝑏 · 0) ∈ {0} ↔ (𝑏 · 0) = 0)
17	14, 16	sylibr 236	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑏 · 0) ∈ {0})
18	10, 17	opelxpd 5660	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ⟨(𝑎 · 𝑐), (𝑏 · 0)⟩ ∈ (ℤ × {0}))
19	9, 8	zmulcld 12634	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑐 · 𝑎) ∈ ℤ)
20	13	mul02d 11339	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (0 · 𝑏) = 0)
21		ovex 7393	. . . . . . . . . . . . . . 15 ⊢ (0 · 𝑏) ∈ V
22	21	elsn 4573	. . . . . . . . . . . . . 14 ⊢ ((0 · 𝑏) ∈ {0} ↔ (0 · 𝑏) = 0)
23	20, 22	sylibr 236	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (0 · 𝑏) ∈ {0})
24	19, 23	opelxpd 5660	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ⟨(𝑐 · 𝑎), (0 · 𝑏)⟩ ∈ (ℤ × {0}))
25		zringbas 21432	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤ_ring)
26		zringring 21428	. . . . . . . . . . . . . . . 16 ⊢ ℤ_ring ∈ Ring
27	26	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ℤ_ring ∈ Ring)
28		simplr 775	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 𝑏 ∈ ℤ)
29		0zd 12531	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 0 ∈ ℤ)
30	28, 29	zmulcld 12634	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑏 · 0) ∈ ℤ)
31		zringmulr 21436	. . . . . . . . . . . . . . 15 ⊢ · = (._r‘ℤ_ring)
32		eqid 2741	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝑅) = (._r‘𝑅)
33	1, 25, 25, 27, 27, 8, 28, 9, 29, 10, 30, 31, 31, 32	xpsmul 17534	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) = ⟨(𝑎 · 𝑐), (𝑏 · 0)⟩)
34	33	eleq1d 2826	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ↔ ⟨(𝑎 · 𝑐), (𝑏 · 0)⟩ ∈ (ℤ × {0})))
35		simpl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑐 ∈ ℤ)
36		simprl 777	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℤ)
37	35, 36	zmulcld 12634	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑐 · 𝑎) ∈ ℤ)
38	37	ancoms 460	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑐 · 𝑎) ∈ ℤ)
39		0zd 12531	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 0 ∈ ℤ)
40		simprr 779	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℤ)
41	39, 40	zmulcld 12634	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (0 · 𝑏) ∈ ℤ)
42	41	ancoms 460	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (0 · 𝑏) ∈ ℤ)
43	1, 25, 25, 27, 27, 9, 29, 8, 28, 38, 42, 31, 31, 32	xpsmul 17534	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) = ⟨(𝑐 · 𝑎), (0 · 𝑏)⟩)
44	43	eleq1d 2826	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ((⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0}) ↔ ⟨(𝑐 · 𝑎), (0 · 𝑏)⟩ ∈ (ℤ × {0})))
45	34, 44	anbi12d 639	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ∧ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0})) ↔ (⟨(𝑎 · 𝑐), (𝑏 · 0)⟩ ∈ (ℤ × {0}) ∧ ⟨(𝑐 · 𝑎), (0 · 𝑏)⟩ ∈ (ℤ × {0}))))
46	18, 24, 45	mpbir2and 720	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ∧ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0})))
47	46	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → ((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ∧ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0})))
48		oveq12 7369	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑐, 0⟩) → (𝑥(._r‘𝑅)𝑦) = (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩))
49	48	ancoms 460	. . . . . . . . . . . . 13 ⊢ ((𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩) → (𝑥(._r‘𝑅)𝑦) = (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩))
50	49	adantl 483	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → (𝑥(._r‘𝑅)𝑦) = (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩))
51	6	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → 𝐼 = (ℤ × {0}))
52	50, 51	eleq12d 2835	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ↔ (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0})))
53		oveq12 7369	. . . . . . . . . . . . 13 ⊢ ((𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩) → (𝑦(._r‘𝑅)𝑥) = (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩))
54	53	adantl 483	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → (𝑦(._r‘𝑅)𝑥) = (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩))
55	54, 51	eleq12d 2835	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → ((𝑦(._r‘𝑅)𝑥) ∈ 𝐼 ↔ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0})))
56	52, 55	anbi12d 639	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → (((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼) ↔ ((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ∧ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0}))))
57	47, 56	mpbird 259	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))
58	57	exp32 422	. . . . . . . 8 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑦 = ⟨𝑐, 0⟩ → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))))
59	58	rexlimdva 3142	. . . . . . 7 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩ → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))))
60	59	com23 86	. . . . . 6 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑥 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩ → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))))
61	60	rexlimivv 3183	. . . . 5 ⊢ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩ → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼)))
62	61	imp 408	. . . 4 ⊢ ((∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = ⟨𝑎, 𝑏⟩ ∧ ∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩) → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))
63	5, 7, 62	syl2anb 605	. . 3 ⊢ ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐼) → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))
64	63	rgen2 3181	. 2 ⊢ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ 𝐼 ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼)
65	1	pzriprnglem1 21460	. . 3 ⊢ 𝑅 ∈ Rng
66	1, 6	pzriprnglem4 21463	. . 3 ⊢ 𝐼 ∈ (SubGrp‘𝑅)
67		eqid 2741	. . . 4 ⊢ (2Ideal‘𝑅) = (2Ideal‘𝑅)
68		eqid 2741	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
69	67, 68, 32	df2idl2rng 21253	. . 3 ⊢ ((𝑅 ∈ Rng ∧ 𝐼 ∈ (SubGrp‘𝑅)) → (𝐼 ∈ (2Ideal‘𝑅) ↔ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ 𝐼 ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼)))
70	65, 66, 69	mp2an 699	. 2 ⊢ (𝐼 ∈ (2Ideal‘𝑅) ↔ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ 𝐼 ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))
71	64, 70	mpbir 233	1 ⊢ 𝐼 ∈ (2Ideal‘𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 397 = wceq 1548 ∈ wcel 2121 ∀wral 3055 ∃wrex 3065 {csn 4558 ⟨cop 4564 × cxp 5619 ‘cfv 6489 (class class class)co 7360 ℂcc 11031 0cc0 11033 · cmul 11038 ℤcz 12519 Basecbs 17174 ↾_s cress 17195 ._rcmulr 17216 ×_s cxps 17465 SubGrpcsubg 19091 Rngcrng 20128 Ringcrg 20209 2Idealc2idl 21246 ℤ_ringczring 21425

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-addf 11112 ax-mulf 11113

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4842 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-tpos 8170 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-er 8637 df-map 8769 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-sup 9349 df-inf 9350 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-7 12244 df-8 12245 df-9 12246 df-n0 12433 df-z 12520 df-dec 12640 df-uz 12784 df-fz 13457 df-struct 17112 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-ress 17196 df-plusg 17228 df-mulr 17229 df-starv 17230 df-sca 17231 df-vsca 17232 df-ip 17233 df-tset 17234 df-ple 17235 df-ds 17237 df-unif 17238 df-hom 17239 df-cco 17240 df-0g 17399 df-prds 17405 df-imas 17467 df-xps 17469 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-grp 18907 df-minusg 18908 df-subg 19094 df-cmn 19752 df-abl 19753 df-mgp 20117 df-rng 20129 df-ur 20158 df-ring 20211 df-cring 20212 df-oppr 20312 df-subrng 20522 df-subrg 20546 df-lss 20926 df-sra 21167 df-rgmod 21168 df-lidl 21205 df-2idl 21247 df-cnfld 21352 df-zring 21426

This theorem is referenced by: pzriprnglem12 21471 pzriprnglem13 21472 pzriprngALT 21474 pzriprng1ALT 21475

W3C validator