Theorem idlsrgmulr

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

	Ref	Expression
Hypotheses	idlsrgmulr.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
	idlsrgmulr.2	⊢ 𝐵 = ( LIdeal ‘ 𝑅 )
	idlsrgmulr.3	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	idlsrgmulr.4	⊢ ⊗ = ( LSSum ‘ 𝐺 )
Assertion	idlsrgmulr	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑖 ∈ 𝐵 , 𝑗 ∈ 𝐵 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) = ( .r ‘ 𝑆 ) )

Proof

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