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 21447

Description: Lemma 8 for pzriprng 21456: 𝐼 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 21441	. . . . . 6 ⊢ (Base‘𝑅) = (ℤ × ℤ)
3	2	eleq2i 2829	. . . . 5 ⊢ (𝑥 ∈ (Base‘𝑅) ↔ 𝑥 ∈ (ℤ × ℤ))
4		elxp2 5649	. . . . 5 ⊢ (𝑥 ∈ (ℤ × ℤ) ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = ⟨𝑎, 𝑏⟩)
5	3, 4	bitri 275	. . . 4 ⊢ (𝑥 ∈ (Base‘𝑅) ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = ⟨𝑎, 𝑏⟩)
6		pzriprng.i	. . . . 5 ⊢ 𝐼 = (ℤ × {0})
7	1, 6	pzriprnglem3 21442	. . . 4 ⊢ (𝑦 ∈ 𝐼 ↔ ∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩)
8		simpll 767	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 𝑎 ∈ ℤ)
9		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 𝑐 ∈ ℤ)
10	8, 9	zmulcld 12606	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑎 · 𝑐) ∈ ℤ)
11		zcn 12497	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ ℤ → 𝑏 ∈ ℂ)
12	11	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℂ)
13	12	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 𝑏 ∈ ℂ)
14	13	mul01d 11336	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑏 · 0) = 0)
15		ovex 7393	. . . . . . . . . . . . . . 15 ⊢ (𝑏 · 0) ∈ V
16	15	elsn 4596	. . . . . . . . . . . . . 14 ⊢ ((𝑏 · 0) ∈ {0} ↔ (𝑏 · 0) = 0)
17	14, 16	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑏 · 0) ∈ {0})
18	10, 17	opelxpd 5664	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ⟨(𝑎 · 𝑐), (𝑏 · 0)⟩ ∈ (ℤ × {0}))
19	9, 8	zmulcld 12606	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑐 · 𝑎) ∈ ℤ)
20	13	mul02d 11335	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (0 · 𝑏) = 0)
21		ovex 7393	. . . . . . . . . . . . . . 15 ⊢ (0 · 𝑏) ∈ V
22	21	elsn 4596	. . . . . . . . . . . . . 14 ⊢ ((0 · 𝑏) ∈ {0} ↔ (0 · 𝑏) = 0)
23	20, 22	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (0 · 𝑏) ∈ {0})
24	19, 23	opelxpd 5664	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ⟨(𝑐 · 𝑎), (0 · 𝑏)⟩ ∈ (ℤ × {0}))
25		zringbas 21412	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤ_ring)
26		zringring 21408	. . . . . . . . . . . . . . . 16 ⊢ ℤ_ring ∈ Ring
27	26	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ℤ_ring ∈ Ring)
28		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 𝑏 ∈ ℤ)
29		0zd 12504	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → 0 ∈ ℤ)
30	28, 29	zmulcld 12606	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑏 · 0) ∈ ℤ)
31		zringmulr 21416	. . . . . . . . . . . . . . 15 ⊢ · = (._r‘ℤ_ring)
32		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝑅) = (._r‘𝑅)
33	1, 25, 25, 27, 27, 8, 28, 9, 29, 10, 30, 31, 31, 32	xpsmul 17500	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) = ⟨(𝑎 · 𝑐), (𝑏 · 0)⟩)
34	33	eleq1d 2822	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ↔ ⟨(𝑎 · 𝑐), (𝑏 · 0)⟩ ∈ (ℤ × {0})))
35		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑐 ∈ ℤ)
36		simprl 771	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℤ)
37	35, 36	zmulcld 12606	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑐 · 𝑎) ∈ ℤ)
38	37	ancoms 458	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑐 · 𝑎) ∈ ℤ)
39		0zd 12504	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 0 ∈ ℤ)
40		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℤ)
41	39, 40	zmulcld 12606	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ ℤ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (0 · 𝑏) ∈ ℤ)
42	41	ancoms 458	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (0 · 𝑏) ∈ ℤ)
43	1, 25, 25, 27, 27, 9, 29, 8, 28, 38, 42, 31, 31, 32	xpsmul 17500	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) = ⟨(𝑐 · 𝑎), (0 · 𝑏)⟩)
44	43	eleq1d 2822	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ((⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0}) ↔ ⟨(𝑐 · 𝑎), (0 · 𝑏)⟩ ∈ (ℤ × {0})))
45	34, 44	anbi12d 633	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ∧ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0})) ↔ (⟨(𝑎 · 𝑐), (𝑏 · 0)⟩ ∈ (ℤ × {0}) ∧ ⟨(𝑐 · 𝑎), (0 · 𝑏)⟩ ∈ (ℤ × {0}))))
46	18, 24, 45	mpbir2and 714	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → ((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ∧ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0})))
47	46	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → ((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ∧ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0})))
48		oveq12 7369	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑐, 0⟩) → (𝑥(._r‘𝑅)𝑦) = (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩))
49	48	ancoms 458	. . . . . . . . . . . . 13 ⊢ ((𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩) → (𝑥(._r‘𝑅)𝑦) = (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩))
50	49	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → (𝑥(._r‘𝑅)𝑦) = (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩))
51	6	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → 𝐼 = (ℤ × {0}))
52	50, 51	eleq12d 2831	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ↔ (⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0})))
53		oveq12 7369	. . . . . . . . . . . . 13 ⊢ ((𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩) → (𝑦(._r‘𝑅)𝑥) = (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩))
54	53	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → (𝑦(._r‘𝑅)𝑥) = (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩))
55	54, 51	eleq12d 2831	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → ((𝑦(._r‘𝑅)𝑥) ∈ 𝐼 ↔ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0})))
56	52, 55	anbi12d 633	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → (((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼) ↔ ((⟨𝑎, 𝑏⟩(._r‘𝑅)⟨𝑐, 0⟩) ∈ (ℤ × {0}) ∧ (⟨𝑐, 0⟩(._r‘𝑅)⟨𝑎, 𝑏⟩) ∈ (ℤ × {0}))))
57	47, 56	mpbird 257	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) ∧ (𝑦 = ⟨𝑐, 0⟩ ∧ 𝑥 = ⟨𝑎, 𝑏⟩)) → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))
58	57	exp32 420	. . . . . . . 8 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ 𝑐 ∈ ℤ) → (𝑦 = ⟨𝑐, 0⟩ → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))))
59	58	rexlimdva 3138	. . . . . . 7 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩ → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))))
60	59	com23 86	. . . . . 6 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑥 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩ → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))))
61	60	rexlimivv 3179	. . . . 5 ⊢ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩ → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼)))
62	61	imp 406	. . . 4 ⊢ ((∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = ⟨𝑎, 𝑏⟩ ∧ ∃𝑐 ∈ ℤ 𝑦 = ⟨𝑐, 0⟩) → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))
63	5, 7, 62	syl2anb 599	. . 3 ⊢ ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐼) → ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))
64	63	rgen2 3177	. 2 ⊢ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ 𝐼 ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼)
65	1	pzriprnglem1 21440	. . 3 ⊢ 𝑅 ∈ Rng
66	1, 6	pzriprnglem4 21443	. . 3 ⊢ 𝐼 ∈ (SubGrp‘𝑅)
67		eqid 2737	. . . 4 ⊢ (2Ideal‘𝑅) = (2Ideal‘𝑅)
68		eqid 2737	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
69	67, 68, 32	df2idl2rng 21215	. . 3 ⊢ ((𝑅 ∈ Rng ∧ 𝐼 ∈ (SubGrp‘𝑅)) → (𝐼 ∈ (2Ideal‘𝑅) ↔ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ 𝐼 ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼)))
70	65, 66, 69	mp2an 693	. 2 ⊢ (𝐼 ∈ (2Ideal‘𝑅) ↔ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ 𝐼 ((𝑥(._r‘𝑅)𝑦) ∈ 𝐼 ∧ (𝑦(._r‘𝑅)𝑥) ∈ 𝐼))
71	64, 70	mpbir 231	1 ⊢ 𝐼 ∈ (2Ideal‘𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3061 {csn 4581 ⟨cop 4587 × cxp 5623 ‘cfv 6493 (class class class)co 7360 ℂcc 11028 0cc0 11030 · cmul 11035 ℤcz 12492 Basecbs 17140 ↾_s cress 17161 ._rcmulr 17182 ×_s cxps 17431 SubGrpcsubg 19054 Rngcrng 20091 Ringcrg 20172 2Idealc2idl 21208 ℤ_ringczring 21405

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-addf 11109 ax-mulf 11110

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-iun 4949 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 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 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12150 df-2 12212 df-3 12213 df-4 12214 df-5 12215 df-6 12216 df-7 12217 df-8 12218 df-9 12219 df-n0 12406 df-z 12493 df-dec 12612 df-uz 12756 df-fz 13428 df-struct 17078 df-sets 17095 df-slot 17113 df-ndx 17125 df-base 17141 df-ress 17162 df-plusg 17194 df-mulr 17195 df-starv 17196 df-sca 17197 df-vsca 17198 df-ip 17199 df-tset 17200 df-ple 17201 df-ds 17203 df-unif 17204 df-hom 17205 df-cco 17206 df-0g 17365 df-prds 17371 df-imas 17433 df-xps 17435 df-mgm 18569 df-sgrp 18648 df-mnd 18664 df-grp 18870 df-minusg 18871 df-subg 19057 df-cmn 19715 df-abl 19716 df-mgp 20080 df-rng 20092 df-ur 20121 df-ring 20174 df-cring 20175 df-oppr 20277 df-subrng 20483 df-subrg 20507 df-lss 20887 df-sra 21129 df-rgmod 21130 df-lidl 21167 df-2idl 21209 df-cnfld 21314 df-zring 21406

This theorem is referenced by: pzriprnglem12 21451 pzriprnglem13 21452 pzriprngALT 21454 pzriprng1ALT 21455

W3C validator