Theorem isirred

Description: An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irred.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	irred.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	irred.3	⊢ 𝐼 = ( Irred ‘ 𝑅 )
	irred.4	⊢ 𝑁 = ( 𝐵 ∖ 𝑈 )
	irred.5	⊢ · = ( .r ‘ 𝑅 )
Assertion	isirred	⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		irred.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		irred.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		irred.3	⊢ 𝐼 = ( Irred ‘ 𝑅 )
4		irred.4	⊢ 𝑁 = ( 𝐵 ∖ 𝑈 )
5		irred.5	⊢ · = ( .r ‘ 𝑅 )
6		elfvdm	⊢ ( 𝑋 ∈ ( Irred ‘ 𝑅 ) → 𝑅 ∈ dom Irred )
7	6 3	eleq2s	⊢ ( 𝑋 ∈ 𝐼 → 𝑅 ∈ dom Irred )
8	7	elexd	⊢ ( 𝑋 ∈ 𝐼 → 𝑅 ∈ V )
9		eldifi	⊢ ( 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) → 𝑋 ∈ 𝐵 )
10	9 4	eleq2s	⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ 𝐵 )
11	10 1	eleqtrdi	⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
12	11	elfvexd	⊢ ( 𝑋 ∈ 𝑁 → 𝑅 ∈ V )
13	12	adantr	⊢ ( ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) → 𝑅 ∈ V )
14		fvex	⊢ ( Base ‘ 𝑟 ) ∈ V
15		difexg	⊢ ( ( Base ‘ 𝑟 ) ∈ V → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ∈ V )
16	14 15	mp1i	⊢ ( 𝑟 = 𝑅 → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ∈ V )
17		simpr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) )
18		simpl	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → 𝑟 = 𝑅 )
19	18	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
20	19 1	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Base ‘ 𝑟 ) = 𝐵 )
21	18	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) )
22	21 2	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Unit ‘ 𝑟 ) = 𝑈 )
23	20 22	difeq12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) = ( 𝐵 ∖ 𝑈 ) )
24	23 4	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) = 𝑁 )
25	17 24	eqtrd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → 𝑏 = 𝑁 )
26	18	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
27	26 5	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( .r ‘ 𝑟 ) = · )
28	27	oveqd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
29	28	neeq1d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 ↔ ( 𝑥 · 𝑦 ) ≠ 𝑧 ) )
30	25 29	raleqbidv	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 ↔ ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 ) )
31	25 30	raleqbidv	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 ) )
32	25 31	rabeqbidv	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 } = { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } )
33	16 32	csbied	⊢ ( 𝑟 = 𝑅 → ⦋ ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 } = { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } )
34		df-irred	⊢ Irred = ( 𝑟 ∈ V ↦ ⦋ ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 } )
35		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
36	1 35	eqeltri	⊢ 𝐵 ∈ V
37	36	difexi	⊢ ( 𝐵 ∖ 𝑈 ) ∈ V
38	4 37	eqeltri	⊢ 𝑁 ∈ V
39	38	rabex	⊢ { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ∈ V
40	33 34 39	fvmpt	⊢ ( 𝑅 ∈ V → ( Irred ‘ 𝑅 ) = { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } )
41	3 40	syl5eq	⊢ ( 𝑅 ∈ V → 𝐼 = { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } )
42	41	eleq2d	⊢ ( 𝑅 ∈ V → ( 𝑋 ∈ 𝐼 ↔ 𝑋 ∈ { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ) )
43		neeq2	⊢ ( 𝑧 = 𝑋 → ( ( 𝑥 · 𝑦 ) ≠ 𝑧 ↔ ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
44	43	2ralbidv	⊢ ( 𝑧 = 𝑋 → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
45	44	elrab	⊢ ( 𝑋 ∈ { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
46	42 45	syl6bb	⊢ ( 𝑅 ∈ V → ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) )
47	8 13 46	pm5.21nii	⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )