Theorem idlsrgbas

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

	Ref	Expression
Hypotheses	idlsrgbas.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
	idlsrgbas.2	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
Assertion	idlsrgbas	⊢ ( 𝑅 ∈ 𝑉 → 𝐼 = ( Base ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		idlsrgbas.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
2		idlsrgbas.2	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
3	2	fvexi	⊢ 𝐼 ∈ V
4		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 ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } )
5	4	idlsrgstr	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) Struct ⟨ 1 , ; 1 0 ⟩
6		baseid	⊢ Base = Slot ( Base ‘ ndx )
7		snsstp1	⊢ { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ }
8		ssun1	⊢ { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } )
9	7 8	sstri	⊢ { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } )
10	5 6 9	strfv	⊢ ( 𝐼 ∈ V → 𝐼 = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) ) )
11	3 10	ax-mp	⊢ 𝐼 = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
12		eqid	⊢ ( LSSum ‘ 𝑅 ) = ( LSSum ‘ 𝑅 )
13		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
14		eqid	⊢ ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
15	2 12 13 14	idlsrgval	⊢ ( 𝑅 ∈ 𝑉 → ( IDLsrg ‘ 𝑅 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
16	1 15	eqtrid	⊢ ( 𝑅 ∈ 𝑉 → 𝑆 = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
17	16	fveq2d	⊢ ( 𝑅 ∈ 𝑉 → ( Base ‘ 𝑆 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑅 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) ) )
18	11 17	eqtr4id	⊢ ( 𝑅 ∈ 𝑉 → 𝐼 = ( Base ‘ 𝑆 ) )