Metamath Proof Explorer

Definition df-dic

Description: Isomorphism C has domain of lattice atoms that are not less than or equal to the fiducial co-atom w . The value is a one-dimensional subspace generated by the pair consisting of the iota_ vector below and the endomorphism ring unity. Definition of phi(q) in Crawley p. 121. Note that we use the fixed atom ( ( oc k ) w ) to represent the p in their "Choose an atom p..." on line 21. (Contributed by NM, 15-Dec-2013)

Ref Expression
Assertion df-dic 
|- DIsoC = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( q e. { r e. ( Atoms ` k ) | -. r ( le ` k ) w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdic 
 |-  DIsoC
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 vq 
 |-  q
8 vr 
 |-  r
9 catm 
 |-  Atoms
10 5 9 cfv 
 |-  ( Atoms ` k )
11 8 cv 
 |-  r
12 cple 
 |-  le
13 5 12 cfv 
 |-  ( le ` k )
14 3 cv 
 |-  w
15 11 14 13 wbr 
 |-  r ( le ` k ) w
16 15 wn 
 |-  -. r ( le ` k ) w
17 16 8 10 crab 
 |-  { r e. ( Atoms ` k ) | -. r ( le ` k ) w }
18 vf 
 |-  f
19 vs 
 |-  s
20 18 cv 
 |-  f
21 19 cv 
 |-  s
22 vg 
 |-  g
23 cltrn 
 |-  LTrn
24 5 23 cfv 
 |-  ( LTrn ` k )
25 14 24 cfv 
 |-  ( ( LTrn ` k ) ` w )
26 22 cv 
 |-  g
27 coc 
 |-  oc
28 5 27 cfv 
 |-  ( oc ` k )
29 14 28 cfv 
 |-  ( ( oc ` k ) ` w )
30 29 26 cfv 
 |-  ( g ` ( ( oc ` k ) ` w ) )
31 7 cv 
 |-  q
32 30 31 wceq 
 |-  ( g ` ( ( oc ` k ) ` w ) ) = q
33 32 22 25 crio 
 |-  ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q )
34 33 21 cfv 
 |-  ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) )
35 20 34 wceq 
 |-  f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) )
36 ctendo 
 |-  TEndo
37 5 36 cfv 
 |-  ( TEndo ` k )
38 14 37 cfv 
 |-  ( ( TEndo ` k ) ` w )
39 21 38 wcel 
 |-  s e. ( ( TEndo ` k ) ` w )
40 35 39 wa 
 |-  ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) )
41 40 18 19 copab 
 |-  { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) }
42 7 17 41 cmpt 
 |-  ( q e. { r e. ( Atoms ` k ) | -. r ( le ` k ) w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } )
43 3 6 42 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> ( q e. { r e. ( Atoms ` k ) | -. r ( le ` k ) w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } ) )
44 1 2 43 cmpt 
 |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( q e. { r e. ( Atoms ` k ) | -. r ( le ` k ) w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } ) ) )
45 0 44 wceq 
 |-  DIsoC = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( q e. { r e. ( Atoms ` k ) | -. r ( le ` k ) w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } ) ) )