Metamath Proof Explorer

Theorem maxidlval

Description: The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011)

		Ref	Expression
	Hypotheses	maxidlval.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
		maxidlval.2	⊢ 𝑋 = ran 𝐺
	Assertion	maxidlval	⊢ ( 𝑅 ∈ RingOps → ( MaxIdl ‘ 𝑅 ) = { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		maxidlval.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		maxidlval.2	⊢ 𝑋 = ran 𝐺
3		fveq2	⊢ ( 𝑟 = 𝑅 → ( Idl ‘ 𝑟 ) = ( Idl ‘ 𝑅 ) )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( 1^st ‘ 𝑟 ) = ( 1^st ‘ 𝑅 ) )
5	4 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 1^st ‘ 𝑟 ) = 𝐺 )
6	5	rneqd	⊢ ( 𝑟 = 𝑅 → ran ( 1^st ‘ 𝑟 ) = ran 𝐺 )
7	6 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ran ( 1^st ‘ 𝑟 ) = 𝑋 )
8	7	neeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑖 ≠ ran ( 1^st ‘ 𝑟 ) ↔ 𝑖 ≠ 𝑋 ) )
9	7	eqeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑗 = ran ( 1^st ‘ 𝑟 ) ↔ 𝑗 = 𝑋 ) )
10	9	orbi2d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ↔ ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) )
11	10	imbi2d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) ↔ ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) )
12	3 11	raleqbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) ↔ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) )
13	8 12	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑖 ≠ ran ( 1^st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) ) ↔ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) ) )
14	3 13	rabeqbidv	⊢ ( 𝑟 = 𝑅 → { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1^st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) ) } = { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) } )
15		df-maxidl	⊢ MaxIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1^st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) ) } )
16		fvex	⊢ ( Idl ‘ 𝑅 ) ∈ V
17	16	rabex	⊢ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) } ∈ V
18	14 15 17	fvmpt	⊢ ( 𝑅 ∈ RingOps → ( MaxIdl ‘ 𝑅 ) = { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝑋 ) ) ) } )