Metamath Proof Explorer

Theorem idlsrgval

Description: Lemma for idlsrgbas through idlsrgtset . (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypotheses idlsrgval.1 ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
idlsrgval.2 ⊢ ⊕ = ( LSSum ‘ 𝑅 )
idlsrgval.3 ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
idlsrgval.4 ⊢ ⊗ = ( LSSum ‘ 𝐺 )
Assertion idlsrgval ( 𝑅 ∈ 𝑉 → ( IDLsrg ‘ 𝑅 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ⊕ ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )

Proof

Step Hyp Ref Expression
1 idlsrgval.1 ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
2 idlsrgval.2 ⊢ ⊕ = ( LSSum ‘ 𝑅 )
3 idlsrgval.3 ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
4 idlsrgval.4 ⊢ ⊗ = ( LSSum ‘ 𝐺 )
5 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
6 fvexd ⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ 𝑟 ) ∈ V )
7 simpr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → 𝑏 = ( LIdeal ‘ 𝑟 ) )
8 simpl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → 𝑟 = 𝑅 )
9 8 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( LIdeal ‘ 𝑟 ) = ( LIdeal ‘ 𝑅 ) )
10 7 9 eqtrd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → 𝑏 = ( LIdeal ‘ 𝑅 ) )
11 10 1 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → 𝑏 = 𝐼 )
12 11 opeq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ )
13 8 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( LSSum ‘ 𝑟 ) = ( LSSum ‘ 𝑅 ) )
14 13 2 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( LSSum ‘ 𝑟 ) = ⊕ )
15 14 opeq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ = ⟨ ( +g ‘ ndx ) , ⊕ ⟩ )
16 8 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( RSpan ‘ 𝑟 ) = ( RSpan ‘ 𝑅 ) )
17 8 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
18 17 3 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( mulGrp ‘ 𝑟 ) = 𝐺 )
19 18 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) = ( LSSum ‘ 𝐺 ) )
20 19 4 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) = ⊗ )
21 20 oveqd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) = ( 𝑖 ⊗ 𝑗 ) )
22 16 21 fveq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) = ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) )
23 11 11 22 mpoeq123dv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) = ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) )
24 23 opeq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ = ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) ⟩ )
25 12 15 24 tpeq123d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ⊕ ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) ⟩ } )
26 11 rabeqdv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } )
27 11 26 mpteq12dv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
28 27 rneqd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
29 28 opeq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ = ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ )
30 11 sseq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( { 𝑖 , 𝑗 } ⊆ 𝑏 ↔ { 𝑖 , 𝑗 } ⊆ 𝐼 ) )
31 30 anbi1d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) ↔ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) ) )
32 31 opabbidv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } )
33 32 opeq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ = ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ )
34 29 33 preq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } = { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } )
35 25 34 uneq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( LIdeal ‘ 𝑟 ) ) → ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ⊕ ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
36 6 35 csbied ⊢ ( 𝑟 = 𝑅 → ⦋ ( LIdeal ‘ 𝑟 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ⊕ ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
37 df-idlsrg ⊢ IDLsrg = ( 𝑟 ∈ V ↦ ⦋ ( LIdeal ‘ 𝑟 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( LSSum ‘ 𝑟 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝑏 , 𝑗 ∈ 𝑏 ↦ ( ( RSpan ‘ 𝑟 ) ‘ ( 𝑖 ( LSSum ‘ ( mulGrp ‘ 𝑟 ) ) 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝑏 ↦ { 𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
38 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ⊕ ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) ⟩ } ∈ V
39 prex ⊢ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ∈ V
40 38 39 unex ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ⊕ ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) ∈ V
41 36 37 40 fvmpt ⊢ ( 𝑅 ∈ V → ( IDLsrg ‘ 𝑅 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ⊕ ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )
42 5 41 syl ⊢ ( 𝑅 ∈ 𝑉 → ( IDLsrg ‘ 𝑅 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ⊕ ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐼 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑖 ⊗ 𝑗 ) ) ) ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗 ) } ⟩ } ) )