0idl

Description: The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	0idl.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
	0idl.2	⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion	0idl	⊢ ( 𝑅 ∈ RingOps → { 𝑍 } ∈ ( Idl ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		0idl.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		0idl.2	⊢ 𝑍 = ( GId ‘ 𝐺 )
3		eqid	⊢ ran 𝐺 = ran 𝐺
4	1 3 2	rngo0cl	⊢ ( 𝑅 ∈ RingOps → 𝑍 ∈ ran 𝐺 )
5	4	snssd	⊢ ( 𝑅 ∈ RingOps → { 𝑍 } ⊆ ran 𝐺 )
6	2	fvexi	⊢ 𝑍 ∈ V
7	6	snid	⊢ 𝑍 ∈ { 𝑍 }
8	7	a1i	⊢ ( 𝑅 ∈ RingOps → 𝑍 ∈ { 𝑍 } )
9		velsn	⊢ ( 𝑥 ∈ { 𝑍 } ↔ 𝑥 = 𝑍 )
10		velsn	⊢ ( 𝑦 ∈ { 𝑍 } ↔ 𝑦 = 𝑍 )
11	1 3 2	rngo0rid	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑍 ∈ ran 𝐺 ) → ( 𝑍 𝐺 𝑍 ) = 𝑍 )
12	4 11	mpdan	⊢ ( 𝑅 ∈ RingOps → ( 𝑍 𝐺 𝑍 ) = 𝑍 )
13		ovex	⊢ ( 𝑍 𝐺 𝑍 ) ∈ V
14	13	elsn	⊢ ( ( 𝑍 𝐺 𝑍 ) ∈ { 𝑍 } ↔ ( 𝑍 𝐺 𝑍 ) = 𝑍 )
15	12 14	sylibr	⊢ ( 𝑅 ∈ RingOps → ( 𝑍 𝐺 𝑍 ) ∈ { 𝑍 } )
16		oveq2	⊢ ( 𝑦 = 𝑍 → ( 𝑍 𝐺 𝑦 ) = ( 𝑍 𝐺 𝑍 ) )
17	16	eleq1d	⊢ ( 𝑦 = 𝑍 → ( ( 𝑍 𝐺 𝑦 ) ∈ { 𝑍 } ↔ ( 𝑍 𝐺 𝑍 ) ∈ { 𝑍 } ) )
18	15 17	syl5ibrcom	⊢ ( 𝑅 ∈ RingOps → ( 𝑦 = 𝑍 → ( 𝑍 𝐺 𝑦 ) ∈ { 𝑍 } ) )
19	10 18	biimtrid	⊢ ( 𝑅 ∈ RingOps → ( 𝑦 ∈ { 𝑍 } → ( 𝑍 𝐺 𝑦 ) ∈ { 𝑍 } ) )
20	19	ralrimiv	⊢ ( 𝑅 ∈ RingOps → ∀ 𝑦 ∈ { 𝑍 } ( 𝑍 𝐺 𝑦 ) ∈ { 𝑍 } )
21		eqid	⊢ ( 2^nd ‘ 𝑅 ) = ( 2^nd ‘ 𝑅 )
22	2 3 1 21	rngorz	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) = 𝑍 )
23		ovex	⊢ ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ V
24	23	elsn	⊢ ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ { 𝑍 } ↔ ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) = 𝑍 )
25	22 24	sylibr	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ { 𝑍 } )
26	2 3 1 21	rngolz	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) = 𝑍 )
27		ovex	⊢ ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ V
28	27	elsn	⊢ ( ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ↔ ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) = 𝑍 )
29	26 28	sylibr	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } )
30	25 29	jca	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ { 𝑍 } ∧ ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) )
31	30	ralrimiva	⊢ ( 𝑅 ∈ RingOps → ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ { 𝑍 } ∧ ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) )
32	20 31	jca	⊢ ( 𝑅 ∈ RingOps → ( ∀ 𝑦 ∈ { 𝑍 } ( 𝑍 𝐺 𝑦 ) ∈ { 𝑍 } ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ { 𝑍 } ∧ ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ) )
33		oveq1	⊢ ( 𝑥 = 𝑍 → ( 𝑥 𝐺 𝑦 ) = ( 𝑍 𝐺 𝑦 ) )
34	33	eleq1d	⊢ ( 𝑥 = 𝑍 → ( ( 𝑥 𝐺 𝑦 ) ∈ { 𝑍 } ↔ ( 𝑍 𝐺 𝑦 ) ∈ { 𝑍 } ) )
35	34	ralbidv	⊢ ( 𝑥 = 𝑍 → ( ∀ 𝑦 ∈ { 𝑍 } ( 𝑥 𝐺 𝑦 ) ∈ { 𝑍 } ↔ ∀ 𝑦 ∈ { 𝑍 } ( 𝑍 𝐺 𝑦 ) ∈ { 𝑍 } ) )
36		oveq2	⊢ ( 𝑥 = 𝑍 → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) = ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) )
37	36	eleq1d	⊢ ( 𝑥 = 𝑍 → ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ { 𝑍 } ↔ ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ { 𝑍 } ) )
38		oveq1	⊢ ( 𝑥 = 𝑍 → ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) = ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) )
39	38	eleq1d	⊢ ( 𝑥 = 𝑍 → ( ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ↔ ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) )
40	37 39	anbi12d	⊢ ( 𝑥 = 𝑍 → ( ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ { 𝑍 } ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ↔ ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ { 𝑍 } ∧ ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ) )
41	40	ralbidv	⊢ ( 𝑥 = 𝑍 → ( ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ { 𝑍 } ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ↔ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ { 𝑍 } ∧ ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ) )
42	35 41	anbi12d	⊢ ( 𝑥 = 𝑍 → ( ( ∀ 𝑦 ∈ { 𝑍 } ( 𝑥 𝐺 𝑦 ) ∈ { 𝑍 } ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ { 𝑍 } ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ) ↔ ( ∀ 𝑦 ∈ { 𝑍 } ( 𝑍 𝐺 𝑦 ) ∈ { 𝑍 } ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑍 ) ∈ { 𝑍 } ∧ ( 𝑍 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ) ) )
43	32 42	syl5ibrcom	⊢ ( 𝑅 ∈ RingOps → ( 𝑥 = 𝑍 → ( ∀ 𝑦 ∈ { 𝑍 } ( 𝑥 𝐺 𝑦 ) ∈ { 𝑍 } ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ { 𝑍 } ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ) ) )
44	9 43	biimtrid	⊢ ( 𝑅 ∈ RingOps → ( 𝑥 ∈ { 𝑍 } → ( ∀ 𝑦 ∈ { 𝑍 } ( 𝑥 𝐺 𝑦 ) ∈ { 𝑍 } ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ { 𝑍 } ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ) ) )
45	44	ralrimiv	⊢ ( 𝑅 ∈ RingOps → ∀ 𝑥 ∈ { 𝑍 } ( ∀ 𝑦 ∈ { 𝑍 } ( 𝑥 𝐺 𝑦 ) ∈ { 𝑍 } ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ { 𝑍 } ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ) )
46	1 21 3 2	isidl	⊢ ( 𝑅 ∈ RingOps → ( { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ↔ ( { 𝑍 } ⊆ ran 𝐺 ∧ 𝑍 ∈ { 𝑍 } ∧ ∀ 𝑥 ∈ { 𝑍 } ( ∀ 𝑦 ∈ { 𝑍 } ( 𝑥 𝐺 𝑦 ) ∈ { 𝑍 } ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ { 𝑍 } ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ { 𝑍 } ) ) ) ) )
47	5 8 45 46	mpbir3and	⊢ ( 𝑅 ∈ RingOps → { 𝑍 } ∈ ( Idl ‘ 𝑅 ) )

Metamath Proof Explorer

Theorem 0idl

Proof