Definition df-dic 36462

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 unit. 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.)

Assertion

Ref	Expression
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 ) ) } ) ) )

Distinct variable group:   w, k, q, r, f, s, g

Detailed syntax breakdown of Definition df-dic

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

This definition is referenced by:  dicffval  36463