Theorem idlsrgplusg

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

	Ref	Expression
Hypotheses	idlsrgplusg.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
	idlsrgplusg.2	⊢ ⊕ = ( LSSum ‘ 𝑅 )
Assertion	idlsrgplusg	⊢ ( 𝑅 ∈ 𝑉 → ⊕ = ( +g ‘ 𝑆 ) )

Proof

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