Metamath Proof Explorer

Definition df-idlsrg

Description: Define a structure for the ideals of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Assertion df-idlsrg 
|- IDLsrg = ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cidlsrg 
 |-  IDLsrg
1 vr 
 |-  r
2 cvv 
 |-  _V
3 clidl 
 |-  LIdeal
4 1 cv 
 |-  r
5 4 3 cfv 
 |-  ( LIdeal ` r )
6 vb 
 |-  b
7 cbs 
 |-  Base
8 cnx 
 |-  ndx
9 8 7 cfv 
 |-  ( Base ` ndx )
10 6 cv 
 |-  b
11 9 10 cop 
 |-  <. ( Base ` ndx ) , b >.
12 cplusg 
 |-  +g
13 8 12 cfv 
 |-  ( +g ` ndx )
14 clsm 
 |-  LSSum
15 4 14 cfv 
 |-  ( LSSum ` r )
16 13 15 cop 
 |-  <. ( +g ` ndx ) , ( LSSum ` r ) >.
17 cmulr 
 |-  .r
18 8 17 cfv 
 |-  ( .r ` ndx )
19 vi 
 |-  i
20 vj 
 |-  j
21 crsp 
 |-  RSpan
22 4 21 cfv 
 |-  ( RSpan ` r )
23 19 cv 
 |-  i
24 cmgp 
 |-  mulGrp
25 4 24 cfv 
 |-  ( mulGrp ` r )
26 25 14 cfv 
 |-  ( LSSum ` ( mulGrp ` r ) )
27 20 cv 
 |-  j
28 23 27 26 co 
 |-  ( i ( LSSum ` ( mulGrp ` r ) ) j )
29 28 22 cfv 
 |-  ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) )
30 19 20 10 10 29 cmpo 
 |-  ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) )
31 18 30 cop 
 |-  <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >.
32 11 16 31 ctp 
 |-  { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >. }
33 cts 
 |-  TopSet
34 8 33 cfv 
 |-  ( TopSet ` ndx )
35 23 27 wss 
 |-  i C_ j
36 35 wn 
 |-  -. i C_ j
37 36 20 10 crab 
 |-  { j e. b | -. i C_ j }
38 19 10 37 cmpt 
 |-  ( i e. b |-> { j e. b | -. i C_ j } )
39 38 crn 
 |-  ran ( i e. b |-> { j e. b | -. i C_ j } )
40 34 39 cop 
 |-  <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >.
41 cple 
 |-  le
42 8 41 cfv 
 |-  ( le ` ndx )
43 23 27 cpr 
 |-  { i , j }
44 43 10 wss 
 |-  { i , j } C_ b
45 44 35 wa 
 |-  ( { i , j } C_ b /\ i C_ j )
46 45 19 20 copab 
 |-  { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) }
47 42 46 cop 
 |-  <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >.
48 40 47 cpr 
 |-  { <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >. }
49 32 48 cun 
 |-  ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >. } )
50 6 5 49 csb 
 |-  [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >. } )
51 1 2 50 cmpt 
 |-  ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >. } ) )
52 0 51 wceq 
 |-  IDLsrg = ( r e. _V |-> [_ ( LIdeal ` r ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( LSSum ` r ) >. , <. ( .r ` ndx ) , ( i e. b , j e. b |-> ( ( RSpan ` r ) ` ( i ( LSSum ` ( mulGrp ` r ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. b |-> { j e. b | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >. } ) )