Theorem idlsrgtset

Description: Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	idlsrgtset.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
	idlsrgtset.2	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
	idlsrgtset.3	⊢ 𝐽 = ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } )
Assertion	idlsrgtset	⊢ ( 𝑅 ∈ 𝑉 → 𝐽 = ( TopSet ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		idlsrgtset.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
2		idlsrgtset.2	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
3		idlsrgtset.3	⊢ 𝐽 = ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } )
4	2	fvexi	⊢ 𝐼 ∈ V
5	4	mptex	⊢ ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ∈ V
6	5	rnex	⊢ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ∈ V
7		eqid	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } )
8	7	idlsrgstr	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) Struct ⟨ 1 , ; 1 0 ⟩
9		tsetid	⊢ TopSet = Slot ( TopSet ‘ ndx )
10		snsspr1	⊢ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ } ⊆ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ }
11		ssun2	⊢ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } )
12	10 11	sstri	⊢ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } )
13	8 9 12	strfv	⊢ ( ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ∈ V → ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) ) )
14	6 13	ax-mp	⊢ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
15		eqid	⊢ ( LSSum ‘ 𝑅 ) = ( LSSum ‘ 𝑅 )
16		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
17		eqid	⊢ ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
18	2 15 16 17	idlsrgval	⊢ ( 𝑅 ∈ 𝑉 → ( IDLsrg ‘ 𝑅 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
19	1 18	syl5eq	⊢ ( 𝑅 ∈ 𝑉 → 𝑆 = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
20	19	fveq2d	⊢ ( 𝑅 ∈ 𝑉 → ( TopSet ‘ 𝑆 ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) ) )
21	14 20	eqtr4id	⊢ ( 𝑅 ∈ 𝑉 → ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( TopSet ‘ 𝑆 ) )
22	3 21	syl5eq	⊢ ( 𝑅 ∈ 𝑉 → 𝐽 = ( TopSet ‘ 𝑆 ) )