idlval

Description: The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	idlval.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
	idlval.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
	idlval.3	⊢ 𝑋 = ran 𝐺
	idlval.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion	idlval	⊢ ( 𝑅 ∈ RingOps → ( Idl ‘ 𝑅 ) = { 𝑖 ∈ 𝒫 𝑋 ∣ ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		idlval.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		idlval.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
3		idlval.3	⊢ 𝑋 = ran 𝐺
4		idlval.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
5		fveq2	⊢ ( 𝑟 = 𝑅 → ( 1^st ‘ 𝑟 ) = ( 1^st ‘ 𝑅 ) )
6	5 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 1^st ‘ 𝑟 ) = 𝐺 )
7	6	rneqd	⊢ ( 𝑟 = 𝑅 → ran ( 1^st ‘ 𝑟 ) = ran 𝐺 )
8	7 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ran ( 1^st ‘ 𝑟 ) = 𝑋 )
9	8	pweqd	⊢ ( 𝑟 = 𝑅 → 𝒫 ran ( 1^st ‘ 𝑟 ) = 𝒫 𝑋 )
10	6	fveq2d	⊢ ( 𝑟 = 𝑅 → ( GId ‘ ( 1^st ‘ 𝑟 ) ) = ( GId ‘ 𝐺 ) )
11	10 4	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( GId ‘ ( 1^st ‘ 𝑟 ) ) = 𝑍 )
12	11	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖 ↔ 𝑍 ∈ 𝑖 ) )
13	6	oveqd	⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
14	13	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ↔ ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ) )
15	14	ralbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ↔ ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ) )
16		fveq2	⊢ ( 𝑟 = 𝑅 → ( 2^nd ‘ 𝑟 ) = ( 2^nd ‘ 𝑅 ) )
17	16 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 2^nd ‘ 𝑟 ) = 𝐻 )
18	17	oveqd	⊢ ( 𝑟 = 𝑅 → ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) = ( 𝑧 𝐻 𝑥 ) )
19	18	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ↔ ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ) )
20	17	oveqd	⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) = ( 𝑥 𝐻 𝑧 ) )
21	20	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ↔ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) )
22	19 21	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ↔ ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) )
23	8 22	raleqbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) )
24	15 23	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ↔ ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) )
25	24	ralbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ↔ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) )
26	12 25	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) ↔ ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) ) )
27	9 26	rabeqbidv	⊢ ( 𝑟 = 𝑅 → { 𝑖 ∈ 𝒫 ran ( 1^st ‘ 𝑟 ) ∣ ( ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) } = { 𝑖 ∈ 𝒫 𝑋 ∣ ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) } )
28		df-idl	⊢ Idl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ 𝒫 ran ( 1^st ‘ 𝑟 ) ∣ ( ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) } )
29	1	fvexi	⊢ 𝐺 ∈ V
30	29	rnex	⊢ ran 𝐺 ∈ V
31	3 30	eqeltri	⊢ 𝑋 ∈ V
32	31	pwex	⊢ 𝒫 𝑋 ∈ V
33	32	rabex	⊢ { 𝑖 ∈ 𝒫 𝑋 ∣ ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) } ∈ V
34	27 28 33	fvmpt	⊢ ( 𝑅 ∈ RingOps → ( Idl ‘ 𝑅 ) = { 𝑖 ∈ 𝒫 𝑋 ∣ ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) } )

Metamath Proof Explorer

Theorem idlval

Proof