mxidlirred - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mxidlirred		Structured version Visualization version GIF version

Theorem mxidlirred 33755

Description: In a principal ideal domain, maximal ideals are exactly the ideals generated by irreducible elements. (Contributed by Thierry Arnoux, 22-Mar-2025.)

**Hypotheses**
Ref	Expression
mxidlirred.b	⊢ 𝐵 = (Base‘𝑅)
mxidlirred.k	⊢ 𝐾 = (RSpan‘𝑅)
mxidlirred.0	⊢ 0 = (0_g‘𝑅)
mxidlirred.m	⊢ 𝑀 = (𝐾‘{𝑋})
mxidlirred.r	⊢ (𝜑 → 𝑅 ∈ PID)
mxidlirred.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
mxidlirred.y	⊢ (𝜑 → 𝑋 ≠ 0 )
mxidlirred.1	⊢ (𝜑 → 𝑀 ∈ (LIdeal‘𝑅))

**Assertion**
Ref	Expression
mxidlirred	⊢ (𝜑 → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ 𝑋 ∈ (Irred‘𝑅)))

Proof of Theorem mxidlirred Dummy variables 𝑡 𝑥 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mxidlirred.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
2		mxidlirred.k	. . 3 ⊢ 𝐾 = (RSpan‘𝑅)
3		mxidlirred.0	. . 3 ⊢ 0 = (0_g‘𝑅)
4		mxidlirred.m	. . 3 ⊢ 𝑀 = (𝐾‘{𝑋})
5		mxidlirred.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ PID)
6		df-pid 21505	. . . . . 6 ⊢ PID = (IDomn ∩ LPIR)
7	5, 6	eleqtrdi 2873	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ (IDomn ∩ LPIR))
8	7	elin1d 4157	. . . 4 ⊢ (𝜑 → 𝑅 ∈ IDomn)
9	8	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑅 ∈ IDomn)
10		mxidlirred.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
11	10	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑋 ∈ 𝐵)
12		mxidlirred.y	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 0 )
13	12	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑋 ≠ 0 )
14		simpr 489	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (MaxIdeal‘𝑅))
15	1, 2, 3, 4, 9, 11, 13, 14	mxidlirredi 33754	. 2 ⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑋 ∈ (Irred‘𝑅))
16		eqid 2763	. . . . . . . . . . 11 ⊢ (∥_r‘𝑅) = (∥_r‘𝑅)
17		simplr 780	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑥 ∈ 𝐵)
18	17	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑥 ∈ 𝐵)
19	10	ad8antr 752	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑋 ∈ 𝐵)
20		eqid 2763	. . . . . . . . . . 11 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
21		eqid 2763	. . . . . . . . . . 11 ⊢ (._r‘𝑅) = (._r‘𝑅)
22	8	idomringd 20826	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Ring)
23	22	ad4antr 744	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑅 ∈ Ring)
24	23	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑅 ∈ Ring)
25	24	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑅 ∈ Ring)
26		simplr 780	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑡 ∈ 𝐵)
27		simpr 489	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑋 = (𝑡(._r‘𝑅)𝑥))
28		simp-8r 803	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑋 ∈ (Irred‘𝑅))
29	27, 28	eqeltrrd 2864	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → (𝑡(._r‘𝑅)𝑥) ∈ (Irred‘𝑅))
30		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (Irred‘𝑅) = (Irred‘𝑅)
31	30, 1, 20, 21	irredmul 20507	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ (𝑡(._r‘𝑅)𝑥) ∈ (Irred‘𝑅)) → (𝑡 ∈ (Unit‘𝑅) ∨ 𝑥 ∈ (Unit‘𝑅)))
32	26, 18, 29, 31	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → (𝑡 ∈ (Unit‘𝑅) ∨ 𝑥 ∈ (Unit‘𝑅)))
33		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑘 = (𝐾‘{𝑥}))
34	33	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑘 = (𝐾‘{𝑥}))
35		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))
36		annim 408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ⊆ 𝑘 ∧ ¬ (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)) ↔ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))
37	35, 36	sylibr 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → (𝑀 ⊆ 𝑘 ∧ ¬ (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))
38	37	simprd 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ¬ (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))
39		ioran 999	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (𝑘 = 𝑀 ∨ 𝑘 = 𝐵) ↔ (¬ 𝑘 = 𝑀 ∧ ¬ 𝑘 = 𝐵))
40	38, 39	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → (¬ 𝑘 = 𝑀 ∧ ¬ 𝑘 = 𝐵))
41	40	simprd 500	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ¬ 𝑘 = 𝐵)
42	41	neqned 2965	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑘 ≠ 𝐵)
43	42	ad4antr 744	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑘 ≠ 𝐵)
44	34, 43	eqnetrrd 3026	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → (𝐾‘{𝑥}) ≠ 𝐵)
45	44	neneqd 2963	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → ¬ (𝐾‘{𝑥}) = 𝐵)
46		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝐾‘{𝑥}) = (𝐾‘{𝑥})
47	8	ad8antr 752	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑅 ∈ IDomn)
48	47	idomcringd 20825	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑅 ∈ CRing)
49	20, 2, 46, 1, 18, 48	unitpidl1 33732	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → ((𝐾‘{𝑥}) = 𝐵 ↔ 𝑥 ∈ (Unit‘𝑅)))
50	45, 49	mtbid 327	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → ¬ 𝑥 ∈ (Unit‘𝑅))
51	32, 50	olcnd 890	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑡 ∈ (Unit‘𝑅))
52	27	eqcomd 2769	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → (𝑡(._r‘𝑅)𝑥) = 𝑋)
53	1, 2, 16, 18, 19, 20, 21, 25, 51, 52	dvdsruassoi 33697	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → (𝑥(∥_r‘𝑅)𝑋 ∧ 𝑋(∥_r‘𝑅)𝑥))
54	1, 2, 16, 18, 19, 25	rspsnasso 33701	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → ((𝑥(∥_r‘𝑅)𝑋 ∧ 𝑋(∥_r‘𝑅)𝑥) ↔ (𝐾‘{𝑋}) = (𝐾‘{𝑥})))
55	53, 54	mpbid 235	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → (𝐾‘{𝑋}) = (𝐾‘{𝑥}))
56	55, 34	eqtr4d 2801	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → (𝐾‘{𝑋}) = 𝑘)
57	4, 56	eqtr2id 2811	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑘 = 𝑀)
58	40	simpld 499	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ¬ 𝑘 = 𝑀)
59	58	ad4antr 744	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → ¬ 𝑘 = 𝑀)
60	57, 59	pm2.21dd 198	. . . . . 6 ⊢ (((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(._r‘𝑅)𝑥)) → 𝑀 ∈ (MaxIdeal‘𝑅))
61	37	simpld 499	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑀 ⊆ 𝑘)
62	61	ad2antrr 738	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑀 ⊆ 𝑘)
63	10	snssd 4752	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑋} ⊆ 𝐵)
64	2, 1	rspssid 21365	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ {𝑋} ⊆ 𝐵) → {𝑋} ⊆ (𝐾‘{𝑋}))
65	22, 63, 64	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑋} ⊆ (𝐾‘{𝑋}))
66	65, 4	sseqtrrdi 3978	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑋} ⊆ 𝑀)
67		snssg 4749	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ 𝐵 → (𝑋 ∈ 𝑀 ↔ {𝑋} ⊆ 𝑀))
68	67	biimpar 482	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝐵 ∧ {𝑋} ⊆ 𝑀) → 𝑋 ∈ 𝑀)
69	10, 66, 68	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝑀)
70	69	ad6antr 748	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑋 ∈ 𝑀)
71	62, 70	sseldd 3938	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑋 ∈ 𝑘)
72	71, 33	eleqtrd 2865	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑋 ∈ (𝐾‘{𝑥}))
73	1, 21, 2	elrspsn 21371	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑋 ∈ (𝐾‘{𝑥}) ↔ ∃𝑡 ∈ 𝐵 𝑋 = (𝑡(._r‘𝑅)𝑥)))
74	73	biimpa 481	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ∧ 𝑋 ∈ (𝐾‘{𝑥})) → ∃𝑡 ∈ 𝐵 𝑋 = (𝑡(._r‘𝑅)𝑥))
75	24, 17, 72, 74	syl21anc 850	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → ∃𝑡 ∈ 𝐵 𝑋 = (𝑡(._r‘𝑅)𝑥))
76	60, 75	r19.29a 3173	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑀 ∈ (MaxIdeal‘𝑅))
77		simplr 780	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑘 ∈ (LIdeal‘𝑅))
78	7	elin2d 4158	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ LPIR)
79		eqid 2763	. . . . . . . . . . 11 ⊢ (LPIdeal‘𝑅) = (LPIdeal‘𝑅)
80		eqid 2763	. . . . . . . . . . 11 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
81	79, 80	islpir 21496	. . . . . . . . . 10 ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ (LIdeal‘𝑅) = (LPIdeal‘𝑅)))
82	81	simprbi 502	. . . . . . . . 9 ⊢ (𝑅 ∈ LPIR → (LIdeal‘𝑅) = (LPIdeal‘𝑅))
83	78, 82	syl 18	. . . . . . . 8 ⊢ (𝜑 → (LIdeal‘𝑅) = (LPIdeal‘𝑅))
84	83	ad4antr 744	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → (LIdeal‘𝑅) = (LPIdeal‘𝑅))
85	77, 84	eleqtrd 2865	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑘 ∈ (LPIdeal‘𝑅))
86	79, 2, 1	islpidl 21493	. . . . . . 7 ⊢ (𝑅 ∈ Ring → (𝑘 ∈ (LPIdeal‘𝑅) ↔ ∃𝑥 ∈ 𝐵 𝑘 = (𝐾‘{𝑥})))
87	86	biimpa 481	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LPIdeal‘𝑅)) → ∃𝑥 ∈ 𝐵 𝑘 = (𝐾‘{𝑥}))
88	23, 85, 87	syl2anc 595	. . . . 5 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ∃𝑥 ∈ 𝐵 𝑘 = (𝐾‘{𝑥}))
89	76, 88	r19.29a 3173	. . . 4 ⊢ (((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑀 ∈ (MaxIdeal‘𝑅))
90		mxidlirred.1	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (LIdeal‘𝑅))
91	90	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (LIdeal‘𝑅))
92	30, 20	irrednu 20503	. . . . . . . . . 10 ⊢ (𝑋 ∈ (Irred‘𝑅) → ¬ 𝑋 ∈ (Unit‘𝑅))
93	92	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → ¬ 𝑋 ∈ (Unit‘𝑅))
94	8	idomcringd 20825	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ CRing)
95	20, 2, 4, 1, 10, 94	unitpidl1 33732	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 = 𝐵 ↔ 𝑋 ∈ (Unit‘𝑅)))
96	95	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → (𝑀 = 𝐵 ↔ 𝑋 ∈ (Unit‘𝑅)))
97	96	necon3abid 2994	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → (𝑀 ≠ 𝐵 ↔ ¬ 𝑋 ∈ (Unit‘𝑅)))
98	93, 97	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → 𝑀 ≠ 𝐵)
99	98	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵)
100	91, 99	jca 520	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵))
101	1	ismxidl 33745	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))))
102	22, 101	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))))
103		df-3an 1105	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ↔ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))))
104	102, 103	bitrdi 290	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))))
105	104	notbid 321	. . . . . . . 8 ⊢ (𝜑 → (¬ 𝑀 ∈ (MaxIdeal‘𝑅) ↔ ¬ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))))
106	105	biimpa 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))))
107	106	adantlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))))
108	100, 107	mpnanrd 414	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))
109		rexnal 3117	. . . . 5 ⊢ (∃𝑘 ∈ (LIdeal‘𝑅) ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)) ↔ ¬ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))
110	108, 109	sylibr 237	. . . 4 ⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → ∃𝑘 ∈ (LIdeal‘𝑅) ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))
111	89, 110	r19.29a 3173	. . 3 ⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (MaxIdeal‘𝑅))
112	111	pm2.18da 811	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → 𝑀 ∈ (MaxIdeal‘𝑅))
113	15, 112	impbida 812	1 ⊢ (𝜑 → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ 𝑋 ∈ (Irred‘𝑅)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 ∩ cin 3904 ⊆ wss 3905 {csn 4589 class class class wbr 5109 ‘cfv 6536 (class class class)co 7410 Basecbs 17264 ._rcmulr 17306 0_gc0g 17487 Ringcrg 20310 ∥_rcdsr 20432 Unitcui 20433 Irredcir 20434 IDomncidom 20792 LIdealclidl 21330 RSpancrsp 21331 LPIdealclpidl 21488 LPIRclpir 21489 PIDcpid 21504 MaxIdealcmxidl 33742

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-tpos 8218 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-3 12299 df-4 12300 df-5 12301 df-6 12302 df-7 12303 df-8 12304 df-sets 17219 df-slot 17237 df-ndx 17249 df-base 17265 df-ress 17286 df-plusg 17318 df-mulr 17319 df-sca 17321 df-vsca 17322 df-ip 17323 df-0g 17489 df-mgm 18693 df-sgrp 18772 df-mnd 18788 df-grp 18998 df-minusg 18999 df-sbg 19000 df-subg 19184 df-cmn 19847 df-abl 19848 df-mgp 20212 df-rng 20226 df-ur 20259 df-ring 20312 df-cring 20313 df-oppr 20415 df-dvdsr 20435 df-unit 20436 df-irred 20437 df-invr 20466 df-nzr 20610 df-subrg 20669 df-domn 20794 df-idom 20795 df-lmod 20983 df-lss 21053 df-lsp 21093 df-sra 21294 df-rgmod 21295 df-lidl 21332 df-rsp 21333 df-lpidl 21490 df-lpir 21491 df-pid 21505 df-mxidl 33743

This theorem is referenced by: rprmirredb 33822 algextdeglem4 34110

W3C validator